0
$\begingroup$

Suppose we have a set of clauses $\Gamma$ that are disjunctions, so that the whole set can be viewed to represent a Boolean expression in CNF form. Then we can say $\Gamma$ entails the clause $C$ iff the set $\Gamma \cup \neg C$ is unsatisfiable. (Note that $\neg C$ is a set of unit clauses.)

For any such clause $C$, we can say that it is trivially entailed by $\Gamma$ if it meets one of the following conditions:

  1. Subsumption: There is some clause $A \in \Gamma$ and some arbitrary disjunction $B$ such that $C = A \lor B$
  2. Tautology: $C$ contains both a literal and its negation, and is true in every model

Otherwise, we say that $C$ is nontrivially entailed by $\Gamma$.

One procedure that can produce nontrivial clauses is resolution, where we take two clauses sharing exactly one literal that differs in sign between them, and generate the clause that is the disjunction of all other literals in the two clauses. For example, $(a \lor b \lor c)$ and $(\neg c \lor d \lor e)$ resolve to $(a \lor b \lor d \lor e)$.

My question: Can repeated use of the resolution operator produce every non-trivially entailed clause from $\Gamma$?

In other words, do there exist non-trivially entailed clauses that we cannot obtain by repeated use of resolution on $\Gamma$ and intermediate resolvents?

Formally speaking, this is equivalent to asking if the resolution operation, coupled with operations for subsumption and tautology, leads to a strongly complete formal system. This is a much stronger criterion than "refutation completeness," which resolution is known to have.

$\endgroup$
  • $\begingroup$ While $a \vee b$ is entailed by $a$, it cannot be obtained from $a$ by resolution. Do you want to impose any restrictions on which variables appear in the entailed clause? $\endgroup$ – Fabio Somenzi Aug 17 '17 at 3:57
  • $\begingroup$ That's one of the trivially entailed clauses I listed under subsumption. I'm only asking about nontrivially entailed clauses. $\endgroup$ – Mike Battaglia Aug 17 '17 at 3:57
  • 1
    $\begingroup$ Sorry, I rushed my comment. The answer is that by repeated resolution one obtains all prime implicates of the given CNF formula. See, for instance, Boolean Reasoning: The Logic of Boolean Equations by F. M. Brown. Hence, all clauses entailed by the formula are entailed by some clause generated by resolution. $\endgroup$ – Fabio Somenzi Aug 17 '17 at 4:07
  • $\begingroup$ Thanks, that's helpful! Had not seen the crossover since they use different terminology. $\endgroup$ – Mike Battaglia Aug 17 '17 at 4:28
  • $\begingroup$ Glad to be of help. It is also not difficult to produce a resolution proof that $\Gamma \wedge \neg C$ is unsatisfiable that is guaranteed to contain a clause $D$ that either is $C$ itself, or subsumes it. A proof-producing CDCL SAT solver would normally do just that. $D$ would also be returned as interpolant for $\Gamma \rightarrow C$. $\endgroup$ – Fabio Somenzi Aug 17 '17 at 5:12

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.