Technical Report No. 188 - Abstract

Marc Herbstritt
zChaff: Modifications and Extensions

The application of SAT solver in industrial verification tools is mandatory for the successful analysis of problems derived from hardware design, e.g. Combinational Equivalence Checking (CEC) and Bounded Model Checking (BMC). Moskewicz et al. have developed a new powerful SAT solver in 2001 that outperforms most of the existing publicly available SAT solvers when applied to hard real-world problems, e.g. from VLSI CAD. There are two versions available of Chaff: mChaff and zChaff. Both are instances of Chaff, but from the viewpoint of implementation they are totally different since they were developped independently by M.~Moskewicz (mChaff) and L. Zhang (zChaff). In this paper we concentrate on zChaff. We analyze the core issues and propose modifications and extensions.