Exploiting the real power of unit propagation lookahead

One of the best SAT solvers for random 3-SAT formulae, SATZ, is based on a heuristic called unit propagation lookahead (UPL). Unfortunately, it does not perform so well on specific structured instances, especially on the ones coming from an area where a huge interest for SAT has emerged in recent years: symbolic model checking (SMC). We claim that all the power of this heuristic is not used in SATZ, and that UPL can be extended to solve some real world structured problems, where the major competitors are using intelligent backtracking or specific deduction rules. We introduce a preprocessing technique that can be applied to simplify instances containing equivalent literals. This technique is based on UPL, so it can be easily added to any solver using this heuristic. We compare our approach to the new extension of SATZ for equivalency reasoning (EqSATZ) and another approach, the Stهlmarck method, which is mainly used in SMC. thor would like to thank Yacine Boufkhad for his insights about C-SAT and 2-simplify, Mamoun Filali-Amine for pointing out the Stهlmark method, Chu-Min Li for his discussions about EqSATZ and his implementation of the implied literal propagation in SATZ, Laurent Simon for his SAT-Ex web site, Miroslav Velev for his remarks on the early version of the paper and the referees for their helpful comments. This research was funded by an ARC Large Grant at The University of Newcastle.