Sciweavers

Share
SAT
2009
Springer

VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search

9 years 6 months ago
VARSAT: Integrating Novel Probabilistic Inference Techniques with DPLL Search
Probabilistic inference techniques can be used to estimate variable bias, or the proportion of solutions to a given SAT problem that fix a variable positively or negatively. Methods like Belief Propagation (BP), Survey Propagation (SP), and Expectation Maximization BP (EMBP) have been used to guess solutions directly, but intuitively they should also prove useful as variable- and valueordering heuristics within full backtracking (DPLL) search. Here we report on practical design issues for realizing this intuition in the VARSAT system, which is built upon the full-featured MiniSat solver. A second, algorithmic, contribution is to present four novel inference techniques that combine BP/SP models with local/global consistency constraints via the EMBP framework. Empirically, we can also report exponential speed-up over existing complete methods, for random problems at the critically-constrained phase transition region in problem hardness. For industrial problems, VARSAT is slower that Min...
Eric I. Hsu, Sheila A. McIlraith
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SAT
Authors Eric I. Hsu, Sheila A. McIlraith
Comments (0)
books