SAT for positive CNF clauses with exactly half of the variables being true

Question

I am focusing here on positive even SAT problems, that is a CNF for which all literals are positive, and in which an even number n of variables occur. This is obviously trivial : just set all variables to true and all clauses are satisfied. The same if we look for an assignment that would have all but one variables being true (unless the problem is 1-SAT, which is also trivial)

But I am wondering if we could find an algorithm that searches for some solution (or proves the absence of solutions) with exactly half of the variables being true, the other half being false. Have you an idea of how to create this algorithm ? And what could be its complexity ?

Answer 1

Your problem is NP-complete by the modern presentation of Schaefer's dichotomy theorem.

You can also prove its NP-completeness by direct reduction of SAT to your problem. If a CNF formula has $n$ variables $x_1 \dots x_n$ introduce $n$ new variables $y_1 \dots y_n$ and add 2-CNF clauses that force each $y$ variable to have the opposite value of the corresponding $x$ value. I.e. $$(x_1 \lor y_1)$$ $$(\lnot x_1 \lor \lnot y_1)$$ $$(x_2 \lor y_2)$$ $$(\lnot x_2 \lor \lnot y_2)$$ $$\dots$$ $$(x_n \lor y_n)$$ $$(\lnot x_n \lor \lnot y_n)$$

All solutions to the resulting formula will have half the variables with true values and half false.

For unaltered formulas, you don't need a special algorithm to find half-true half-false solutions. Take any CNF formula with an even number of variables and then add CNF clauses encoding a chain of adder circuits that sums the values of all the variables. Next, add a comparison circuit that is only satisfied if the sum is one-half the total number of variables. Run a normal SAT solver on the result and it will output only solutions where one-half the original variables have a true value. This is a somewhat naive solution but it gets the job done.

Search the literature a bit more and you will discover SAT solvers that accept pseudo-Boolean constraints in addition to CNF. With these you can write out the $x_1 + x_2 + x_3 + \dots + x_n = n / 2$ equation explicitly and the solver will either churn out the adder circuits for you or just handle the equation internally.

Your special SAT problem is also readily transformed into a 0-1 integer programming problem for which there are solvers available.