SAT 2003 Competitor Toolbox

Last updated: January 23, 2003.

This web page is intented to provide useful tools and information for competitors of the forthcoming SAT 2003 competition.

Those programs are provided in order to help competitors to check the competition input/output requirements and to allow people to take a look at the programs used during the competition process. Those programs are provided under the GNU General Public Licence.
Please feel free to send comments about those programs to SATcompetition@satlive.org.

The compile those files on most unix boxes:

# make <filename_without_extension>

You can get all thoses programs in the archive.

Benchmarks submitters

Counter.c: this program checks that benchmarks comply with the competition input requirements.

Input: benchmark file name.
Output: the number of literals in the benchmark if the instance complies with the input format, else an error message indicating where a problem was detected.

To run it:

# counter <instance_file_name>

Examples:

# ./counter aim/aim-50-1_6-no-1.cnf 
Clause 63, variable 44:
error 5001: 
A variable occurs twice in a clause

In that benchmark, the clause 63 is 4 44 -44 0, a tautological clause.
The same message would be displayed for the clause 4 44 44 0.

# ./counter aim/aim-50-1_6-no-2.cnf 
240

There are 240 literals in that benchmark.

Solvers submitters

Verifier.c: this program is used to check that the solvers comply with the competition output requirements.

Input: the solver output on STDIN and the instance filename for checking satisfiability certificate.

Output: an explicit message concerning the solver output.

To run it:

# <yoursolver> <theinstancename> | verifier <theinstancename>

Examples:

#./limmat-1.3/limmat aim/aim-50-1_6-yes1-1.cnf | ./verifier aim/aim-50-1_6-yes1-1.cnf

c~~ verifier: OK: SATISFIABLE claimed, and implicant is correct

# ./limmat-1.3/limmat aim/aim-50-1_6-no-1.cnf | ./verifier aim/aim-50-1_6-no-1.cnf

c~~ verifier: OK: UNSATISFIABLE claimed, no model provided by solver

Misc

Reorder.c: this program is used to shuffle clauses and to rename literals in the benchmarks submitted for the competition.

That program is not ANSI C compliant (it uses long long int). Use g++ for instance to compile it:

# g++ -o reorder reorder.c

Input: A benchmark file name and a random seed.
Output: the shuffled instance is displayed on STDOUT.

Example:

 ./reorder /home-local/benchs/bw_large.a.cnf 123

GenAlea.c: this program was used to generate some random 3SAT instances for the SAT2002 competition (uniform 3SAT random instances).
The files my_random.h and my_random.c are needed to compile it.