<p>Let $P(x_1,\ldots,x_n)$ be a property on $n$ variables. Suppose that there is a 2CNF formula $\varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)$ such that
$$P(x_1,\ldots,x_n) \Leftrightarrow \exists y_1 \cdots \exists y_m \varphi(x_1,\ldots,x_n,y_1,\ldots,y_m).$$
We claim that $\varphi$ is equivalent to a 2CNF formula $\psi$ involving only $x_1,\ldots,x_n$. To prove this, it is enough to show how to eliminate $y_m$. Write
$$ \varphi = \chi \land \bigwedge_{k=1}^s (y_m \lor U_k) \land \bigwedge_{\ell=1}^t (\overline{y_m} \lor V_\ell),$$
where $U_k,V_\ell$ are literals, and $\chi$ doesn't involve $y_m$. The formula $\varphi$ is equivalent to
$$
\chi \land (\overline{y_m} \Rightarrow \bigwedge_{k=1}^s U_k) \land (y_m \Rightarrow \bigwedge_{\ell=1}^t V_\ell) \\ \Longleftrightarrow \\
\chi \land (\bigwedge_{k=1}^s U_k \lor \bigwedge_{\ell=1}^t V_\ell) \\ \Longleftrightarrow \\
\chi \land \bigwedge_{k=1}^s \bigwedge_{\ell=1}^t (U_k \lor V_\ell)
$$
This proves the claim when $y_m$ doesn't appear in a unit clause; if it does, we can eliminate it directly.</p>

<p>We conclude that $P(x_1,\ldots,x_n)$ is expressible as a 2CNF formula iff there is a 2CNF formula $\psi(x_1,\ldots,x_n)$ equivalent to $P$. Therefore a property $P$ is expressible as a 2CNF if every falsifying assignment is forced by at most two literals. In particular, $K$-clique and $K$-matching are not expressible as 2CNFs (except for the corner case $n$-clique).</p>

CC BY-SA 3.0
2014-11-29T06:54:41.300Z
Yuval, thanks, but I have a question. why eliminate the $y_i$'s? Why restrict $\psi$ to contain only $x_1$, $x_2$, $\cdots$, $x_n$? For example, consider a poly-time solvable special case $\phi_1$ of 3CNF. When you convert this to a 2CNF formula $\phi_2$, one would "expect" $\phi_2$ to contain additional variables, isn't it?  Am I missing something?
Sameer Gupta
CC BY-SA 3.0
2014-11-29T07:30:46.980Z
@Sameer What I'm showing is that you don't need the $y_i$s. They don't help you. You can get rid of them. If you don't have the $y_i$s, it's much easier to understand what's going on.
Yuval Filmus
CC BY-SA 3.0
2014-11-29T02:32:01.267Z
2014-11-29T02:32:01.267Z
Yuval Filmus
<p>(a) Addition and multiplication are both in $L$:
<a href="http://people.clarkson.edu/~alexis/PCMI/Notes/lectureB02.pdf">http://people.clarkson.edu/~alexis/PCMI/Notes/lectureB02.pdf</a> $-$
so counting in $L$ should be possible.</p>

