VARSAT Solver Homepage


Thanks for visiting the homepage of the VARSAT SAT-solver!

graph showing performance of VARSAT

At this point we have a series of experimental results concerning bias estimation, maintained by Christian Muise. The graphs compare the surveys produced by various bias estimation techniques to the true bias profiles we calculated exhaustively, for randomly generated problems. The experiments study the techniques both in isolation and in backtrack-free search. Backtrack-free search tries to find a solution by repeatedly calculating surveys and setting one variable at a time (specifically, by setting the most strongly biased variable to its more strongly biased value.) The process ends either by setting a whole string of variables to good values and thus reaching a solution, or by setting a variable to a bad value that eliminates all remaining solutions--resulting in failure.

Two technical reports are also available here: the first describes an experimental comparison of various bias estimation techniques operating in isolation, and when embedded within a backtracking SAT-Solver. The second explains how to derive the four estimators that were created by employing the Expectation Maximization framework.


Please contact Eric Hsu with any comments or questions!