Prev: JSH: Some history
Next: Only two human-beings able to do a valid Indirect proof of Euclid Infinitude of Primes #4.02 Correcting Math
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: JSH: Some history
Next: Only two human-beings able to do a valid Indirect proof of Euclid Infinitude of Primes #4.02 Correcting Math