To solve boolean satisfiability (SAT) problems more efficient, this paper presents a polarity decision policy, which calculates the polarity of variable according to the Jeroslow-Wang heuristic and Glucose heuristic, the proposed approach is embed into the SAT solver Glucose2.3. Experiment results show that the performance of the new solver, named Glucose_IM, is better than Glucose2.3 on the application certified UNSAT instances and hard combinatorial SAT instances at SAT competition 2013.
展开▼
