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

 

 
 
 
 
 
 
 

qgs :
CP-2001 paper : "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 solver.
To use qg2s, type : qg2s size
size is the order of the QG2 existence problem to be solved.
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 web page from the CSPLIB website.

 
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, SATLIB, SatLive, CSPLIB, Lecture Note in Computer Science

Last updating : February, 25, 2003