Guiding CNF-SAT search via efficient constraint partitioning

Contemporary techniques to identify a good variable order for SAT rely on identifying minimum tree-width decompositions. However, the problem of finding a minimal width tree decomposition for an arbitrary graph is NP complete. The available tools and methods are impractical, as they cannot handle large and hard-to-solve CNF-SAT instances. This work proposes a hypergraph partitioning based constraint decomposition technique as an alternative to contemporary methods. We model the CNF-SAT problem on a hypergraph and apply min-cut based bi-partitioning. Clause-variable statistics across the partitions are analyzed to further decompose the problem, iteratively. The resulting tree-like decomposition provides a variable order for guiding CNF-SAT search. Experiments demonstrate that our partitioning procedure is fast, scalable and the derived variable order results in significant increase in performance of the SAT engine.