Nonchronological backtracking in stochastic Boolean satisfiability

Stochastic Boolean satisfiability (SSAT) is a generalization of satisfiability (SAT) that has shown promise as a vehicle for encoding and competitively solving probabilistic reasoning problems. We extend the theory and enhance the applicability of SSAT-based solution techniques by 1) establishing theoretical results that allow the incorporation of nonchronological backtracking (NCB), and lay the foundation for the incorporation of learning, into an SSAT solver, 2) implementing SOLVESSAT-NCB, an NCB-augmented SSAT solver, and 3) describing the results of tests of SOLVESSAT-NCB on randomly generated SSAT problems and SSAT encodings of probabilistic planning problems. Our experiments indicate that NCB has the potential to boost the performance of an SSAT solver, both in terms of time, yielding speedups of as much as five orders of magnitude, and space, allowing the solution of SSAT problems with larger solution trees. In some cases, however, NCB can degrade performance. We analyze the reasons for this behavior, present initial results incorporating a technique to mitigate this effect, and discuss other approaches to addressing this problem suggested by our empirical results.