2
$\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$
  • $\begingroup$ What do you think? Have you tried applying Schaeffer's theorem to the bounded width case? $\endgroup$ – Yuval Filmus Nov 19 '17 at 16:51
  • $\begingroup$ Have you tried either coming up with an algorithm or showing that the problem is NP-complete? $\endgroup$ – Yuval Filmus Nov 19 '17 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$ – csTheoryBeginner Nov 19 '17 at 17:08
2
$\begingroup$

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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