Current Slide
Small screen detected. You are viewing the mobile version of SlideWiki. If you wish to edit slides you will need to use a larger device.
Resolution (cont’)
-
Theorem : Resolvent C is satisfiable if and only if the parent clauses C 1 ,C 2 are simultaneously satisfiable
-
Resolution Algorithm:
Input : S – a set of clauses
Output : “S is satisfiable” or “S is not satisfiable”
-
Set S 0 := S
-
Suppose S i has already been constructed
-
To construct S i+1 , choose a pair of clashing literals and clauses C 1 ,C 2 in S (if there are any) and derive
C := Res( C 1 ,C 2 )
S i+1 := S i U {C}
-
If C is the empty clause, output “S is not satisfiable”; if S i+1 = S i , output “S is satisfiable”
-
Otherwise, set i := i + 1 and go back to Step 2
