3
$\begingroup$

If a CNF contains only Horn and Xor clauses, and does not contain clauses of other types, then can its Satisfiability be determined in polynomial time?

$\endgroup$
3
  • $\begingroup$ What do you think? Have you tried applying Schaeffer's theorem to the bounded width case? $\endgroup$ Nov 19, 2017 at 16:51
  • $\begingroup$ Have you tried either coming up with an algorithm or showing that the problem is NP-complete? $\endgroup$ Nov 19, 2017 at 16:53
  • $\begingroup$ @Yuval Filmus - I have to admit that I am very new to this field, as a result not aware of Schaeffer's theorem. The problem that motivated my question is from a CSP that has continuous variables, whose feasibility is reducible to a SAT. I have been unsuccessful in resolving its complexity with the problem described in CSP form, but have no clue on how to go about this in SAT form. $\endgroup$ Nov 19, 2017 at 17:08

1 Answer 1

3
$\begingroup$

Hint: Using XOR clauses you can express "$x = \lnot y$", and this allows you to simulate general clauses by Horn clauses.

$\endgroup$
2
  • $\begingroup$ So I guess it should be NP complete. $\endgroup$ Nov 19, 2017 at 17:15
  • $\begingroup$ Yes, that's the conclusion. $\endgroup$ Nov 19, 2017 at 17:16

Your Answer

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

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