Complexity of 1-or-3-in-3-SAT (odd-3-SAT)

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?

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.

• 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!
– holf
Commented Sep 2, 2023 at 13:30
• 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. Commented Sep 3, 2023 at 20:19
• @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 ;))
– a3nm
Commented Sep 3, 2023 at 22:19
• @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?
– a3nm
Commented Sep 3, 2023 at 22:32
• Not on top of my head, I do not even remember the ref, I will check it out this week!
– holf
Commented Sep 4, 2023 at 10:25