@inproceedings{14061262ef7148a9bcac4494fe6b2811,
title = "Improving local search for structured SAT formulas via unit propagation based construct and cut initialization",
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.",
keywords = "Local Search, Mathematical Problems, Satisfiability, Unit Propagation",
author = "Shaowei Cai and Chuan Luo and Xindi Zhang and Jian Zhang",
note = "Publisher Copyright: {\textcopyright} Shaowei Cai, Chuan Luo, Xindi Zhang, and Jian Zhang.; 27th International Conference on Principles and Practice of Constraint Programming, CP 2021 ; Conference date: 25-10-2021 Through 29-10-2021",
year = "2021",
month = oct,
day = "1",
doi = "10.4230/LIPIcs.CP.2021.5",
language = "英语",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Michel, \{Laurent D.\}",
booktitle = "27th International Conference on Principles and Practice of Constraint Programming, CP 2021",
address = "德国",
}