Eric I. Hsu, Christian J. Muise, J. Christopher Beck, Sheila McIlraith
Backbone variables have the same assignment in all solutions to a given constraint satisfaction problem; more generally, bias represents the proportion of solutions that assign a variable a particular value. Intuitively such constructs would seem important to efficient search, but their study to date has assumed a mostly conceptual perspective, in terms of indicating problem hardness or motivating and interpreting heuristics. In this work, we first measure the ability of both existing and novel probabilistic message-passing techniques to directly estimate bias (and identify backbones) for the specific problem of Boolean Satisfiability (SAT). We confirm that methods like Belief Propagation and Survey Propagation — plus Expectation Maximization-based variants — do produce good estimates with distinctive properties. We demonstrate the use of bias estimation within a modern SAT solver, and exhibit a correlation between accurate, stable, estimates and successful search. The same process also yields a family of search heuristics that can dramatically improve search efficiency for the hard random problems considered in this study.
Subjects: 15.7 Search; 3.4 Probabilistic Reasoning
Submitted: May 1, 2008