Local Search for Hard SAT Formulas: The Strength of the Polynomial Law

Authors

  • Sixue Liu Tsinghua University
  • Periklis Papakonstantinou Rutgers University

DOI:

https://doi.org/10.1609/aaai.v30i1.10083

Keywords:

SAT-solver, local search, theory, experiments

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.

Downloads

Published

2016-02-21

How to Cite

Liu, S., & Papakonstantinou, P. (2016). Local Search for Hard SAT Formulas: The Strength of the Polynomial Law. Proceedings of the AAAI Conference on Artificial Intelligence, 30(1). https://doi.org/10.1609/aaai.v30i1.10083

Issue

Section

Technical Papers: Heuristic Search and Optimization