12
$\begingroup$

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.

Improve this question
$\endgroup$
7
  • $\begingroup$ 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? $\endgroup$
    – Sameer Gupta
    Nov 28, 2014 at 20:38
  • $\begingroup$ @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? $\endgroup$
    – vzn
    Nov 28, 2014 at 22:35
  • 5
    $\begingroup$ @vzn: a trivial boolean function that is not expressible in 2-CNF is: $(x_1 \lor x_2 \lor x_3)$ $\endgroup$
    – Marzio De Biasi
    Nov 29, 2014 at 0:04
  • 2
    $\begingroup$ @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). $\endgroup$
    – Marzio De Biasi
    Nov 29, 2014 at 0:50
  • 1
    $\begingroup$ 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). $\endgroup$
    – vzn
    Nov 29, 2014 at 1:43

3 Answers 3

Reset to default
19
$\begingroup$

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.

Improve this answer
$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$
    – Sameer Gupta
    Nov 29, 2014 at 7:29
  • $\begingroup$ 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: cstheory.stackexchange.com/questions/200/… - 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? $\endgroup$
    – Sameer Gupta
    Nov 30, 2014 at 4:25
  • 1
    $\begingroup$ 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. $\endgroup$
    – David Eppstein
    Nov 30, 2014 at 6:32
  • 4
    $\begingroup$ 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). $\endgroup$
    – arnab
    Nov 30, 2014 at 7:37
10
$\begingroup$

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).

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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? $\endgroup$
    – Sameer Gupta
    Nov 29, 2014 at 6:54
  • 1
    $\begingroup$ @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. $\endgroup$
    – Yuval Filmus
    Nov 29, 2014 at 7:30
5
$\begingroup$

(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.

Improve this answer
$\endgroup$
7
  • 1
    $\begingroup$ Re (c), if you believe my answer then an equisatisfiable 2-CNF expression can be converted to a bona fide equivalent 2-CNF expression. $\endgroup$
    – Yuval Filmus
    Dec 5, 2014 at 20:42
  • $\begingroup$ At cstheory.stackexchange.com/questions/200/… $-$ 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.) $\endgroup$
    – Martin Seymour
    Dec 6, 2014 at 1:53
  • $\begingroup$ You can read my answer and see for yourself. Note that there are no time/space bounds in this case. $\endgroup$
    – Yuval Filmus
    Dec 6, 2014 at 5:34
  • 1
    $\begingroup$ @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. $\endgroup$
    – Emil Jeřábek
    Dec 6, 2014 at 17:08
  • $\begingroup$ 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? $\endgroup$
    – Martin Seymour
    Dec 6, 2014 at 20:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.