# Satisfiability of general Boolean formulas with at most two occurrences per variable

(If you know basics in theoretical computer science, you may skip immediately to the dark box below. I thought I would try to explain my question very carefully, to maximize the number of people that understand it.)

We say that a Boolean formula is a propositional formula over some 0-1 variables $x_1,\ldots,x_n$ involving AND and OR connectives, where the atoms are literals which are instances of either $x_i$ or $\neg x_i$ for some $i$. That is, a Boolean formula is a "monotone" formula over the $2n$ atoms $x_1,\ldots, x_n, \neg x_1,\ldots, \neg x_n$. For example, $$((\neg x_1 ~OR~ x_2) ~AND~ (\neg x_2 ~OR~ x_1)) ~OR~ x_3$$ is a Boolean formula expressing that either $x_1$ and $x_2$ take on the same value, or $x_3$ must be $1$. We say that a 0-1 assignment to the variables of a formula is satisfying if the formula evaluates to $1$ on the assignment.

The Cook-Levin theorem says that the general satisfiability of Boolean formulas problem is $NP$-complete: given an arbitrary formula, it is $NP$-hard to find a satisfying assignment for it. In fact, even satisfying Boolean formulas where each variable $x_i$ appears at most three times in the formula is $NP$-complete. (Here is a reduction from the general case to this case: Suppose a variable $x$ appears $k > 3$ times. Replace each of its occurrences with fresh new variables $x^1, x^2, \ldots, x^k$, and constrain these $k$ variables to all take on the same value, by ANDing the formula with $$(\neg x^1 ~OR~ x^2) ~AND~ (\neg x^2 ~OR~ x^3) ~AND~ \cdots ~AND~ (\neg x^{k-1} ~OR~ x^k) ~AND~ (\neg x^k ~OR~ x^1).$$ The total number of occurrences of each variable $x^j$ is now three.) On the other hand, if each variable appears only once in the formula, then the satisfiability algorithm is very easy: since we have a monotone formula in $x_1,\ldots, x_n, \neg x_1,\ldots, \neg x_n$, we set $x_i$ to $0$ if $\neg x_i$ appears, otherwise we set $x_i$ to $1$. If this assignment does not get the formula to output $1$, then no assignment will.

My question is, suppose every variable appears at most twice in a general Boolean formula. Is the satisfiability problem for this class of formulas $NP$-complete, or solvable in polynomial time?

EDIT: To clarify further, here is an example instance of the problem: $$((x_1 ~AND~ x_3) ~OR~ (x_2 ~AND~ x_4 ~AND~ x_5)) ~AND~ (\neg x_1 ~OR~ \neg x_4) ~AND~ (\neg x_2 ~OR~ (\neg x_3 ~AND~ \neg x_5))$$

Note that when we restrict the class of formulas further to conjunctive normal form (i.e. a depth-2 circuit, an AND of ORs of literals) then this "at most twice" problem is known to be solvable in polynomial time. In fact, applying the "resolution rule" repeatedly will work. But it is not clear (at least, not to me) how to extend resolution for the class of general formulas to get a polytime algorithm. Note when we reduce a formula to conjunctive normal form in the usual way, this reduction introduces variables with three occurrences. So it seems plausible that perhaps one might be able to encode an $NP$-complete problem in the additional structure provided by a formula, even one with only two occurrences per variable.

My guess is that the problem is polynomial time solvable. I'm very surprised that I could not find a reference to this problem in the literature. Perhaps I'm just not looking in the right places.

-
2-SAT is in P. See en.wikipedia.org/wiki/2-satisfiability . – Qiaochu Yuan Dec 21 '09 at 22:30
That is not my question! 2-SAT is conjunctive normal form with two variables per clause. – Ryan Williams Dec 21 '09 at 22:36
2-SAT is a different problem where each clause contains at most two literals. – Boris Bukh Dec 21 '09 at 22:36
+1 for detailed intro – Theo Johnson-Freyd Dec 22 '09 at 6:05

A theorem in a paper of Peter Heusch, "The Complexity of the Falsifiability Problem for Pure Implicational Formulas" (MFCS'95), seems to suggest the problem is NP-hard. I repeat the first part of its proof here:

By reduction from the restricted version of 3SAT where every variable occurs at most 3 times. Given such a CNF, WOLOG every variable with 3 occurrences occurs once positively and twice negatively. If $x$ is such a variable, let $C_1$, $C_2$ be the clauses such that $C_1 = \neg x \vee C_1'$ and $C_2 = \neg x \vee C_2'$. Introduce new variables $x'$ and $x''$ and replace $C_1$ and $C_2$ by $\neg x \vee (x' \wedge x'')$, $\neg x' \vee C_1'$, $\neg x'' \vee C_2'$. Repeat.

