IJCAI-01 paper : "A
backbone-search heuristic for efficient solving of hard 3-SAT formulae"
The source code of the solver : kcnfs (2004 competition version)(Complete solver winner of SAT'03, SAT'04 and SAT'05 competitions in the category Random Benchmarks)
(in a ZIP archive, 46Ko).
The description of the solver is here.
The last version of kcnfs (submitted to the SAT'07 competition) is here: kcnfs-2006
The SMP version of kcnfs (submitted to the SAT'07 competition) will be available here: kcnfs-smp
kcnfs is a generalization of cnfs (and his "h" heuristic) for random k-SAT formulae. This version ends the first part of this project.
To compile kcnfs*, just type 'make' in the kcnfs* directory
To use kcnfs*, type : kcnfs* yourfile.cnf
yourfile.cnf must contain a dimacs formula in DIMACS Format. kcnfs is built to solve random k-SAT formulae.
: "The non-existence of (3,1,2)-Conjugate Orthogonal
Idempotent Latin Square of Order 10"
A static binary of qg2s
(in a ZIP archive, 492Ko).
qg2s is a QG2 quasigroup existence problem
To use qg2s, type : qg2s size
size is the order of the QG2 existence problem to
for example type qg2s 10 to solve QG2(10) (answer
140 days later with one Athlon-equipped PC!).
The 16085 RC configurations to prove
the non-existence of the QG2(10) (650Ko).
The open quasigroup existence problems can be seen at this
page from the CSPLIB
The binaries cnfs and qgs were
generated with a PC workstation under a Linux
OS with the gcc compiler and "-O3 -funroll-loops" options.
Contact Authors : Olivier
Dubois and Gilles Dequen.
Links : DIMACS,
Note in Computer Science
Last updating : February, 25, 2003