<p>(Yes, I know that addition, multiplication and counting compute functions, but it's easy to convert them to decision versions of their respective problems.)</p>

<p>(b) Since $L \subseteq NL$, and 2-CNF is complete for $NL$ under $AC^0$ reductions, the counting algorithm (the TM) can be reduced to a 2-CNF expression similarly (under $AC^0$).</p>

<p>(c) So <strong>for counting</strong>, even though you may be unable to obtain an equivalent expression in 2-CNF, using the method outlined in (b), you can obtain an <em>equisatisfiable</em> 2-CNF expression.</p>

<p>So yes, 2-SAT <em>can</em> count.</p>

<p>Were you hoping to show that Matching cannot be in $NL$ by showing that $|M|$ cannot be counted in $NL$? I don't think that's going to work.</p>

CC BY-SA 3.0
2014-12-05T20:42:00.147Z
Re (c), if you believe my answer then an equisatisfiable 2-CNF expression can be converted to a bona fide equivalent 2-CNF expression.
Yuval Filmus
CC BY-SA 3.0
2014-12-06T01:53:37.153Z
At http://cstheory.stackexchange.com/questions/200/translating-sat-to-hornsat $-$ it is shown that for Horn-SAT, equisatifiability is **not** the same as equivalence. $~$  Are you saying that they are the same for 2-CNF? $~$  (Also the equisatisfiable or equivalent expression should be obtained within certain time/space bounds.)
Martin Seymour
CC BY-SA 3.0
2014-12-06T05:34:47.513Z
You can read my answer and see for yourself. Note that there are no time/space bounds in this case.
Yuval Filmus
CC BY-SA 3.0
2014-12-06T17:08:28.307Z
@Yuval: What Martin Seymour means by equisatisfiability is that for the given problem $L$, there is an efficient (say, $\mathrm{AC}^0$?) reduction $f$ whose range are 2-CNF, and $x\in L$ iff $f(x)$ is satisfiable. The reduction is not in any way part of the syntax of the formula, so there is nothing in your answer that would magic it away. And, as follows from David Eppstein’s answer, it is in general indispensable. What I’m not convinced about is that this idea of “equisatisfiability” has anything to do with the original question.
Emil Jeřábek
CC BY-SA 3.0
2014-12-06T20:11:20.370Z
Emil, Precisely! In the other direction, if Yuval starts with an *equisatisfiable* expression ($\phi$ in his answer), there will be NO $x_i$'s in his $\phi$ to begin with $-$ so at the end of all his operations (or rather, during his operations), he will NOT be able to magically make the $x_i$'s appear in his expression. $~$ Emil, sorry I don't understand what you mean by "indispensable according to David Eppstein's answer". Can you please explain?
Martin Seymour
CC BY-SA 3.0
2014-12-06T23:31:34.033Z
Using David's concept -- Consider an instance of Matching, say a path with 20 edges. Let the lower bound $K$ be 8.  We can produce 3 feasible solutions (matchings) with 8 edges in each, whereas the 4th solution produced by majority polymorphism from the first 3 solutions only has 7 edges and hence infeasible (*not* a matching). Easy to do this. But (I believe) this only rules out "equivalent" 2CNF formulas for Matching. However a reduction from Matching which produces an *equisatisfiable* 2-CNF formula as described by Emil is still a possibility. I think this is what Martin means.
Sameer Gupta
CC BY-SA 3.0
2014-12-07T19:43:25.803Z
That's right. There needs to be a proof that there is **no** efficient reduction (as Emil described) from some Problem $A$ resulting in an equisatisfiable 2-CNF formula. **Only** then can it be concluded that $A$ cannot be expressed in 2-CNF. The methods outlined by David Eppstein and Yual Filmus are NOT sufficient to draw such a conclusion.  Anyway, that's my 2 cents.
Martin Seymour
CC BY-SA 3.0
2014-12-05T06:48:37.523Z
2014-12-05T11:49:36.143Z
2014-12-05T11:49:36.143Z
Martin Seymour
<p>A family of bitvectors is the class of solutions to a 2-SAT problem if and only if it has the median property: if you apply the bitwise majority function to any three solutions you get another solution. See e.g. <a href="https://en.wikipedia.org/wiki/Median_graph#2-satisfiability">https://en.wikipedia.org/wiki/Median_graph#2-satisfiability</a> and its references. So if you can find three solutions for which this is not true, then you know it cannot be expressed in 2-CNF.</p>

CC BY-SA 3.0
2014-11-29T07:29:05.937Z
David, thanks, will look this up. @vzn - Is David's answer related to what you commented 2 days ago at the chat site, that 3SAT formulas exist for all sets of bit vectors, and looking for a result for 2SAT formulas concerning bit-vector sets?
Sameer Gupta
CC BY-SA 3.0
2014-11-30T04:25:23.667Z
David, Yuval - Certainly your proofs will work if one uses the same set of variables.  But what if the set of variables used can be completely different? Have a look at Martin Seymour's answer here: http://cstheory.stackexchange.com/questions/200/translating-sat-to-hornsat - To show that there is no equi-satisfiable *reduction* (preferably logspace) from K-Clique or K-Matching to 2SAT would require a different proof. Thoughts?
Sameer Gupta
CC BY-SA 3.0
2014-11-30T06:32:11.533Z
Adding auxiliary variables and then projecting them out won't help, because if the median property is true for the augmented system of variables then it's still true in the projection.
David Eppstein
CC BY-SA 3.0
2014-11-30T07:37:56.003Z
Another way to say it is that median (or majority) is a *polymorphism* for 2SAT constraints. In fact, it's known that *any* CSP (even non-boolean) that has majority as a polymorphism is in $\mathsf{NL} \subseteq \mathsf{P}$ (Dalmau-Krokhin '08).
arnab
CC BY-SA 3.0
2014-11-29T03:58:47.290Z
2014-11-29T03:58:47.290Z
David Eppstein
<p>How does one show that a certain property cannot be expressed in 2-CNF (2-SAT)?  Are there any games, such as pebble games?  It seems that the classical black pebble game and the black-white pebble game are unsuitable for this (they are PSPACE complete, according to Hertel and Pitassi, SIAM J of Computing, 2010).</p>

