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.SAT.2023.18
URN: urn:nbn:de:0030-drops-184803
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18480/
Oliveras, Albert ;
Li, Chunxiao ;
Wu, Darryl ;
Chung, Jonathan ;
Ganesh, Vijay
Learning Shorter Redundant Clauses in SDCL Using MaxSAT
Abstract
In this paper we present the design and implementation of a Satisfaction-Driven Clause Learning (SDCL) SAT solver, MapleSDCL, which uses a MaxSAT-based technique that enables it to learn shorter, and hence better, redundant clauses. We also perform a thorough empirical evaluation of our method and show that our SDCL solver solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver.
BibTeX - Entry
@InProceedings{oliveras_et_al:LIPIcs.SAT.2023.18,
author = {Oliveras, Albert and Li, Chunxiao and Wu, Darryl and Chung, Jonathan and Ganesh, Vijay},
title = {{Learning Shorter Redundant Clauses in SDCL Using MaxSAT}},
booktitle = {26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-286-0},
ISSN = {1868-8969},
year = {2023},
volume = {271},
editor = {Mahajan, Meena and Slivovsky, Friedrich},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18480},
URN = {urn:nbn:de:0030-drops-184803},
doi = {10.4230/LIPIcs.SAT.2023.18},
annote = {Keywords: SAT, SDCL, MaxSAT}
}
|
Keywords: |
|
SAT, SDCL, MaxSAT |
|
Collection: |
|
26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
09.08.2023 |
