0
$\begingroup$

Resolution allows to generate new clauses for an existing set of clauses.

In many cases, the rule is simple:

{ a, b }     { -a, b }
----------------------
        { b }

But what if the clauses contain multiple literals suitable for resolution?

{ a, b }     { -a, -b }
-----------------------
        { ? }

If we choose a, then the result should be { b, -b } by definition. Is this correct?

If it is, what does this imply? I would assume { b, -b } to always be true as it means $b \lor \lnot b$ which is a tautology. Is this correct, and if it is not, what else does the result imply?

$\endgroup$
  • $\begingroup$ In the second pair of clauses answer is trivially $(a\oplus b)$. $\endgroup$ – rus9384 Aug 12 '17 at 10:40
  • $\begingroup$ @rus9384 The second pair of clauses was just an example, it can be arbitrarily complex, the only important assumption is that there are two variables of which there are different literals in the clauses. $\endgroup$ – just.kidding Aug 12 '17 at 10:49
  • $\begingroup$ I don't think that an answer would be that simple. That's why SAT is NP-complete. $\endgroup$ – rus9384 Aug 12 '17 at 11:13
  • $\begingroup$ You can check that the assumption $a\oplus b$ implies no clause other than the trivial one. $\endgroup$ – Yuval Filmus Aug 12 '17 at 12:05
  • $\begingroup$ If you have a clause with more than one negative literal you can apply the hyperresolution rule with the corresponding number of clauses containing positive literals. $\endgroup$ – Dmitri Chubarov Aug 14 '17 at 2:14

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.