Info
Experimental results
Hardware configuration used for all benchmarks: Core 2 Duo, 3 GB RAM
Results of CNF->DNF conversion
This set of benchmarks shows the times of conversion from CNF to DNF. CNF is obtained by negating the original input PLA file. The whole operation corresponds to getting off-set from on-set.
| benchmark | time [s] |
|---|---|
| ibm.pla | 1.231 |
| soar.pla | 5.357 |
| ti.pla | 44.959 |
| ex4.pla | 29.648 |
| ex1010.pla | 63.903 |
| test3.pla | 138.154 |
| pdc.pla | 206.596 |
| x7dn.pla | 553.682 |
| test2.pla | 916.021 |
| xparc.pla | 1263.380 |
Results of collapsing
This set of benchmarks shows the results of collapsing with comparison to MVSIS. The form for testing is obtained the same way as in the previous test by negating the original PLA file.
| time [s] | terms [-] | literals [-] | ||||
|---|---|---|---|---|---|---|
| benchmark | BoolTool | MVSIS | BoolTool | MVSIS | BoolTool | MVSIS |
| b12 | 0,155 | 0,33 | 42 | 34 | 132 | - |
| cordic | 318,546 | 3,19 | 1757 | 1191 | 27284 | - |
| cps | 5,566 | 1,23 | 4810 | 1870 | 21900 | - |
| duke2 | 2,883 | 0,37 | 2330 | 452 | 10611 | - |
| ex4 | 29,580 | 0,78 | 579 | 334 | 3465 | - |
| ex1010 | 64,530 | 2,62 | 11196 | 1415 | 70817 | - |
| misex2 | 0,065 | 0,08 | 286 | 146 | 503 | - |
| misex3c | 11,577 | 0,34 | 2502 | 508 | 15174 | - |
| pdc | 204,837 | 30,26 | 2694 | 897 | 11869 | - |
| rd84 | 1,661 | 0,53 | 482 | 239 | 3344 | - |
| spla | 197,931 | 32,27 | 1900 | 855 | 6744 | - |
Results of SAT solving
This table shows results of SAT solving with comparison to BDDCUDD, which uses binary decision diagrams to solve the problem. Number of solutions found denotes the number of minterms in result.
| time [s] | Terms [-] | |||
|---|---|---|---|---|
| benchmark | BoolTool | BDDCUDD | BoolTool | BDDCUDD |
| uf20-0500.cnf | 4,162 | 0,780 | 3 | 2 |
| uf20-0501.cnf | 2,712 | 0,733 | 19 | 1 |
| uf20-0502.cnf | 2,584 | 0,749 | 52 | 4 |
| uf20-0503.cnf | 3,338 | 0,733 | 16 | 4 |
| uf20-0504.cnf | 2,408 | 0,718 | 1 | 1 |
| uf20-0505.cnf | 1,799 | 0,717 | 3 | 2 |
| uf20-0506.cnf | 4,335 | 0,733 | 16 | 1 |
| uf20-0507.cnf | 3,290 | 0,734 | 64 | 4 |
| uf20-0508.cnf | 2,544 | 0,733 | 5 | 1 |
| uf20-0509.cnf | 1,140 | 0,733 | 4 | 1 |
| uf20-0510.cnf | 3,077 | 0,733 | 17 | 2 |
| uf20-0511.cnf | 1,717 | 0,718 | 4 | 2 |