<p>Somewhat surprisingly to me, this problem is in fact in PTIME.</p>
<p>The key insight is that, considering a clause <span class="math-container">$C$</span>, letting <span class="math-container">$0 \leq k \leq 3$</span> be the number of negated literals in <span class="math-container">$C$</span>, then the clause is true iff the number of variables (not literals!) of <span class="math-container">$C$</span> assigned to true, plus <span class="math-container">$k$</span>, is odd.</p>
<p>For instance, take the clause <span class="math-container">$(x, \neg y, z)$</span>, there is one negation, so it is true if there is an even number of the variables <span class="math-container">$x, y, z$</span> which are true -- it doesn't matter which.</p>
<p>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 <span class="math-container">$x + y + z = 0$</span> mod 2. This problem is known to be in PTIME -- it is one of the tractable cases of <a href="https://en.wikipedia.org/wiki/Schaefer%27s_theorem" rel="noreferrer">Schaefer's theorem</a>.</p>
<p>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.</p>

CC BY-SA 4.0
2023-09-02T13:30:45.313Z
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
CC BY-SA 4.0
2023-09-03T20:19:05.727Z
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.
Huck Bennett
CC BY-SA 4.0
2023-09-03T22:19:04.713Z
@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 ;))
Antoine Amarilli 'a3nm'
CC BY-SA 4.0
2023-09-03T22:32:44.183Z
@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?
Antoine Amarilli 'a3nm'
CC BY-SA 4.0
2023-09-04T10:25:08.093Z
Not on top of my head, I do not even remember the ref, I will check it out this week!
holf
CC BY-SA 4.0
2023-09-02T01:08:01.993Z
2023-09-03T22:18:41.110Z
2023-09-03T22:18:41.110Z
Antoine Amarilli 'a3nm'
<p>Consider a 3-CNF formula <span class="math-container">$\Phi$</span>, 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.</p>
<p><strong>Is this 3SAT variant NP-hard?</strong></p>

<np-hardness><sat><polynomial-time><csp>
Complexity of 1-or-3-in-3-SAT (odd-3-SAT)
Antoine Amarilli 'a3nm'
# Complexity of 1-or-3-in-3-SAT (odd-3-SAT)

(Asked by: username_0 on 2023-09-02)

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?**

**Tags:** np-hardness, sat, polynomial-time, csp

---

## 1 answers

### Answer by username_0 on 2023-09-02. Score: 14 | Accepted answer

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](https://en.wikipedia.org/wiki/Schaefer%27s_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.

> **Comments:**
> **username_1**: 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!  
> **username_2**: 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.  
> **username_0**: @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 ;))  
> **username_0**: @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?  
> **username_1**: Not on top of my head, I do not even remember the ref, I will check it out this week!  

---

