A New Formula Rewriting by Reasoning on a Graphical Representation of SAT Instances

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.