Lazy Reimplication in Chronological Backtracking
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866915101159718912 |
|---|---|
| author | Coutelier, Robin Fleury, Mathias Kovács, Laura |
| author_facet | Coutelier, Robin Fleury, Mathias Kovács, Laura |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_07457 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Lazy Reimplication in Chronological Backtracking Coutelier, Robin Fleury, Mathias Kovács, Laura Logic in Computer Science 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. |
| title | Lazy Reimplication in Chronological Backtracking |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2501.07457 |