Wednesday, February 16, 2011

XOR gates

I finally came about to extract XOR gates from cnf formulas. First thing I wanted to check how much of the literals come from XOR clauses on a few instances from SAT09 competition. The table below suggest that handing XOR gates is promising.

Test name
Literals in XOR gates
Literals in formula
Percent
aprove09/AProVE09-24.cnf
366734
760056
48,25
aprove09/AProVE09-22.cnf
65416
138984
47,07
aprove09/AProVE09-25.cnf
205992
447524
46,03
aprove09/AProVE09-13.cnf
38150
94732
40,27
aprove09/AProVE09-19.cnf
162024
410098
39,51
aprove09/AProVE09-12.cnf
145400
371302
39,16
aprove09/AProVE09-05.cnf
68630
177140
38,74
aprove09/AProVE09-06.cnf
361904
942686
38,39
aprove09/AProVE09-08.cnf
39716
103498
38,37
aprove09/AProVE09-07.cnf
39716
103528
38,36
aprove09/AProVE09-11.cnf
109548
285640
38,35
aprove09/AProVE09-10.cnf
312994
884978
35,37
aprove09/AProVE09-17.cnf
133408
383728
34,77
aprove09/AProVE09-15.cnf
372164
1077424
34,54
aprove09/AProVE09-20.cnf
123232
385046
32,00
aprove09/AProVE09-03.cnf
46820
718720
6,51
aprove09/AProVE09-01.cnf
72476
1127880
6,43
aprove09/AProVE09-21.cnf
19180
305486
6,28

Update: I finished implemented xor-gates and fixed most of the bugs. The change required to change the way I store clauses. Until now clauses were stored as: a b c ... 0. Now they are stored as (length,type) a b c ..., where length is the length of the clause, type is OR/XOR/NXOR and (length, type) means that length and type encoded together as a single integer. The most basic solver is working now, but except for equivalent literals renaming other simplification algorithms are not functional. The graph below shows the impact of handling XOR-gates.


The benefits of handing xor gates are multiple. First formulas are much shorter because xor gates requires exponential number of CNF clauses. This means that it is less costly to move instances around. Second the branch heuristic is less fooled by almost identical clauses. Third most other algorithms can safely ignore xor clauses to a bonus speedup. In conclusion I'm glad I spent the last few days refactoring STRUCTure.

Update: When I enabled all reasoning algorithms (e.g. hyper binary resolution, sub-summing, etc.) the performance difference changed dramatically. It leads me to believe that initial evaluations contained a bug. The graph below shoes the performance of STRUCTure behaves with and without xor gates. It seems that handling xor gates helps on a few instances, but the instances from AProvE class are better of without them.



No comments:

Post a Comment