ESampler: Boosting sampling of satisfying assignments for Boolean formulas via derivation

Boolean satisfiability (SAT) plays a key role in diverse areas such as spanning planning, inference, data mining, testing and optimization. Apart from the classical problem of checking Boolean satisfiability, generating random satisfying assignments has attracted significant theoretical and practical interests over the past years. In practical applications, usually a large number of satisfying assignments for a given Boolean formula are needed, the generation of which turns out to be a computational hard problem in both theory and practice. In this work, we propose a novel approach to derive a large set of satisfying assignments from a given one in an efficient way. Our approach is based on an insight that flipping the truth values of properly chosen variables of a satisfying assignment could result in satisfying assignments without invoking computationally expensive SAT solving. We propose a derivation algorithm to discover such variables for each given satisfying assignment. Our approach is orthogonal to the previous techniques for generating satisfying assignments and could be integrated into the existing SAT samplers. We implement our approach as an open-source tool using two representative state-of-the-art samplers ( and ) as the underlying satisfying assignment generation engine. We conduct extensive experiments on various publicly available benchmarks and apply to solve Bayesian inference. The results show that can efficiently boost the sampling of satisfying assignments of both and on a large portion of the benchmarks and is at least comparable on the others. performs considerably better than and , as well as another state-of-the-art sampler SearchTreeSampler.