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