# How to solve boolean SAT with equality constraints

Say I have boolean formula in form of a CNF(x1,x2,...) with $$x_i$$ being boolean variables.

Testing the satisfiability of the CNF is the SAT problem, i.e. determine if there are $$x_i$$ for which the formula becomes True. So far I understand, this assumes that the variables are independent.

But what if my $$x_i$$ are not independent variables but have some sort of interdependence? (e.g. $$x_1$$ and $$x_2$$ are mutually exclusive. Which for instance would be encoded as $$x_1 \hat{} x_2$$ == True)

Lets assume these constraints are written by CONSTR-CNF(x1,x2,...) == True with CONSTR-CNF being some boolean expression (i.e. one or more interdependencies).

The question is now is there an efficient algorithm to tackle these kind of problems?

Or can we rewrite the problem to the original unconstrained problem with some algorithm? I.e. integrate the constraints into the CNF, possibly introducing new variables but not changing the satisfiability?

Note: This is not the same as the cardinality constrains where one places limits on the number of input variables to be true at the same time.

• If you can write the constraints in CNF, you can just append them to the formula as additional clauses. Your problem cannot be easier than CNF-SAT since (when the constraints can be arbitrary) it is a generalization. If you restrict yourself to constraints of specific form the problem might become easier (think e.g., of formulas where at most one variable can be set to true, which can trivially be solved in polynomial-time). May 11 at 9:31
• @Steven Yes, true. After posting the question, that occurred to me as well. I guess I should have thought about it a bit more before posting. Not sure if I should leave the question. May 11 at 9:33

Simply test if CNF(x_1,x_2,...) & CONST-CNF(x_1,x_2,...) is satisfiable.