0
$\begingroup$

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.

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ 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). $\endgroup$
    – Steven
    May 11 at 9:31
  • $\begingroup$ @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. $\endgroup$
    – Andreas H.
    May 11 at 9:33

1 Answer 1

Reset to default
1
$\begingroup$

Nevermind, I guess the answer is very simple.

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

If the problem and constraints are already in CNF form this a trivial append operation.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.