---
title: "Depth-Driven Circuit-Level Stochastic Local Search for SAT"
authors:
  - "Anton Belov"
  - "Matti Järvisalo"
  - "Zbigniew Stachniak"
doi: "10.5591/978-1-57735-516-8/IJCAI11-092"
url: "https://ijcai.org/proceedings/2011/92"
pdf: "https://ijcai.org/proceedings/2011/0092.pdf"
venue: "Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence"
year: 2011
pages: "504-508"
track: ""
keywords:
---

# Depth-Driven Circuit-Level Stochastic Local Search for SAT

Anton Belov, Matti Järvisalo, Zbigniew Stachniak

*Proceedings of the Twenty-Second International Joint Conference on Artificial Intelligence*, pages 504-508. DOI: [10.5591/978-1-57735-516-8/IJCAI11-092](https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-092)

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