DC Field
Value
Language
dc.contributor.author
Coutelier, Robin
-
dc.contributor.author
Fleury, Mathias
-
dc.contributor.author
Kovacs, Laura
-
dc.contributor.editor
Chakraborty, Supratik
-
dc.contributor.editor
Jiang, Jie-Hong Roland
-
dc.date.accessioned
2025-02-04T16:49:21Z
-
dc.date.available
2025-02-04T16:49:21Z
-
dc.date.issued
2024-08-19
-
dc.identifier.citation
<div class="csl-bib-body"> <div class="csl-entry">Coutelier, R., Fleury, M., &#38; Kovacs, L. (2024). Lazy Reimplication in Chronological Backtracking. In S. Chakraborty &#38; J.-H. R. Jiang (Eds.), <i>27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)</i> (pp. 9:1-9:19). Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.SAT.2024.9</div> </div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/210852
-
dc.description.abstract
Chronological backtracking is an interesting SAT solving technique within CDCL reasoning, as it backtracks less aggressively upon conflicts. However, chronological backtracking is more difficult to maintain due to its weaker SAT solving invariants. This paper introduces a lazy reimplication procedure for missed lower implications in chronological backtracking. Our method saves propagations by reimplying literals on demand, rather than eagerly. Due to its modularity, our work can be replicated in other solvers, as shown by our results in the solvers CaDiCaL and Glucose.
en
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.rights.uri
https://creativecommons.org/licenses/by/4.0/
-
dc.subject
Chronological Backtracking
en
dc.subject
CDCL
en
dc.subject
Invariants
en
dc.subject
Watcher Lists
en
dc.title
Lazy Reimplication in Chronological Backtracking
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.relation.publication
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
-
dc.contributor.affiliation
University of Freiburg, Germany
-
dc.contributor.editoraffiliation
Indian Institute of Technology Bombay, India
-
dc.contributor.editoraffiliation
National Taiwan University, Taiwan (Province of China)
-
dc.relation.isbn
978-3-95977-334-8
-
dc.relation.issn
1868-8969
-
dc.description.startpage
9:1
-
dc.description.endpage
9:19
-
dc.relation.grantno
F 8500
-
dc.relation.grantno
ICT22-007
-
dc.rights.holder
© Robin Coutelier, Mathias Fleury, and Laura Kovács;
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
-
tuw.container.volume
305
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Schloss Dagstuhl
-
tuw.relation.publisherplace
Leibniz-Zentrum für Informatik
-
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.publisher.doi
10.4230/LIPIcs.SAT.2024.9
-
dc.identifier.libraryid
AC17426713
-
dc.description.numberOfPages
19
-
tuw.author.orcid
0009-0002-4735-5215
-
tuw.author.orcid
0000-0002-8299-2714
-
dc.rights.identifier
CC BY 4.0
en
dc.rights.identifier
CC BY 4.0
de
tuw.event.name
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)
en
tuw.event.startdate
21-08-2024
-
tuw.event.enddate
24-08-2024
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Pune
-
tuw.event.country
IN
-
tuw.event.presenter
Coutelier, Robin
-
tuw.event.track
Single Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.grantfulltext
open
-
item.fulltext
with Fulltext
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.cerifentitytype
Publications
-
item.openairetype
conference paper
-
item.mimetype
application/pdf
-
item.openaccessfulltext
Open Access
-
crisitem.project.funder
FWF - Österr. Wissenschaftsfonds
-
crisitem.project.funder
WWTF Wiener Wissenschafts-, Forschu und Technologiefonds
-
crisitem.project.grantno
F 8500
-
crisitem.project.grantno
ICT22-007
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.dept
University of Freiburg, Germany
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
crisitem.author.orcid
0009-0002-4735-5215
-
crisitem.author.orcid
0000-0002-8299-2714
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
crisitem.author.parentorg
E192 - Institut für Logic and Computation
-
Appears in Collections:
Conference Paper
Fulltext (Version of Record (published version))
Adobe PDF
(945.88 kB)
Lazy Reimplication in Chronological Backtracking
Open Access CC BY 4.0
Show simple item record

Page view(s)

455
checked on Feb 4, 2025

Download(s)

200
checked on Feb 4, 2025

Google ScholarTM

Check