# If a CNF contains only Horn and Xor clauses, then what is the complexity of determining Satisfiability?

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?

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

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