## 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.