Local Search for Hard SAT Formulas: The Strength of the Polynomial Law
Abstract
Random k-CNF formulas at the anticipated k-SAT phase-transition point are prototypical hard k-SAT instances. We develop a stochastic local search algorithm and study it both theoretically and through a large-scale experimental study. The algorithm comes as a result of a systematic study that contrasts rates at which a certain measure concentration phenomenon occurs. This study yields a new stochastic rule for local search. A strong point of our contribution is the conceptual simplicity of our algorithm. More importantly, the empirical results overwhelmingly indicate that our algorithm outperforms the state-of-the-art. This includes a number of winners and medalist solvers from the recent SAT Competitions.
Cite
Text
Liu and Papakonstantinou. "Local Search for Hard SAT Formulas: The Strength of the Polynomial Law." AAAI Conference on Artificial Intelligence, 2016. doi:10.1609/AAAI.V30I1.10083Markdown
[Liu and Papakonstantinou. "Local Search for Hard SAT Formulas: The Strength of the Polynomial Law." AAAI Conference on Artificial Intelligence, 2016.](https://mlanthology.org/aaai/2016/liu2016aaai-local/) doi:10.1609/AAAI.V30I1.10083BibTeX
@inproceedings{liu2016aaai-local,
title = {{Local Search for Hard SAT Formulas: The Strength of the Polynomial Law}},
author = {Liu, Sixue and Papakonstantinou, Periklis A.},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2016},
pages = {732-738},
doi = {10.1609/AAAI.V30I1.10083},
url = {https://mlanthology.org/aaai/2016/liu2016aaai-local/}
}