Extending unit propagation look-ahead of DPLL procedure

Abstract

The DPLL (Davis-Putnam-Logemann-Loveland) procedure is one of the most effective methods for solving SAT problems. It is well known that its efficiency depends on the choice of the branching rule. Different branching rules are proposed in the literature. Unit propagation look-ahead (UPLA) branching rule was one of the main improvements in the DPLL procedure (e.g.,[10]). The UPLA branching rule integrated in satz SAT solver [10] performs a series of variable filtering process at each node as a static variable filtering agency. In this paper we introduce and experiment with dynamic variable filtering (DVF) based branching rule which extends the UPLA heuristic process for doing more filtering and choosing a best branching variable from an irreducible sub-formula. To enhance the performance of DVF branching rule, we integrate neighborhood variable ordering heuristic (NVO) for exploring only the neighborhood variables of the current assigned variable. Experimental results of DVF+NVO branching rule on a number of real-world benchmark instances and quasigroup problems prove our approaches to be useful in many circumstances. © Springer-Verlag Berlin Heidelberg 2004.