## 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 |