<p>Or any techniques other than games?</p>

<p><strong>Edit</strong>:  I was thinking of properties that involve counting (or cardinality) of an <em>unknown</em> predicate (<em>SO</em> predicate, as finite model theorists would say).  For example, as in Clique or unweighted Matching.
(a) <i>Clique</i>: Is there a clique $C$ in the given graph $G$ such that $|C| \ge$ some given number $K$? $~$ (b) <i>Matching</i>: Is there a matching $M$ in $G$ such that $|M| \ge K$?</p>

<p>Can 2-SAT count?  Does it have a counting mechanism?  Seems doubtful.</p>

CC BY-SA 3.0
2014-11-28T20:38:33.853Z
I understand that there are Ehrenfeucht–Fraïssé game (for FO) and Ajtai-Fagin game (for monadic SO) in finite model theory.  But not sure if they are sufficient here.  Also the games in FMT get complicated with ordered structures, right?
Sameer Gupta
CC BY-SA 3.0
2014-11-28T22:35:54.420Z
@Marzio it seems like some proof that not all Boolean functions are expressible in 2CNF as you state would answer the question (not actually sure of that, dont see it as obvious). what is that proof? is it published somewhere?
vzn
CC BY-SA 3.0
2014-11-29T00:04:42.013Z
@vzn: a trivial boolean function  that is not expressible in 2-CNF is: $(x_1 \lor x_2 \lor x_3)$
Marzio De Biasi
CC BY-SA 3.0
2014-11-29T00:50:57.633Z
@SameerGupta: after the reformulation, perhpas the question becomes difficult :-); indeed $\exists P_1...\exists P_n \forall \bar{z} \varphi( P_1,...,P_n, \bar{z})$, where $\varphi$ is limited to clauses with two variables (SO-Krom) captures NL over ordered structures, while existential SO captures NP. Obviously limited to FO 2-SAT cannot count (and the Ehrenfeucht–Fraïssé game or compactness techniques are far enough, because you can use them to prove that PARITY is not FO definable).
Marzio De Biasi
CC BY-SA 3.0
2014-11-29T01:12:48.690Z
Marzio, I think we should find a game for SO-Krom.  At least this is one of the options.  I wonder if there's anything on separating Horn-SAT from 2-SAT (Horn-SAT being P-complete).
Sameer Gupta
CC BY-SA 3.0
2014-11-29T01:43:36.920Z
ok. there seems to be some general theory that $k$-SAT cannot express all boolean functions for constant $k$. what is that theory? this question asks about special case $k=2$. note there is a concept of "reducing" $n$-SAT to 3-SAT via the [Tseitin transform](http://en.wikipedia.org/wiki/Tseitin_transformation). also have seen a similar concept show up in monotone circuit lower bounds proofs (Razborov).
vzn
CC BY-SA 3.0
2014-11-29T07:15:59.283Z
vzn, thanks, and see my comment below David's answer.
Sameer Gupta
<sat><lower-bounds><combinatorial-game-theory>
Properties expressible in 2-CNF or 2-SAT
Sameer Gupta
# Properties expressible in 2-CNF or 2-SAT

(Asked by: username_0 on 2014-11-28)

How does one show that a certain property cannot be expressed in 2-CNF (2-SAT)? Are there any games, such as pebble games? It seems that the classical black pebble game and the black-white pebble game are unsuitable for this (they are PSPACE complete, according to Hertel and Pitassi, SIAM J of Computing, 2010).

Or any techniques other than games?

**Edit**: I was thinking of properties that involve counting (or cardinality) of an *unknown* predicate (*SO* predicate, as finite model theorists would say). For example, as in Clique or unweighted Matching.
(a) *Clique*: Is there a clique $C$ in the given graph $G$ such that $|C| \ge$ some given number $K$? $~$ (b) *Matching*: Is there a matching $M$ in $G$ such that $|M| \ge K$?

Can 2-SAT count? Does it have a counting mechanism? Seems doubtful.

**Tags:** sat, lower-bounds, combinatorial-game-theory

> **Comments:**
> **username_0**: I understand that there are Ehrenfeucht–Fraïssé game (for FO) and Ajtai-Fagin game (for monadic SO) in finite model theory.  But not sure if they are sufficient here.  Also the games in FMT get complicated with ordered structures, right?  
> **username_1**: @Marzio it seems like some proof that not all Boolean functions are expressible in 2CNF as you state would answer the question (not actually sure of that, dont see it as obvious). what is that proof? is it published somewhere?  
> **username_2**: @username_1: a trivial boolean function  that is not expressible in 2-CNF is: $(x_1 \lor x_2 \lor x_3)$  
> **username_2**: @SameerGupta: after the reformulation, perhpas the question becomes difficult :-); indeed $\exists P_1...\exists P_n \forall \bar{z} \varphi( P_1,...,P_n, \bar{z})$, where $\varphi$ is limited to clauses with two variables (SO-Krom) captures NL over ordered structures, while existential SO captures NP. Obviously limited to FO 2-SAT cannot count (and the Ehrenfeucht–Fraïssé game or compactness techniques are far enough, because you can use them to prove that PARITY is not FO definable).  
> **username_0**: Marzio, I think we should find a game for SO-Krom.  At least this is one of the options.  I wonder if there's anything on separating Horn-SAT from 2-SAT (Horn-SAT being P-complete).  
> **username_1**: ok. there seems to be some general theory that $k$-SAT cannot express all boolean functions for constant $k$. what is that theory? this question asks about special case $k=2$. note there is a concept of "reducing" $n$-SAT to 3-SAT via the [Tseitin transform](http://en.wikipedia.org/wiki/Tseitin_transformation). also have seen a similar concept show up in monotone circuit lower bounds proofs (Razborov).  
> **username_0**: username_1, thanks, and see my comment below David's answer.  

---

## 3 answers

### Answer by username_6 on 2014-11-29. Score: 19 | Accepted answer

A family of bitvectors is the class of solutions to a 2-SAT problem if and only if it has the median property: if you apply the bitwise majority function to any three solutions you get another solution. See e.g. <https://en.wikipedia.org/wiki/Median_graph#2-satisfiability> and its references. So if you can find three solutions for which this is not true, then you know it cannot be expressed in 2-CNF.

> **Comments:**
> **username_0**: David, thanks, will look this up. @username_1 - Is David's answer related to what you commented 2 days ago at the chat site, that 3SAT formulas exist for all sets of bit vectors, and looking for a result for 2SAT formulas concerning bit-vector sets?  
> **username_0**: David, Yuval - Certainly your proofs will work if one uses the same set of variables.  But what if the set of variables used can be completely different? Have a look at username_4's answer here: http://cstheory.stackexchange.com/questions/200/translating-sat-to-hornsat - To show that there is no equi-satisfiable *reduction* (preferably logspace) from K-Clique or K-Matching to 2SAT would require a different proof. Thoughts?  
> **username_6**: Adding auxiliary variables and then projecting them out won't help, because if the median property is true for the augmented system of variables then it's still true in the projection.  
> **username_7**: Another way to say it is that median (or majority) is a *polymorphism* for 2SAT constraints. In fact, it's known that *any* CSP (even non-boolean) that has majority as a polymorphism is in $\mathsf{NL} \subseteq \mathsf{P}$ (Dalmau-Krokhin '08).  

