Using cross-entropy for satisfiability
Hana Chockler, Alexander Ivrii, Arie Matsliah, Simone Fulvio Rollini, Natasha Sharygina · 2013
This paper proposes a novel approach to SAT solving by using the cross-entropy method for optimization. It introduces an extension of the Boolean satisfiability setting to a multi-valued framework, where a probability space is induced over the set of all possible assignments. For a given formula, a cross-entropy-based algorithm (implemented in a tool named CROiSSANT) is used to find a satisfying assignment by applying an iterative procedure that optimizes an objective function correlated with the likelihood of satisfaction.