*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