Is the problem of deciding whether a SAT instance, where at most one clause is false (that is, any given variable assignment will either lead to all clauses being true, or all but one), is satisfiable solvable in polynomial time?
-
$\begingroup$ @Evil None of the restricted versions on Wikiepdia seemed very similar to my problem, so I couldn't find out anything there. I've also tried to encode a simple 3CNF problem in this format, but I couldn't come up with anything (even though I'm still trying). $\endgroup$– user110726Commented Oct 15, 2019 at 0:33
-
$\begingroup$ What is the input and what is the output? I can image two possible interpretations: 1. The input is a SAT instance, and the output is a boolean value indicating whether this SAT instance satisfies at most one clause is false. 2. The input is a SAT instance where at most one clause is false, and the output is a boolean value indicating whether this instance is satisfiable (i.e. whether there exists a variable assignment making all clauses true). $\endgroup$– xskxzrCommented Oct 15, 2019 at 2:58
-
$\begingroup$ @xskxzr Your second option is what I had in mind. Thank you! $\endgroup$– user110726Commented Oct 15, 2019 at 3:16
1 Answer
Given a CNF with $n$ variables and $m$ clauses, we denote by $A_i$ the set of truth assignments that do not satisfy clause $i$. Then the number of satisfiable assignments is $$2^n-\left|\bigcup_{i=1}^m A_i\right|.$$ Since each assignment makes at most one clause false, $A_i$ and $A_j$ are disjoint for $i\neq j$. Also note $|A_i|=2^{n-n_i}$ where $n_i$ is the number of variables in clause $i$. Hence, the number of satisfiable assignments is exactly $2^n-\sum_{i=1}^m 2^{n-n_i}$ (this result is also given as lemma 2 in [1]).
So we can decide whether the CNF is satisfiable by checking whether $2^n-\sum_{i=1}^m 2^{n-n_i}>0$, which can be done in polynomial time.
[1] Nishimura, N., Ragde, P., & Szeider, S. (2007). Solving #SAT using vertex covers. Acta Informatica, 44(7-8), 509-523.