Utilisation de la Propagation de Contraintes Booléennes pour la Production de Sous-Clauses

Overview & Synopsis

La propagation de contraintes booléennes (BCP) est la technique la plus utile et la plus utilisÈe dans les solveurs SAT. Dans cet article, nous proposons une autre utilisation de cette technique dans le but de réduire, en termes de nombre de clauses et de longueur des clauses, la formule initiale. En considérant le graphe d'implications généré par la procédure BCP comme un arbre de résolution, nous pouvons déduire des sous-clauses de la formule initiale. Nous montrons ensuite, comment une telle extension peut être implémentée dans les solveurs actuels où la procédure BCP est utilisée à chaque noeud de l'arbre de recherche. Nous présentons une première implémentation de cette approche dans le cadre d'un pré-traitement pour le solveur Zchaff. Pour finir, des résultats comparatifs préliminaires montrant les points forts et les faiblesses de l'approche sont fournis sur certaines classes d'instances de nature structurées.