12

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.

Sameer Gupta
  • 171
  • 7
  • 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 Nov 28 '14 at 20:38
  • @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 Nov 28 '14 at 22:35
  • 5
    @vzn: a trivial boolean function that is not expressible in 2-CNF is: $(x_1 \lor x_2 \lor x_3)$ – Marzio De Biasi Nov 29 '14 at 00:04
  • 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). – Marzio De Biasi Nov 29 '14 at 00:50
  • 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 Nov 29 '14 at 01:12
  • 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. also have seen a similar concept show up in monotone circuit lower bounds proofs (Razborov). – vzn Nov 29 '14 at 01:43
  • vzn, thanks, and see my comment below David's answer. – Sameer Gupta Nov 29 '14 at 07:15

3 Answers3

19

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.

David Eppstein
  • 50,990
  • 3
  • 170
  • 278
  • 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 Nov 29 '14 at 07:29
  • 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 Nov 30 '14 at 04:25
  • 1
    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 Nov 30 '14 at 06:32
  • 4
    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 Nov 30 '14 at 07:37
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).

Yuval Filmus
  • 14,445
  • 1
  • 48
  • 92
  • 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 Nov 29 '14 at 06:54
  • 1
    @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 Nov 29 '14 at 07:30
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.

Martin Seymour
  • 273
  • 2
  • 5
  • 1
    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 Dec 05 '14 at 20:42
  • 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 Dec 06 '14 at 01:53
  • You can read my answer and see for yourself. Note that there are no time/space bounds in this case. – Yuval Filmus Dec 06 '14 at 05:34
  • 1
    @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 Dec 06 '14 at 17:08
  • 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 Dec 06 '14 at 20:11
  • 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 Dec 06 '14 at 23:31
  • 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 Dec 07 '14 at 19:43