2026-08-17T08:32:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:18480 2024-03-06T11:02:00Z ddc:004 open_access

Learning Shorter Redundant Clauses in SDCL Using MaxSAT Oliveras, Albert Li, Chunxiao Wu, Darryl Chung, Jonathan Ganesh, Vijay SAT SDCL MaxSAT 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Albert Oliveras and Chunxiao Li and Darryl Wu and Jonathan Chung and Vijay Ganesh 2023 Is Part Of LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2023.18 urn:nbn:de:0030-drops-184803 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.18 eng https://creativecommons.org/licenses/by/4.0/legalcode