Title :
Satometer: how much have we searched?
Author :
Aloul, Fadi A. ; Sierawski, Brian D. ; Sakallah, Karem A.
Author_Institution :
Dept. of Electr. Eng. & Comput. Sci., Michigan Univ., Dearborn, 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 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 BDD 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; data structures; electronic design automation; fault diagnosis; logic CAD; EDA problem instances; SAT solvers; Satometer; adjustable accuracy; backtrack SAT solver; conflict diagnosis; conflicts; normalized minterm count; search progress; search space; zero-suppressed BDD data structure; Binary decision diagrams; Data structures; Decision trees; Electronic design automation and methodology; Large-scale systems; Permission; Space exploration;
Conference_Titel :
Design Automation Conference, 2002. Proceedings. 39th
Print_ISBN :
1-58113-461-4
DOI :
10.1109/DAC.2002.1012720
