AAAI Publications, Eighth Symposium on Abstraction, Reformulation, and Approximation

Font Size: 
A New Formula Rewriting by Reasoning on a Graphical Representation of SAT Instances
Philippe Jégou, Lionel Paris

Last modified: 2009-10-22


In this paper, we propose a new approach for solving the SAT problem.
This approach consists in representing SAT instances thanks to an undirected graph issued from a polynomial transformation from SAT to the CLIQUE problem. Considering this graph, we exploit well known properties of chordal graphs to manipulate the SAT instance.
Firstly, these properties allow us to define a new class of SAT polynomial instances.
Moreover, they allow us to rewrite SAT instances in disjunctions of smaller instances which could be significantly easier to solve.


SAT; reformulation; Perfect graphs; rewriting

Full Text: PDF