Efficiently Exploiting Dependencies in Local Search for SAT
Abstract
We propose a new local search platform that splits a CNF formula into three sub-components: i) a minimal dependency lattice (representing the core connections between logic gates), ii) a conjunction of equivalence clauses, and iii) the remaining clauses. We also adopt a new hierarchical cost function that focuses on solving the core components of the problem first. We then show experimentally that our platform not only significantly outperforms existing local search approaches but is also competitive with modern systematic solvers on highly structured problems.
Cite
Text
Pham et al. "Efficiently Exploiting Dependencies in Local Search for SAT." AAAI Conference on Artificial Intelligence, 2008.Markdown
[Pham et al. "Efficiently Exploiting Dependencies in Local Search for SAT." AAAI Conference on Artificial Intelligence, 2008.](https://mlanthology.org/aaai/2008/pham2008aaai-efficiently/)BibTeX
@inproceedings{pham2008aaai-efficiently,
title = {{Efficiently Exploiting Dependencies in Local Search for SAT}},
author = {Pham, Duc Nghia and Thornton, John and Sattar, Abdul},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2008},
pages = {1476-1478},
url = {https://mlanthology.org/aaai/2008/pham2008aaai-efficiently/}
}