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.