Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

how do I find the resolvent of this formula?

$(A \vee C) \wedge ( \neg A \vee B) \wedge C$

Is it as easy as taking every clause with the same statements?

$(A \vee C)$ and $( \neg A \vee B)$ and put out the contradiction (in this case $A$ and $\neg A$)

Could you recommend me some source for resolution method except Wikipedia, because there are too easy examples?

share|cite|improve this question
Try Googling "resolution proof system". – Yuval Filmus Dec 5 '10 at 23:52
The version of resolution I'm aware of is a proof system for refuting a conjunction of clauses, but your formula is not contradictory. In fact, it is a 2-SAT formula and so there's a simple efficient algorithm for deciding whether it's satisfiable. – Yuval Filmus Dec 5 '10 at 23:53
up vote 1 down vote accepted

Yes, you're going to find clauses with contradictory literals and apply the resolution rule to those. So you're going to resolve the first two clauses in your example.

Here are a couple of pages you can look at:

share|cite|improve this answer
Thanks for usefull sources at MIT and Stanford... I can't believe, our university is keeping similar materials only for their students and teachers even it's not as good (self-explaining) as materials from MIT/Stanford :D – Radek Simko Dec 6 '10 at 9:02

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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