Moreover, any faithful translation is potentially of exponential size when additional

```
variables are not allowed (Lifs
                                hitz and Razborov 2006)2
                                                           . However, for any tight
                                                                                    

```

program Π it holds that the answer sets of Π 
an be 
hara
terized faithfully by the satisfying truth assignments of a linear-size propositional formula alled Clark's ompletion (Clark 1978; Fages 1994) of Π, dened using a Boolean variable xa for ea h a ∈ atom(Π) as

$$C(\Pi)=\bigwedge_{h\in\mathsf{atom}(\Pi)\cup\{\bot\}}\bigg{(}x_{h}\leftrightarrow\bigvee_{r\in\mathsf{rule}(h)}\bigg{(}\bigwedge_{b\in\mathsf{body}(r)^{+}}x_{b}\wedge\bigwedge_{b\in\mathsf{body}(r)^{-}}\bar{x}_{b}\bigg{)}\bigg{)},\tag{6}$$

where rule(h) = {r ∈ Π | head(r) = h}. Noti
e that there are the spe
ial 
ases
(i) if h is ⊥ then the equivalen
e be
omes the negation of the right hand side,
(ii) if h is a fa
t, then the equivalen
e redu
es to the 
lause {xh}, and (iii) if an atom h does not appear in the head of any rule then the equivalen
e redu
es to the lause {x¯h}.

In this work, we will onsider the lausal representation of Boolean formulas.

A linear-size lausal translation of C(Π) is a
hieved by introdu
ing additionally a new Boolean variable xB for ea
h B ∈ body(Π). Using the new variables for the bodies, we arrive at the lausal ompletion

$$\mathsf{comp}(\Pi)=\bigcup_{B\in\mathsf{body}(\Pi)}\left\{x_{B}\equiv\bigwedge_{a\in B^{+}}x_{a}\wedge\bigwedge_{b\in B^{-}}\bar{x}_{b}\right\}\cup\bigcup_{B\in\mathsf{body}(\mathsf{rule}(\bot))}\{\{\bar{x}_{B}\}\}\tag{7}$$ $$\cup\bigcup_{h\in\mathsf{head}(\Pi)\setminus\{\bot\}}\left\{x_{h}\equiv\bigvee_{B\in\mathsf{body}(\mathsf{rule}(h))}x_{B}\right\}$$ (8) $$\cup\bigcup_{a\in\mathsf{atom}(\Pi)\setminus\mathsf{head}(\Pi)}\{\{\bar{x}_{a}\}\},\tag{9}$$  for the coherent $a=\Lambda$, $a=\mathsf{and}\equiv\mathsf{1}$, $a=\mathsf{and}$ for the sets of all non 

where the shorthands x ≡Vxi∈X xi and x ≡Wxi∈X xi stand for the sets of 
lauses
{x, x¯1, . . . , x¯n} ∪ Sxi∈X{**x, x** ¯ i} and Sxi∈X{x, x¯i} ∪ {x, x ¯ 1**, . . . , x**n}, respe
tively.

Example 2.3 For the normal logi program Π = {a ← b, ∼a. b ← c. c ← ∼b}, the lausal ompletion is

comp(Π) = {{x{b,∼a}, xa, x¯b}, {x¯{b,∼a}, x¯a}, {x¯{b,∼a}, xb}, {x{c}, x¯c}, {x¯{c}, xc}, {x{∼b}, xb}, {x¯{∼b}, x¯b}, {xa, x¯{b,∼a}}, {x¯a, x{b,∼a}}, {xb, x¯{c}}, {x¯b, x{c}}, {xc, x¯{∼b}}}, {x¯c, x{∼b}}.