2
$\begingroup$

I know that resolution is refutation complete, but what can we conclude if a resolution procedure leads to a situation with no more chance to operate the resolution?

Given a propositional formula which we want to check its satisfiability,

( a + b ) ( ¬a + c )

after one resolution the formula become

( a + b ) ( ¬a + c ) ( b + c )

what can we conclude at this point?

$\endgroup$
  • 2
    $\begingroup$ I'm afraid you can't delete clauses you've used in a resolution if you want to keep completeness. In particular, what you get is (in your notation) $(a+b)(\neg a + c)(b + c)$, rather than just $(b + c)$. $\endgroup$ – cody Sep 10 '15 at 14:46
  • 1
    $\begingroup$ @cody It's actually valid in this case. In general if you resolve all the clauses with a given positive variable against all clauses with that variable negated, you can keep the clauses resolution produced and discard the original clauses you used and maintain equisatisfiability. Sometimes you can even do this without increasing the overall number of clauses, which is why MiniSat uses to trick to eliminate variables in some situations. $\endgroup$ – Kyle Jones Sep 12 '15 at 0:53
3
$\begingroup$

By definition if a proof system is refutation-complete then once you've applied it to the maximum extent and not found a contradiction, you have proven that there are no refutations, i.e. the formula is satisfiable. To find a satisfying assignment, add a unit clause that asserts a value for one of the variables, e.g. $(a)$, and use resolution on the resulting formula. If you find a refutation (produce an empty clause), then replace the asserting clause with its negation e.g. $(\lnot{a})$, otherwise leave the original assertion in the formula. Repeat the procedure with a different variable. Eventually you'll have successfully asserted values for all the variables and found a satisfying assignment.

$\endgroup$
  • $\begingroup$ You wouldn't even need backtracking - if a variable cannot take a value, the saturated formula should contain the relevant unit clause, telling you which value to pick. $\endgroup$ – Klaus Draeger Sep 10 '15 at 15:27
  • $\begingroup$ thanks for answering my question, now I'm wondering how to prove the refutation-completeness of resolution? $\endgroup$ – chen Sep 11 '15 at 7:10
  • $\begingroup$ @chen, Please don't use comments to ask new questions. Comments on answers should be used only to suggest improvements or clarifications to answers. In general, if you have a new question, then you should post it separately as a new question. As always make sure to follow all our standard expectations for questions, including doing research before asking, showing us what research you've done, etc. (In this case I would expect that to have been proved in the literature or covered in textbooks.) This site isn't a discussion forum. $\endgroup$ – D.W. Sep 12 '15 at 0:32

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.