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

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 ?

• $NP$-complete. But due to the constraints much of the solution space for standart SAT would be swept out. – rus9384 Sep 28 '18 at 22:15
• I suggest you work on finding a reduction from 3SAT, to prove this is NP-hard. – D.W. Sep 28 '18 at 22:55
• Yes I also think it is NP-complete. Reducing from 3-SAT seems a good idea. I will work on this track. Thank you ! – serge boisse Sep 29 '18 at 15:31

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