The resolvent of the set of clauses (A ∨ B, ~A ∨ D, C ∨ ~B) is
2014
The resolvent of the set of clauses
(A ∨ B, ~A ∨ D, C ∨ ~B) is
- A.
A ∨ B
- B.
C ∨ D
- C.
A ∨ C
- D.
A ∨ D
Attempted by 214 students.
Show answer & explanation
Correct answer: B
Final resolvent: C ∨ D
Reasoning:
Resolve A ∨ B and ¬A ∨ D on A: complementary literals A and ¬A cancel, producing B ∨ D.
Resolve B ∨ D and C ∨ ¬B on B: complementary literals B and ¬B cancel, producing C ∨ D.
Therefore the resolvent of the set {A ∨ B, ¬A ∨ D, C ∨ ¬B} is C ∨ D.
Note: Resolution eliminates a pair of complementary literals (like A and ¬A) and combines the remaining literals from the parent clauses.