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.

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.