Satometer v0.1

Measures the progress of backtrack-search SAT solvers



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.



Maintained by Fadi Aloul (
Last updated Mon June 17, 2009