Solving SAT Problem by Pseudo-Boolean Optimization Engine

Boolean satisfiability (SAT) problem is a well-known problem with many applications in the field of VLSI Computer-Aided Design. In recent years, dramatic improvements in SAT solver help us to solve instances more efficiently. In this thesis, we propose a novel idea to translate SAT problem into Pseudo-Boolean (PB) optimization problem and then solve by PB engine. Our approach produces a cut for the instance by breaking part of clause connectivity from some variables. We utilize the requirement of synchronizing same variables with identical assignment during the process, making sum of the difference in value between a cutting variable in different clauses as the optimization goal to be minimized. To pick appropriate variables, we apply two algorithms based on clause partitioning - one views CNF as hypergraph and uses hMETIS for min-cut bi-partitioning; another evaluates the clauses depending on literal and variable activity. The experimental results show that the PB optimization modeling technique performs well for a few instances.