License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2021.5
URN: urn:nbn:de:0030-drops-152969
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/15296/
Cai, Shaowei ;
Luo, Chuan ;
Zhang, Xindi ;
Zhang, Jian
Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper)
Abstract
This work is dedicated to improving local search solvers for the Boolean satisfiability (SAT) problem on structured instances. We propose a construct-and-cut (CnC) algorithm based on unit propagation, which is used to produce initial assignments for local search. We integrate our CnC initialization procedure within several state-of-the-art local search SAT solvers, and obtain the improved solvers. Experiments are carried out with a benchmark encoded from a spectrum repacking project as well as benchmarks encoded from two important mathematical problems namely Boolean Pythagorean Triple and Schur Number Five. The experiments show that the CnC initialization improves the local search solvers, leading to better performance than state-of-the-art SAT solvers based on Conflict Driven Clause Learning (CDCL) solvers.
BibTeX - Entry
@InProceedings{cai_et_al:LIPIcs.CP.2021.5,
author = {Cai, Shaowei and Luo, Chuan and Zhang, Xindi and Zhang, Jian},
title = {{Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization}},
booktitle = {27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
pages = {5:1--5:10},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-211-2},
ISSN = {1868-8969},
year = {2021},
volume = {210},
editor = {Michel, Laurent D.},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/15296},
URN = {urn:nbn:de:0030-drops-152969},
doi = {10.4230/LIPIcs.CP.2021.5},
annote = {Keywords: Satisfiability, Local Search, Unit Propagation, Mathematical Problems}
}
