Depth-Driven Circuit-Level Stochastic Local Search for SAT

Abstract

We develop a novel circuit-level stochastic local search (SLS) method D-CRSat for Boolean satisfiability by integrating a structure-based heuristic into the recent CRSat algorithm. D-CRSat significantly improves on CRSat on real-world application benchmarks on which other current CNF and circuit-level SLS methods tend to perform weakly. We also give an intricate proof of probabilistically approximate completeness for D-CRSat, highlighting key features of the method.

Cite

Text

Belov et al. "Depth-Driven Circuit-Level Stochastic Local Search for SAT." International Joint Conference on Artificial Intelligence, 2011. doi:10.5591/978-1-57735-516-8/IJCAI11-092

Markdown

[Belov et al. "Depth-Driven Circuit-Level Stochastic Local Search for SAT." International Joint Conference on Artificial Intelligence, 2011.](https://mlanthology.org/ijcai/2011/belov2011ijcai-depth/) doi:10.5591/978-1-57735-516-8/IJCAI11-092

BibTeX

@inproceedings{belov2011ijcai-depth,
  title     = {{Depth-Driven Circuit-Level Stochastic Local Search for SAT}},
  author    = {Belov, Anton and Järvisalo, Matti and Stachniak, Zbigniew},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2011},
  pages     = {504-509},
  doi       = {10.5591/978-1-57735-516-8/IJCAI11-092},
  url       = {https://mlanthology.org/ijcai/2011/belov2011ijcai-depth/}
}