<div class="csl-bib-body">
<div class="csl-entry">Coutelier, R., Hader, T., & Kovacs, L. (2026). Generalizing CDCL with Graph Backtracking. In A. Ignatiev & S. Szeider (Eds.), <i>29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)</i> (pp. 1–18). Schloss Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.SAT.2026.14</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/230148
-
dc.description.abstract
We present graph backtracking, a novel, fine-grained backtracking scheme for CDCL-based SAT solving, parametrized by a user-defined weight function. For conflict repair, we challenge the decision level abstraction and use the implication graph as a precise guiding structure to minimize the weight of literals that are unassigned. Graph backtracking is sound, complete, and terminating. We show that it is a generalization of chronological and non-chronological backtracking by simulating them with specific weight functions. Our approach is implemented in the experimental solver NapSAT. Empirical results show that graph backtracking requires fewer literal propagations than standard approaches, leading to improved solver runtime.
en
dc.description.sponsorship
European Commission
-
dc.description.sponsorship
TTTech Auto AG; B & C Privatstiftung
-
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.description.sponsorship
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Leibniz International Proceedings in Informatics (LIPIcs)
-
dc.subject
SAT Solving
en
dc.subject
Backtracking
en
dc.subject
Conflict Analysis
en
dc.subject
CDCL
en
dc.title
Generalizing CDCL with Graph Backtracking
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.editoraffiliation
Monash University, Australia
-
dc.relation.isbn
978-3-95977-431-4
-
dc.description.startpage
1
-
dc.description.endpage
18
-
dc.relation.grantno
ERC Consolidator Grant 2020
-
dc.relation.grantno
nicht bekannt
-
dc.relation.grantno
F 8500
-
dc.relation.grantno
ICT22-007
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)
-
tuw.container.volume
377
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Schloss Dagstuhl Publishing
-
tuw.relation.publisherplace
Leibniz, Germany
-
tuw.book.chapter
14
-
tuw.project.title
Automated Reasoning with Theories and Induction for Software Technologies
-
tuw.project.title
Trustworthy Autonomous Cyber-Physical Systems
-
tuw.project.title
Semantische und kryptografische Grundlagen von Informationssicherheit und Datenschutz durch modulares Design
-
tuw.project.title
Effective Formal Methods for Smart-Contract Certification
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publication.orgunit
E056-17 - Fachbereich Trustworthy Autonomous Cyber-Physical Systems
-
tuw.publication.orgunit
E056-10 - Fachbereich SecInt-Secure and Intelligent Human-Centric Digital Technologies
-
tuw.publication.orgunit
E056-13 - Fachbereich LogiCS
-
tuw.publication.orgunit
E056-26 - Fachbereich Automated Reasoning
-
tuw.publisher.doi
10.4230/LIPIcs.SAT.2026.14
-
dc.description.numberOfPages
18
-
tuw.author.orcid
0009-0002-4735-5215
-
tuw.author.orcid
0009-0002-8920-5469
-
tuw.author.orcid
0000-0002-8299-2714
-
tuw.editor.orcid
0000-0001-8994-1656
-
tuw.event.name
The 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)
en
tuw.event.startdate
20-07-2026
-
tuw.event.enddate
23-07-2026
-
tuw.event.online
On Site
-
tuw.event.place
Lisbon
-
tuw.event.country
PT
-
tuw.event.presenter
Coutelier, Robin
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.grantfulltext
none
-
item.openairetype
conference paper
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.languageiso639-1
en
-
item.fulltext
no Fulltext
-
item.cerifentitytype
Publications
-
crisitem.project.funder
European Commission
-
crisitem.project.funder
B & C Privatstiftung
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.funder
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
crisitem.project.grantno
ERC Consolidator Grant 2020
-
crisitem.project.grantno
nicht bekannt
-
crisitem.project.grantno
F 8500
-
crisitem.project.grantno
ICT22-007
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
