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.