Satometer v0.1

Introduction

• Measures the search space explored by a backtrack SAT solver.
• Can be used dynamically or as a post-processor. This program is set to run as a post-processor, but can easily be adapted to run dynamically during the search process.
• SAT solver has to be able to emit conflict-induced clauses.
• Measures an exact or approximate estimate of the explored search space
  
  

Example

Given a problem with 3 variables: a,b,c. If two conflict clauses were learned:

(a+b) ..... eliminates 25%
(a+!b) .... eliminates 25%

The total explored search space reported by Satometer would be: 50%.

However, advanced conflict diagnosis can record overlapping conflict-induced clauses.
For example:

(a+b) ..... eliminates 25%
(b+c) ..... eliminates 25%

Although each clause individually eliminates 25% of the search space. Their combination eliminates only 37.5% of the search space.

Download

• SATOMETER, version 0.1, download the tarred, gzipped executable
  
  • Executable - Intel/Linux - [Satometer_Linux_v01.tar.gz] (756 Kb)
    
  • Executable - Sun/Solaris - [Satometer_Solaris_v01.tar.gz] (750 Kb)

• Other
  • CUDD: http://vlsi.colorado.edu/~fabio/CUDD/
    
  • ZBDD/CUDD Lib: http://www.aloul.net/Tools/zbddLib

References

• F. Aloul, B. Sierawski, and K. Sakallah, "Satometer: How Much Have We Searched?" IEEE Transactions on Computer Aided Design (TCAD), 22(8), pp. 995-1004, Aug. 2003.
  
  
• F. Aloul, B. Sierawski, and K. Sakallah, "Satometer: How Much Have We Searched?" Design Automation Conference (DAC), New Orleans, Louisiana, 2002.
  
  
• F. Aloul, B. Sierawski, and K. Sakallah, "A Tool for Measuring Progress of Backtrack Search Solvers," Symposium on the Theory and Applications of Satisfiability Testing (SAT), Cincinnati, Ohio, 2002.