Exploiting Hypergraph Partitioning for E±cient Boolean Satis¯ability

Abstract: This paper presents hypergraph parti-tioning based constraint decomposition procedures to guide Boolean Satis¯ability search. Variable-constraint relationships are modeled on a hypergraph and parti-tioning based techniques are employed to decompose the constraints. Subsequently, the decomposition is analyzed to solve the CNF-SAT problem e±ciently. The contributions of this research are two-fold: 1) to engineer a constraint decomposition technique using hy-pergraph partitioning; 2) to engineer a constraint resolu-tion method based on this decomposition. Preliminary experiments show that our approach is fast, scalable and can signi¯cantly increase the performance (often orders of magnitude) of the SAT engine. I