Satometer: How Much Have We Searched? (Preprint)

We introduce Satometer, a tool that can be used to estimate the percentage of the search space actually explored by a backtrack SAT solver. Satometer calculates a normalized minterm count for those portions of the search space identified by conflicts. The computation is carried out using a zero-suppressed binary decision diagram (ZBDD) data structure and can have adjustable accuracy. The data provided by Satometer can help diagnose the performance of SAT solvers and can shed light on the nature of a SAT instance.
Presented at the Design Automation Conference (39th), DAC 2002, held New Orleans, LA on 10-14 Jun 2002 and published in proceedings, p737-742, 2002; ISBN 1-58113-461-4. Also published in IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems, v22, n8, p995-1004, Aug 2003. The original document contains color images.