kcnfs :
IJCAI-01 paper : "A backbone-search heuristic for efficient solving of hard 3-SAT formulae"
 
The source code of the solver : kcnfs(Complete solver winner of SAT'03 and SAT'04 competition in the category Random Benchmarks) (in a ZIP archive, 46Ko).
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