# Solving #SAT and Bayesian Inference with Backtracking Search

arXiv: https://arxiv.org/abs/1401.3458 · HTML: https://mlsanity.com/paper/1401.3458/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 15 Jan 2014.

## Built on by (most cited first, 6 of 6)

- [A Compositional Atlas for Algebraic Circuits](https://mlsanity.com/paper/2412.05481/) (2024)
- [Handling Epistemic and Aleatory Uncertainties in Probabilistic Circuits](https://mlsanity.com/paper/2102.10865/) (2021)
- [Enhancing SMT-based Weighted Model Integration by Structure Awareness](https://mlsanity.com/paper/2302.06188/) (2023)
- [SMT-based Weighted Model Integration with Structure Awareness](https://mlsanity.com/paper/2206.13856/) (2022)
- [Mixtures of All Trees](https://mlsanity.com/paper/2302.14202/) (2023)
- [Quantum Algorithms for Weighted Constrained Sampling and Weighted Model Counting](https://mlsanity.com/paper/2407.12816/) (2024)

## Abstract (arXiv)

Inference in Bayes Nets (BAYES) is an important problem with numerous applications in probabilistic reasoning. Counting the number of satisfying assignments of a propositional formula (#SAT) is a closely related problem of fundamental theoretical importance. Both these problems, and others, are members of the class of sum-of-products (SUMPROD) problems. In this paper we show that standard backtracking search when augmented with a simple memoization scheme (caching) can solve any sum-of-products problem with time complexity that is at least as good any other state-of-the-art exact algorithm, and that it can also achieve the best known time-space tradeoff. Furthermore, backtracking's ability to utilize more flexible variable orderings allows us to prove that it can achieve an exponential speedup over other standard algorithms for SUMPROD on some instances. The ideas presented here have been utilized in a number of solvers that have been applied to various types of sum-of-product problems. These system's have exploited the fact that backtracking can naturally exploit more of the problem's structure to achieve improved performance on a range of probleminstances. Empirical evidence of this performance gain has appeared in published works describing these solvers, and we provide references to these works.