Last page LERIA Faculty of Sciences University of Angers
Version française

Transformation of ksat instances into 3sat instances


Many SAT algorithms must have 3sat instances as input. It is easy to obtain random 3sat instances whereas for structured 3sat instances, it is very hard. The aim of the ksat_3sat algorithm is to transform a ksat instance into a 3sat instance preserving the minimum number of false clauses for unsatisfiable instances. The main features of ksat_3sat can be summarized as follows:

ksat clauses 3sat clauses
(a) (a v X1 v X2) ^
(a v -X1 v X2) ^
(a v X1 v -X2) ^
(a v -X1 v -X2)
(a v b) (a v b v X1) ^
(a v b v -X1)
(a v b v c) (a v b v c)
(a v b v c v d v ... v y v z) (a v b v X1) ^
( -X1 v c v X2) ^
(-X2 v d v X3) ^
... (-Xn v y z)

Download: ksat_3sat.c (9Ko) (gcc -O2 ksat_3sat.c -o ksat_3sat)