---

### Answer by username_3 on 2014-11-29. Score: 10

Let $P(x\_1,\ldots,x\_n)$ be a property on $n$ variables. Suppose that there is a 2CNF formula $\varphi(x\_1,\ldots,x\_n,y\_1,\ldots,y\_m)$ such that
$$P(x\_1,\ldots,x\_n) \Leftrightarrow \exists y\_1 \cdots \exists y\_m \varphi(x\_1,\ldots,x\_n,y\_1,\ldots,y\_m).$$
We claim that $\varphi$ is equivalent to a 2CNF formula $\psi$ involving only $x\_1,\ldots,x\_n$. To prove this, it is enough to show how to eliminate $y\_m$. Write
$$ \varphi = \chi \land \bigwedge\_{k=1}^s (y\_m \lor U\_k) \land \bigwedge\_{\ell=1}^t (\overline{y\_m} \lor V\_\ell),$$
where $U\_k,V\_\ell$ are literals, and $\chi$ doesn't involve $y\_m$. The formula $\varphi$ is equivalent to
$$
\chi \land (\overline{y\_m} \Rightarrow \bigwedge\_{k=1}^s U\_k) \land (y\_m \Rightarrow \bigwedge\_{\ell=1}^t V\_\ell) \\ \Longleftrightarrow \\
\chi \land (\bigwedge\_{k=1}^s U\_k \lor \bigwedge\_{\ell=1}^t V\_\ell) \\ \Longleftrightarrow \\
\chi \land \bigwedge\_{k=1}^s \bigwedge\_{\ell=1}^t (U\_k \lor V\_\ell)
$$
This proves the claim when $y\_m$ doesn't appear in a unit clause; if it does, we can eliminate it directly.

