DocumentCode
749542
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
Volume
22
Issue
8
fYear
2003
Firstpage
995
Lastpage
1004
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;
fLanguage
English
Journal_Title
Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on
Publisher
ieee
ISSN
0278-0070
Type
jour
DOI
10.1109/TCAD.2003.814960
Filename
1214858
Link To Document