# What can be concluded from a full application of resolution?

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?

• 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)$. – cody Sep 10 '15 at 14:46
• @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. – Kyle Jones Sep 12 '15 at 0:53

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.