We conclude that $P(x\_1,\ldots,x\_n)$ is expressible as a 2CNF formula iff there is a 2CNF formula $\psi(x\_1,\ldots,x\_n)$ equivalent to $P$. Therefore a property $P$ is expressible as a 2CNF if every falsifying assignment is forced by at most two literals. In particular, $K$-clique and $K$-matching are not expressible as 2CNFs (except for the corner case $n$-clique).

> **Comments:**
> **username_0**: Yuval, thanks, but I have a question. why eliminate the $y_i$'s? Why restrict $\psi$ to contain only $x_1$, $x_2$, $\cdots$, $x_n$? For example, consider a poly-time solvable special case $\phi_1$ of 3CNF. When you convert this to a 2CNF formula $\phi_2$, one would "expect" $\phi_2$ to contain additional variables, isn't it?  Am I missing something?  
> **username_3**: @Sameer What I'm showing is that you don't need the $y_i$s. They don't help you. You can get rid of them. If you don't have the $y_i$s, it's much easier to understand what's going on.  

---

### Answer by username_4 on 2014-12-05. Score: 5

(a) Addition and multiplication are both in $L$:
<http://people.clarkson.edu/~alexis/PCMI/Notes/lectureB02.pdf> $-$
so counting in $L$ should be possible.

(Yes, I know that addition, multiplication and counting compute functions, but it's easy to convert them to decision versions of their respective problems.)

(b) Since $L \subseteq NL$, and 2-CNF is complete for $NL$ under $AC^0$ reductions, the counting algorithm (the TM) can be reduced to a 2-CNF expression similarly (under $AC^0$).

(c) So **for counting**, even though you may be unable to obtain an equivalent expression in 2-CNF, using the method outlined in (b), you can obtain an *equisatisfiable* 2-CNF expression.

So yes, 2-SAT *can* count.

Were you hoping to show that Matching cannot be in $NL$ by showing that $|M|$ cannot be counted in $NL$? I don't think that's going to work.

> **Comments:**
> **username_3**: Re (c), if you believe my answer then an equisatisfiable 2-CNF expression can be converted to a bona fide equivalent 2-CNF expression.  
> **username_4**: At http://cstheory.stackexchange.com/questions/200/translating-sat-to-hornsat $-$ it is shown that for Horn-SAT, equisatifiability is **not** the same as equivalence. $~$  Are you saying that they are the same for 2-CNF? $~$  (Also the equisatisfiable or equivalent expression should be obtained within certain time/space bounds.)  
> **username_3**: You can read my answer and see for yourself. Note that there are no time/space bounds in this case.  
> **username_5**: @Yuval: What username_4 means by equisatisfiability is that for the given problem $L$, there is an efficient (say, $\mathrm{AC}^0$?) reduction $f$ whose range are 2-CNF, and $x\in L$ iff $f(x)$ is satisfiable. The reduction is not in any way part of the syntax of the formula, so there is nothing in your answer that would magic it away. And, as follows from username_6’s answer, it is in general indispensable. What I’m not convinced about is that this idea of “equisatisfiability” has anything to do with the original question.  
> **username_4**: Emil, Precisely! In the other direction, if Yuval starts with an *equisatisfiable* expression ($\phi$ in his answer), there will be NO $x_i$'s in his $\phi$ to begin with $-$ so at the end of all his operations (or rather, during his operations), he will NOT be able to magically make the $x_i$'s appear in his expression. $~$ Emil, sorry I don't understand what you mean by "indispensable according to username_6's answer". Can you please explain?  
> **username_0**: Using David's concept -- Consider an instance of Matching, say a path with 20 edges. Let the lower bound $K$ be 8.  We can produce 3 feasible solutions (matchings) with 8 edges in each, whereas the 4th solution produced by majority polymorphism from the first 3 solutions only has 7 edges and hence infeasible (*not* a matching). Easy to do this. But (I believe) this only rules out "equivalent" 2CNF formulas for Matching. However a reduction from Matching which produces an *equisatisfiable* 2-CNF formula as described by Emil is still a possibility. I think this is what Martin means.  
> **username_4**: That's right. There needs to be a proof that there is **no** efficient reduction (as Emil described) from some Problem $A$ resulting in an equisatisfiable 2-CNF formula. **Only** then can it be concluded that $A$ cannot be expressed in 2-CNF. The methods outlined by username_6 and Yual Filmus are NOT sufficient to draw such a conclusion.  Anyway, that's my 2 cents.  

---

