It is known that SAT is hard even when restricted to, e.g., formulas with exactly 3 literals per clause and at most 4 occurrences per variable. On the other hand it is easy if there are exactly 3 literals per clause and at most 3 occurrences per variable. I am interested in other restrictions on the number of occurrences per variable.

For a set $S$ of positive integers, define $(k,S)$-SAT to be the satisfiability problem restricted to boolean formulas with exactly $k$ literals per clause, and the number of occurrences of each variable is in the set $S$. For example $(3,\{1,2,3,4\})$-SAT is hard, $(3,\{1,2,3\})$-SAT is easy.


If $k=3$ and $S$ is the even numbers, then you can easily pad an instance of $3$-SAT to get an equivalent instance of $(3,S)$-SAT. Is there anything known more generally? Is it always hard if $S$ is infinite? Are there any easy cases for $k=3$ besides $S\subseteq \{1,2,3\}$?

Main Question

I am really interested in 1-in-3-SAT restricted to the case where each variable appears an even number of times - the standard reduction from 3-SAT introduces new variables some of which occur an odd number of times. My feeling is that the problem should be NP-hard. Is there a suitable reduction from SAT? Or from normal 1-in-3-SAT? Or perhaps some sort of dichotomy theorem I don't know about that can be applied?


The answer to my question as stated is that the problem is indeed hard, because you can simply copy all clauses of a 1-in-3-SAT instance. I now insist that the clauses should not be repeated (we can efficiently preprocess an instance of SAT so that there are no repeat clauses after all)

  • $\begingroup$ Take a hard instance $I$ of 1-in-3-SAT, and add a copy of every individual clause. If a variable occurs $t$-times in $I$, then it occurs $2t$-times in the new instance with the copied clauses. $\endgroup$
    – Gamow
    Sep 11, 2019 at 11:05
  • $\begingroup$ @Gamow :facepalm: yes of course.. unfortunately I'm not sure that helps me in my research... perhaps I should insist that clauses aren't repeated? The clauses should be a set, not a multiset... I will edit the question I think. $\endgroup$ Sep 11, 2019 at 11:50

1 Answer 1


Theorem: The special case of 1-in-3-SAT where each variable appears an even number of times is NP-hard.

Proof: Consider an instance $I$ of 1-in-3-SAT, and let $a_1,\ldots,a_n$ be an enumeration of the variables in $I$. Assume that variables $a_1,\ldots,a_m$ occur an odd number of times, whereas $a_{m+1},\ldots,a_n$ occur an even number of times. Without loss of generality $m$ is an even number (and otherwise, add a new dummy clause with three newly created dummy variables).

From instance $I$, we create a new instance $I'$ of 1-in-3-SAT in which every variable occurs an even number of times. Furthermore, $I$ is satisfiable if and only if $I'$ is satisfiable:

  • Instance $I'$ contains all variables and all clauses of $I$.
  • For every variable $a_i$, instance $I'$ contains a (new) corresponding variable $b_i$.
  • Furthermore, $I'$ contains a (new) variable $c$.
  • For every clause $a_i,a_j,a_k$ in $I$, instance $I'$ contains a new clause $\lnot b_i, \lnot b_j,\lnot b_k$.
  • For $i=1,\ldots,m$, instance $I'$ contains a new clause $a_i,b_i,c$.

It is easy to check that every variable in $I'$ occurs in an even number of clauses. If $I'$ is satisfiable, then this induces a satisfying assignment for $I$.

Finally consider a satisfying assignment for $I$. Use truth values $b_i:=\lnot a_i$ for $1\le i\le n$ and $c:=$FALSE. The resulting assignment satisfies all clauses in $I'$.

  • $\begingroup$ This absolutely answers my question and I think it would be unfair to move the goalposts now, so I am happy to accept (I am interested in this question for more general reasons) However, the problem I am really interested in is the monotone (actually, positive) version of 1-in-3-SAT. If you have any thoughts please let me know. $\endgroup$ Sep 11, 2019 at 14:36

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.