Using cross-entropy for satisfiability

Hana Chockler, Alexander Ivrii, Arie Matsliah, Simone Fulvio Rollini, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

4 Citations (Scopus)
32 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings of the 28th Annual ACM Symposium on Applied Computing, SAC
PublisherACM
Pages1196-1203
Number of pages8
Publication statusPublished - 18 Mar 2013

Fingerprint

Dive into the research topics of 'Using cross-entropy for satisfiability'. Together they form a unique fingerprint.

Cite this