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”

  1. Set S 0 := S

  2. Suppose S i has already been constructed

  3. 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}

  4. If C is the empty clause, output “S is not satisfiable”; if S i+1 = S i , output “S is satisfiable”

  5. Otherwise, set i := i + 1 and go back to Step 2


Speaker notes:

Content Tools

Sources

There are currently no sources for this slide.