COunting for Rank k formulas (COR v1.0) is implemented in Java.

The class files can be downloaded freely for evaluation from here (Copyright of its respective owners).

All tests have been conducted on Red Hat Linux 9.0 Pentium 4, 2.0 GHz processor, and 1 GB of memory Java SDK1.4.2_03.

To run COR, simply type the command: java -Xmx512m COCOR <input_DIMACS_CNF_file> > <output_results>

COunting for Rank k formulas (COR v1.0) is compared against some of state-of-the-art SAT solvers, namely SATO, GRASP, and zChaff.

We start our comparison with GRASP. We observe that the bigger the input data, the larger the gap between COR and GRASP will be. Moreover, if we would know in advance that the input clausal formula F belongs already to the coupled-regular class, then there is no need to solve the membership problem for F. If this is the case, then COR is 100 to 300 faster than GRASP.

Regarding the comparison with SATO and zChaff, we shall refer only to the execution times of COR spend for determinant computation (by skiping the membership problem). So, the determinant computation of COR outperforms SATO in 6 out of 10 cases, and zChaff in all cases with a order of magnitude of 18 to 26.

It must be noted that while our COR solver is a first prototype solver that we have built, the other SAT solvers are state-of-art solvers that have been subjected to performance engineering. Our approach is based on the more general #SAT problem.

1. The input test750-1800DIMACS.txt written in DIMACS format:
   1. test750-1800DIMACSoutputSATO.txt
   2. test750-1800DIMACSGRASP.txt
   3. test750-1800DIMACSoutputZCHAFF.txt
   4. test750-1800DIMACSCOCOR.txt
2. The input test900-2000DIMACS.txt written in DIMACS format:
   1. test900-2000DIMACSoutputSATO.txt
   2. test900-2000DIMACSoutputGRASP.txt
   3. test900-2000DIMACSoutputZCHAFF.txt
   4. test900-2000DIMACSoutputCOCOR.txt
3. The input test1000-2200DIMACS.txt written in DIMACS format:
   1. test1000-2200DIMACSoutputSATO.txt
   2. test1000-2200DIMACSoutputGRASP.txt
   3. test1000-2200DIMACSoutputZCHAFF.txt
   4. test1000-2200DIMACSoutputCOCOR.txt
4. The input test1100-2400DIMACS.txt written in DIMACS format:
   1. test1100-2400DIMACSoutputSATO.txt
   2. test1100-2400DIMACSoutputGRASP.txt
   3. test1100-2400DIMACSoutputZCHAFF.txt
   4. test1100-2400DIMACSoutputCOCOR.txt
5. The input test1200-2600DIMACS.txt written in DIMACS format:
   1. test1200-2600DIMACSoutputSATO.txt
   2. test1200-2600DIMACSoutputGRASP.txt
   3. test1200-2600DIMACSoutputZCHAFF.txt
   4. test1200-2600DIMACSoutputCOCOR.txt
6. The input test1300-2900DIMACS.txt written in DIMACS format:
   1. test1300-2900DIMACSoutputSATO.txt
   2. test1300-2900DIMACSoutputGRASP.txt
   3. test1300-2900DIMACSoutputZCHAFF.txt
   4. test1300-2900DIMACSoutputCOCOR.txt
7. The input test1500-3500DIMACS.txt written in DIMACS format:
   1. test1500-3500DIMACSoutputSATO.txt
   2. test1500-3500DIMACSoutputGRASP.txt
   3. test1500-3500DIMACSoutputZCHAFF.txt
   4. test1500-3500DIMACSoutputCOCOR.txt
8. The input test1750-4000DIMACS.txt written in DIMACS format:
   1. test1750-4000DIMACSoutputSATO.txt
   2. test1750-4000DIMACSoutputGRASP.txt
   3. test1750-4000DIMACSoutputZCHAFF.txt
   4. test1750-4000DIMACSoutputCOCOR.txt
9. The input test2000-5000DIMACS.txt written in DIMACS format:
   1. test2000-5000DIMACSoutputSATO.txt
   2. test2000-5000DIMACSoutputGRASP.txt
   3. test2000-5000DIMACSoutputZCHAFF.txt
   4. test2000-5000DIMACSoutputCOCOR.txt
10. The input test2500-6000DIMACS.txt written in DIMACS format:
    1. test2500-6000DIMACSoutputSATO.txt
    2. test2500-6000DIMACSoutputGRASP.txt
    3. test2500-6000DIMACSoutputZCHAFF.txt
    4. test2500-6000DIMACSoutputCOCOR.txt
11. The input test3000-7000DIMACS.txt written in DIMACS format:
    1. test3000-7000DIMACSoutputSATO.txt
    2. test3000-7000DIMACSoutputGRASP.txt
    3. test3000-7000DIMACSoutputZCHAFF.txt
    4. test3000-7000DIMACSoutputCOCOR.txt