Page précédente LERIA Faculté des Sciences Université d'Angers
English version

Transformation d'un problème ksat en problème 3sat


Beaucoup d'algorithmes travaillant sur le problème SAT ne fonctionnent qu'avec des instances 3sat. Il est très facile de trouver ou de générer des instances 3sat aléatoires mais pour les instances 3sat structurées, c'est beaucoup plus dur. L'objectif de l'algorithme ksat_3sat est donc de proposer une transformation permettant de réduire une instance ksat en une instance 3sat tout en concervant le nombre de clauses fausses minimum pour une instance non satisfiable. Le principe de ksat_3sat est le suivant :

clauses ksat clauses 3sat
(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 v z)

Téléchargement de ksat_3sat.c (9Ko) (gcc -O2 ksat_3sat.c -o ksat_3sat)