Consider a 3-CNF formula $\Phi$, i.e., a conjunction of clauses of 3 literals. I call odd-SAT (or 1-or-3-in-3-SAT) the problem of checking whether there is an assignment of the variables such that each clause contains one or three true literals, i.e., the number of true literals in each clause is odd.

Is this 3SAT variant NP-hard?


1 Answer 1


Somewhat surprisingly to me, this problem is in fact in PTIME.

The key insight is that, considering a clause $C$, letting $0 \leq k \leq 3$ be the number of negated literals in $C$, then the clause is true iff the number of variables (not literals!) of $C$ assigned to true, plus $k$, is odd.

For instance, take the clause $(x, \neg y, z)$, there is one negation, so it is true if there is an even number of the variables $x, y, z$ which are true -- it doesn't matter which.

In other words, this SAT variant is actually a system of equations on the variables mod 2. For the example clause above, it would be $x + y + z = 0$ mod 2. This problem is known to be in PTIME -- it is one of the tractable cases of Schaefer's theorem.

PS: For the benefit of search engines let me also spell out that the problem 0-or-2-in-3-SAT, aka even-3-SAT, where each clause must contain 0 or 2 true literals, is also in PTIME for the same reason.

  • 4
    $\begingroup$ Bonus point: you can also solve #SAT on this class, this is the only class (ie the class of formulas having only affine clauses) from Schaefer's theorem that remains tractable for counting (see Creignou, N., & Hermann, M. (1996). Complexity of generalized satisfiability counting problems. Information and computation, 125(1), 1-12.). But weighted #SAT is #P-complete on this class! $\endgroup$
    – holf
    Sep 2, 2023 at 13:30
  • 5
    $\begingroup$ I think writing "the clause $x \lor \lnot y \lor z$" is the confusing part; this formula is unrelated to the "1-or-3-in-3" constraint on literals $x, \lnot y, z$. If you just write the constraint as $x \oplus (1 \oplus y) \oplus z = 1$ (which is equivalent to $x \oplus y \oplus z = 0$) then it's clear that this is an XOR constraint, and the problem is just XOR-SAT. $\endgroup$ Sep 3, 2023 at 20:19
  • 2
    $\begingroup$ @HuckBennett: thanks, you are right I should not write clauses in this way. (And yes I agree once you write them with XOR it becomes clear that the problem is tractable ;)) $\endgroup$
    – a3nm
    Sep 3, 2023 at 22:19
  • $\begingroup$ @holf: Oh, interesting, thanks! By "weighted #SAT" do you mean with weights 0, 1/2, 1; or do you need arbitrary weights for hardness? In fact do you remember where this hardness result comes from? $\endgroup$
    – a3nm
    Sep 3, 2023 at 22:32
  • $\begingroup$ Not on top of my head, I do not even remember the ref, I will check it out this week! $\endgroup$
    – holf
    Sep 4, 2023 at 10:25

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.