Exploiting hypergraph partitioning for efficient Boolean satisfiability

This paper presents hypergraph partitioning based constraint decomposition procedures to guide Boolean satisfiability search. Variable-constraint relationships are modeled on a hypergraph and partitioning based techniques are employed to decompose the constraints. Subsequently, the decomposition is analyzed to solve the CNF-SAT problem efficiently. The contributions of this research are two-fold: 1) to engineer a constraint decomposition technique using hypergraph partitioning; 2) to engineer a constraint resolution method based on this decomposition. Preliminary experiments show that our approach is fast, scalable and can significantly increase the performance (often orders of magnitude) of the SAT engine.