Prev: what replaced usenet news?
Next: solutions book
From: RussellE on 21 Jul 2010 03:25 Super resolution is a fast method for deriving binary and unit resolvent clauses from a 3SAT instance. Resolution is a well known method for deriving inferences. http://en.wikipedia.org/wiki/Resolution_(logic) (a+b) r (~a+c) > (b+c) The resolvent of two binary clauses is always a binary or unit clause. Extended binary resolution (EBR) takes a set of binary and unit clauses and performs resolution on the set until no new clauses can be added. EBR can derive unit clauses and/or contradictions as well as binary clauses. Super resolution combines EBR and unit clause propogation (UCP). http://en.wikipedia.org/wiki/Unit_clause Super Resolution: 1) Choose a variable, X. 2) Add the unit clause (x) to the 3SAT instance. 3) Perform UCP on the instance. 4) Let S1 be the set of all binary and unit clauses in the reduced instance. 5) Perform EBR on S1. 6) If a contradiction is derived then X must be false. Add (~x) to the instance and restart. 7) If a unit clauses is derived, add this unit clause to the reduced 3SAT instance, perform UCP on the instance, add any new binary or unit clauses to S1, and go to step 5. Perform the steps above again assuming X is false. 8) Add the unit clause (~x) to the original 3SAT instance. 9) Perform UCP on the instance. 10) Let S2 be the set of all binary and unit clauses in the reduced instance. 11) Perform EBR on S2. 12) If a contradiction is derived then X must be true. Add (x) to the instance and restart. 13) If a unit clauses is derived, add the unit clause to the reduced 3SAT instance, perform UCP on the instance, add any new binary or unit clauses to S2, and go to step 11. 14) Let S3 be the set of binary and unit clauses derived from S1 and S2 using the rules given below. 15) Perform EBR on S3. 16) If a contradiction is derived then the instance is unsatisfiable. 17) If a unit clauses is derived, add the unit clause to the reduced 3SAT instance, perform UCP on the instance, add any new binary or unit clauses to S3, and go to step 15. 18) Add any clauses in S3 to the instance as binary and unit resolvent clauses. Rules for deriving resolvent clauses from S1 and S2: 1) Any clause in both S1 and S2 is a resolvent. 2) If (x) is a unit clause in S1/S2 then any clause in S2/S1 containing x is a resolvent. 3) If (x) in S1 and (y) in S2 then (x+y) is a resolvent. It is important to include the unit clauses of the variable being resolved in S1 and S2. The variable being resolved may appear in a binary clause in S3 because of rule (3). An example: (a+b+c)(~a+~d+~e)(a+b+~d)(~a+c+~e) (~b+~c+d)(~c+d+e)(~b+~c+e)(c+~d+~e) (~a+b+e)(~c+d+~e)(~b+d+e)(a+~c+e) Resolve on variable A. Add (a) to the instance. S1 = (a)(b+e)(c+~e)(~d+~e) Perform EBR on S1. (~d+~e) r (b+e) > (b+~d) (c+~e) r (b+e) > (b+c) No more clauses can be derived. S1 = (a)(b+c)(b+~d)(b+e)(c+~e)(~d+~e) Add (~a) to the original instance. S2 = (~a)(b+c)(b+~d)(~c+e) (b+c) r (~c+e) > (b+e) S1 = (a)(b+c)(b+~d)(b+e)(c+~e)(~d+~e) S2 = (~a)(b+c)(b+~d)(b+e)(~c+e) Create S3 using the rules above. S3 = (b+c)(b+~d)(b+e) Notice that regular resolution on variable A would not derive these binary clauses. Normal resolution on variable A would derive: (b+c+~e)(b+c+e)(b+~c+e)(b+~d+e)(b+c+~d+~e) Add the resolvent clauses in S3 to the instance and subsume clauses. (b+c)(b+~d)(b+e) (~a+~d+~e)(~a+c+~e)(~b+~c+d)(~c+d+e)(~b+~c+e) (c+~d+~e)(~c+d+~e)(~b+d+e)(a+~c+e) Resolve on B. S1 = (b)(~c+d)(~c+e)(d+e) No more clauses can be resolved. After adding (~b) to the instance, UCP will derive a contradiction. Variable B must be true. New instance after subsumption. (b)(~a+~d+~e)(~a+c+~e)(~c+d)(~c+d+e) (~c+e)(c+~d+~e)(~c+d+~e)(d+e)(a+~c+e) Resolve on variable C. Add (c) to instance. After UCP: S1 = (c)(b)(d)(e)(~a) = ~abcde This is a satisfying assignment. (a+B+C)(~A+~d+~e)(a+B+~d)(~A+C+~e) (~b+~c+D)(~c+D+E)(~b+~c+E)(C+~d+~e) (~A+b+E)(~c+D+~e)(~b+D+E)(a+~c+E) Super resolution shows the expression above is equivalent to: (~a)(b)(~c+d)(~c+e)(d+e)(c+~d+~e) Russell  2 many 2 count
From: RussellE on 23 Jul 2010 01:38 > (a+B+C)(~A+~d+~e)(a+B+~d)(~A+C+~e) > (~b+~c+D)(~c+D+E)(~b+~c+E)(C+~d+~e) > (~A+b+E)(~c+D+~e)(~b+D+E)(a+~c+E) > > Super resolution shows the expression > above is equivalent to: > > (~a)(b)(~c+d)(~c+e)(d+e)(c+~d+~e) (a+b+c)(~a+~d+~e)(a+b+~d)(~a+c+~e) (~b+~c+d)(~c+d+e)(~b+~c+e)(c+~d+~e) (~a+b+e)(~c+d+~e)(~b+d+e)(a+~c+e) = (~a+~c)(~a+d)(~a+~e)(b)(~c+d)(~c+e)(c+~d+~e)(d+e)

Pages: 1 Prev: what replaced usenet news? Next: solutions book 