# 4-SAT but two literals per clause must be true

I'm trying to show that a modified 4-SAT in which at least two literals per clause must be true is NP-complete. I'll call it $$4_2$$-SAT. I understand the reduction from 3-SAT to 4-SAT, and I know why $$4_2$$-SAT is in the class NP, so I'm just struggling on the reduction from 4-SAT to $$4_2$$-SAT (or any other way to show that $$4_2$$-SAT is NP-hard).

My initial attempt was to try and convert an instance of 4-SAT

$$(a \vee b \vee c \vee d)$$

into an instance of $$4_2$$-SAT by spelling out the requirement as

$$(a \wedge b) \vee (a \wedge c) \vee (a \wedge d) \vee (b \wedge c) \vee (b \wedge d) \vee (c \wedge d)$$

and then convert to CNF and add extra literals if needed to get to four per clause, but this conversion does not preserve the answer of the original 4-SAT clause.

Any hints or help as to how to convert an instance of 4-SAT into $$4_2$$-SAT would be appreciated.

• I'm not sure that this will help, but one way to do this is to go through all possible combinations of assigning two literals true. i.e. let $T(x_1,x_2) = (x_1 \land x_2)$. Then your clause becomes $T(a,b) \lor T(a,c) \lor T(a,d) \lor T(b,c) \lor T(b,d) \lor T(c,d)$. You should be able to reduce 6-SAT to this by expanding all 2-tuple combinations into 6-tuples. For instance, $(a \land b) \lor (c \land d)$ becomes $(a \lor c) \land (a \lor d) \land (b \lor c) \land (b \lor d)$. To see this more clear, repalce $\lor$ symbols with $+$ and $\land$ symbols with $*$. Commented Apr 24, 2022 at 4:11

Schaefer's dichotomy theorem settles the complexity of your problem.

Consider a constraint satisfaction problem (CSP) in which there is a finite collections $$S$$ of types of constraints over Boolean variables, and an instance is a conjunction of constraints of the form $$R(\ell_1,\ldots,\ell_k)$$, where $$R \in S$$ is a $$k$$-ary constraint and $$\ell_1,\ldots,\ell_k$$ are arbitrary literals; the goal is to determine whether the instance is satisfiable, that is, whether there is a truth assignment to the variables which satisfies all constraints. For example, 3SAT is the case in which $$S$$ consists of the constraint $$x \lor y \lor z$$, and in your problem $$S$$ consists of the constraint $$R_{4,2}$$ "at least two out of $$x,y,z,w$$ are true".

• If each $$R \in S$$ is equivalent to a 2CNF, then the CSP can be solved in polynomial time by reduction to 2SAT. This condition holds iff the set of satisfying assignments of each $$R \in S$$ is closed under ternary majority: if $$R$$ is a $$k$$-ary constraint, then for any three satisfying assignments $$a,b,c$$, the assignment $$\operatorname{maj}(a_1,b_1,c_1),\ldots,\operatorname{maj}(a_k,b_k,c_k)$$ also satisfies $$R$$.

• If each $$R \in S$$ is equivalent to a conjunction of linear equations, then the CSP can be solved in polynomial time using Gaussian elimination. This condition holds iff the set of satisfying assignments of each $$R \in S$$ is closed under ternary XOR: if $$R$$ is a $$k$$-ary constraint, then for any three satisfying assignments $$a,b,c$$, the assignment $$a_1 \oplus b_1 \oplus c_1,\ldots,a_k \oplus b_k \oplus c_k$$ also satisfies $$R$$.

• In all other cases, the CSP is NP-complete.

In your case, you can check that $$R_{4,2}$$ is not closed under the two operations above:

• The truth assignments $$(1,1,0,0),(1,0,1,0),(1,0,0,1)$$ satisfy $$R_{4,2}$$, but their majority $$(1,0,0,0)$$ doesn't.
• The truth assignments $$(1,1,0,0),(0,0,1,1),(1,1,1,1)$$ satisfy $$R_{4,2}$$, but their XOR $$(0,0,0,0)$$ doesn't.

The proof of Schaefer's theorem gives a gadget reduction from either 3SAT or 3NAE-SAT to any NP-complete CSP (3NAE-SAT only occurs if the set of solutions of each $$R$$ is closed under complementation, which is not the case for $$R_{4,2}$$), but this reduction is rather verbose.
In your case, here is a simple reduction from 3SAT to your problem: replace each clause $$a \lor b \lor c$$ with the constraint $$R_{4,2}(a,b,c,d)$$, where $$d$$ is a new variable common to all clauses (alternatively, you can make $$d$$ a new variable for each clause, which would make it a gadget reduction in the sense of Schaefer's theorem).