-
It's also in Discrete Applied Math. 1999, doi:10.1016/S0166-218X(99)00036-0 . What the paper actually proves hard are formulas with only implication and all but one variable appearing at most twice, but one can convert implications into disjunctions (using de Morgan to propagate nots downwards) and eliminate the one variable to show that and-or formulas with two occurrences per variable are also hard. Or, as Ryan O. suggests, pull out the key idea and use it in a direct reduction. – David Eppstein Dec 22 '09 at 4:09
Wow, this shows that the problem is NP-hard even for depth-3 Boolean formulas! I would have never guessed. No wonder I did not find it. Thanks a lot, Other Ryan! – Ryan Williams Dec 22 '09 at 4:15

Here is an argument that vaguely suggests this problem should be hard. Suppose that I had a gate $G$ with 6 incoming wires, $w_1$, $w_2$, ..., $w_6$ and 1 outgoing wire which output TRUE if and only if:

1. ($w_1$ OR $w_2$) AND ($w_3$ OR $w_4$) AND ($w_5$ OR $w_6$)

AND

1. ($w_1 \neq w_3$ OR $w_2 \neq w_4$) AND ($w_1 \neq w_5$ OR $w_2 \neq w_6$) AND ($w_3 \neq w_5$ OR $w_4 \neq w_6$).

I claim that it is NP-complete to determine whether a circuit built of $G$'s and AND's is satisfiable, even if each variable is only used twice.

Proof: I reduce to the problem of 3-edge colorability. For each edge of my graph, I have two boolean variables; for each vertex, I have a $G$-gate, all of those $G$ gates run into a big AND. The definition of $G$ precisely says that all my edges have different colors. Each variable is used twice because each edge lies on two vertices.

So, in order to prove Ryan's problem is polynomial, we have to use some difference between the AND and OR gates and my $G$ gate..

-
Very nice observation. This suggests another question: which collections of basis gates make the problem easy, and which make the problem hard? My intuition is that the choice of basis gates should make a huge difference. – Ryan Williams Dec 22 '09 at 2:34
A simpler but similar argument: if you had a gate with three inputs u,v,w that computed the function (u ⋀ v ⋀ w) ⋁ (¬u ⋀ ¬v ⋀ ¬w) you could use it to split one variable u into two equivalent variables v and w and get around the two-occurrences-per-variable limitation. – David Eppstein Dec 22 '09 at 2:35

I don't really have an answer for you, but there are at least some easy simplifications you can perform:

(1) If both occurrences of a variable have the same sign (or a variable occurs only once), you might as well set it to the value that makes both occurrences true.

(2) Suppose that both occurrences of a variable have opposite signs, and the paths from them to their least common ancestor in the expression tree consists only of conjunctions. Then all the values at the intermediate expressions along one of these paths, and at the LCA, must be false, so you might as well replace that whole subtree by a false literal.

(3) Added after seeing Ryan's example of (x ⋁ y) ⋀ ¬x ⋀ ¬y: suppose that both occurrences of a variable have opposite signs, and one of the paths to their least common ancestor consists only of conjunctions. Then you might as well set that occurrence of the variable to be true, and the other one to false, because the opposite setting cannot lead to a true value at the LCA.

Maybe it's the case that any nontrivial formula containing none of these patterns is always satisfiable?

-
I was aware of points (1) and (2), but neglected to point them out. They should probably be present in any prospective algorithm. As for your question, what about the formula "(x1 OR x2) AND NOT(x1) AND NOT(x2)"? – Ryan Williams Dec 22 '09 at 0:56
By similar logic to (1), in the case where each variable appears only once, the formula is always satisfiable. – Reid Barton Dec 22 '09 at 0:59
Interesting... note we can throw in the "duals" of (2) and (3) as well: if the paths to the LCA of x and NOT(x) are all ORs, then we can replace the subtree with 1; if one path to the LCA is only ORs, we might as well set the literal to make that OR true. Now I do not know if it's always satisfiable otherwise... – Ryan Williams Dec 22 '09 at 1:21