Title :
Satometer: how much have we searched?
Author :
Aloul, Fadi A. ; Sierawski, Brian D. ; Sakallah, Karem A.
Author_Institution :
Electr. Eng. & Comput. Sci. Dept., Univ. of Michigan, Ann Arbor, MI, USA
Abstract :
We introduce Satometer, a tool that can be used to estimate the percentage of the search space actually explored by a backtrack Boolean satisfiability (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 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.
Keywords :
Boolean functions; binary decision diagrams; computability; logic CAD; Boolean functions; CAD; SAT instance; Satometer; backtrack Boolean satisfiability solver; conflicts; normalized minterm count; search space; zero-suppressed binary decision diagram; Boolean algebra; Boolean functions; Data structures; Design automation; Electronic design automation and methodology; Helium; Logic design; Logic functions; Search methods; Space exploration;
Journal_Title :
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
DOI :
10.1109/TCAD.2003.814960
