# SAT for clauses of the form "At most m out of n are false"

Recall some terminology: Let $$\mathsf P$$ be a finite set of propositional atoms, and let $$\Phi$$ be a proposition over $$P$$ that is generated from $$\top$$, $$\bot$$, $$\neg$$, $$\wedge$$, and $$\vee$$. Then:

• A satisfying assignment for $$\Phi$$ is a function $$\varsigma:\mathsf P\to\{\bot,\top\}$$ such that $$\varsigma\vDash\Phi$$ holds with the usual rules for propositional validity. Intuitively: we replace every $$p\in \mathsf P$$ with $$\varsigma(p)$$ in $$\Phi$$, and reduce using truth-tables.
• Write AllSAT for the computational problem of, given $$\Phi$$, finding all of its satisfying assignments.

Question: What is known about AllSAT in the special case that $$\Phi$$ encodes a set of clauses, one for each $$p\in \mathsf P$$, each having the form

"$$p$$ is true if at most $$n_p\geq 0$$ of the elements from $$W_p\subseteq\mathsf P$$ are false"?

I am particularly interested in references for:

1. Mathematical characterisations of the solutions.
2. Algorithms for computing these solutions.
3. The complexity of these algorithms.

Note: We usually further constrain $$\Phi$$ such that $$n_p < \#W_p /2$$ for every $$p$$.

Example: Take $$\mathsf P=\{a, b, c\}$$ and take $$\Phi = ((b \vee c) \rightarrow a) \wedge ((c \wedge a \wedge b) \rightarrow b) \wedge ((a\vee b\vee c) \rightarrow c) .$$ This $$\Phi$$ encodes three clauses:

1. $$a$$ is true if at most one element from $$\{b,c\}$$ is false; so $$n_a=1$$ and $$W_a=\{b,c\}$$.
2. $$b$$ is true if at most zero elements from $$\{a,b,c\}$$ are false; so $$n_b=0$$ and $$W_b=\{a,b,c\}$$.
3. $$c$$ is true if at most two elements from $$\{a,b,c\}$$ are false; so $$n_c=2$$ and $$W_c=\{a,b,c\}$$.

Thank you.

• Circuits of the form $(a\land b)\rightarrow c$ are encoding 3 SAT clauses $(\overline a\lor\overline b\lor c)$. Commented Dec 11, 2023 at 20:11
• You can check NP-hardness (of satisfiability) using Schaefer's dichotomy theorem. Commented Dec 11, 2023 at 20:53