Abstract
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.
We investigate a hybrid approach by employing cross-entropy as a preprocessing step to SAT solving. First CROiSSANT is run to identify the areas of the search space that are more likely to contain a satisfying assignment; this information is then given to a DPLL-based SAT solver as a partial or a complete assignment that is used to suggest variables assignments in the search.
We tested our approach on a set of benchmarks, in different configurations of tunable parameters of the cross-entropy algorithm; as experimental results show, it represents a sound basis for the development of a cross-entropy-based SAT solver.
We investigate a hybrid approach by employing cross-entropy as a preprocessing step to SAT solving. First CROiSSANT is run to identify the areas of the search space that are more likely to contain a satisfying assignment; this information is then given to a DPLL-based SAT solver as a partial or a complete assignment that is used to suggest variables assignments in the search.
We tested our approach on a set of benchmarks, in different configurations of tunable parameters of the cross-entropy algorithm; as experimental results show, it represents a sound basis for the development of a cross-entropy-based SAT solver.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of the 28th Annual ACM Symposium on Applied Computing, SAC |
| Publisher | ACM |
| Pages | 1196-1203 |
| Number of pages | 8 |
| Publication status | Published - 18 Mar 2013 |