Fast and Verified UNSAT Certificate Checking

Peter Lammich

doi:10.1007/978-3-031-63498-7_26

Fast and Verified UNSAT Certificate Checking

Peter Lammich^*

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

6 Downloads (Pure)

Abstract

We describe a formally verified checker for unsatisfiability certificates in the LRAT format, which can be run in parallel with the SAT solver, processing the certificate while it is being produced. It is implemented time and memory efficiently, thus increasing the trust in the SAT solver at low additional cost. The verification is done w.r.t. a grammar of the DIMACS format and a semantics of CNF formulas, down to the LLVM code of the checker. In this paper, we report on the checker and its design process using the Isabelle-LLVM stepwise refinement approach.

Original language	English
Title of host publication	Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings
Editors	Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt
Publisher	Springer
Pages	439-457
Number of pages	19
ISBN (Print)	9783031634970
DOIs	https://doi.org/10.1007/978-3-031-63498-7_26
Publication status	Published - 1 Jul 2024
Event	12th International Joint Conference on Automated Reasoning, IJCAR 2024 - Nancy, France Duration: 3 Jul 2024 → 6 Jul 2024 Conference number: 12

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14739 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	12th International Joint Conference on Automated Reasoning, IJCAR 2024
Abbreviated title	IJCAR 2024
Country/Territory	France
City	Nancy
Period	3/07/24 → 6/07/24

Keywords

2025 OA procedure
LRAT
UNSAT certificates
Verified Software
Isabelle-LLVM

Access to Document

10.1007/978-3-031-63498-7_26

978-3-031-63498-7_26Final published version, 473 KBLicence: Taverne

Cite this

Lammich, P. (2024). Fast and Verified UNSAT Certificate Checking. In C. Benzmüller, M. J. H. Heule, & R. A. Schmidt (Eds.), Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings (pp. 439-457). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14739 LNAI). Springer. https://doi.org/10.1007/978-3-031-63498-7_26

Lammich, Peter. / Fast and Verified UNSAT Certificate Checking. Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings. editor / Christoph Benzmüller ; Marijn J. H. Heule ; Renate A. Schmidt. Springer, 2024. pp. 439-457 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{fe1fc7b37475470587d4210581d3dbf3,

title = "Fast and Verified UNSAT Certificate Checking",

abstract = "We describe a formally verified checker for unsatisfiability certificates in the LRAT format, which can be run in parallel with the SAT solver, processing the certificate while it is being produced. It is implemented time and memory efficiently, thus increasing the trust in the SAT solver at low additional cost. The verification is done w.r.t. a grammar of the DIMACS format and a semantics of CNF formulas, down to the LLVM code of the checker. In this paper, we report on the checker and its design process using the Isabelle-LLVM stepwise refinement approach.",

keywords = "2025 OA procedure, LRAT, UNSAT certificates, Verified Software, Isabelle-LLVM",

author = "Peter Lammich",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2024.; 12th International Joint Conference on Automated Reasoning, IJCAR 2024, IJCAR 2024 ; Conference date: 03-07-2024 Through 06-07-2024",

year = "2024",

month = jul,

day = "1",

doi = "10.1007/978-3-031-63498-7_26",

language = "English",

isbn = "9783031634970",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "439--457",

editor = "Christoph Benzm{\"u}ller and Heule, {Marijn J. H.} and Schmidt, {Renate A.}",

booktitle = "Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings",

address = "Germany",

}

Lammich, P 2024, Fast and Verified UNSAT Certificate Checking. in C Benzmüller, MJH Heule & RA Schmidt (eds), Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14739 LNAI, Springer, pp. 439-457, 12th International Joint Conference on Automated Reasoning, IJCAR 2024, Nancy, France, 3/07/24. https://doi.org/10.1007/978-3-031-63498-7_26

Fast and Verified UNSAT Certificate Checking. / Lammich, Peter.
Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings. ed. / Christoph Benzmüller; Marijn J. H. Heule; Renate A. Schmidt. Springer, 2024. p. 439-457 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14739 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Fast and Verified UNSAT Certificate Checking

AU - Lammich, Peter

N1 - Conference code: 12

PY - 2024/7/1

Y1 - 2024/7/1

N2 - We describe a formally verified checker for unsatisfiability certificates in the LRAT format, which can be run in parallel with the SAT solver, processing the certificate while it is being produced. It is implemented time and memory efficiently, thus increasing the trust in the SAT solver at low additional cost. The verification is done w.r.t. a grammar of the DIMACS format and a semantics of CNF formulas, down to the LLVM code of the checker. In this paper, we report on the checker and its design process using the Isabelle-LLVM stepwise refinement approach.

AB - We describe a formally verified checker for unsatisfiability certificates in the LRAT format, which can be run in parallel with the SAT solver, processing the certificate while it is being produced. It is implemented time and memory efficiently, thus increasing the trust in the SAT solver at low additional cost. The verification is done w.r.t. a grammar of the DIMACS format and a semantics of CNF formulas, down to the LLVM code of the checker. In this paper, we report on the checker and its design process using the Isabelle-LLVM stepwise refinement approach.

KW - 2025 OA procedure

KW - LRAT

KW - UNSAT certificates

KW - Verified Software

KW - Isabelle-LLVM

UR - http://www.scopus.com/inward/record.url?scp=85200222011&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-63498-7_26

DO - 10.1007/978-3-031-63498-7_26

M3 - Conference contribution

AN - SCOPUS:85200222011

SN - 9783031634970

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 439

EP - 457

BT - Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings

A2 - Benzmüller, Christoph

A2 - Heule, Marijn J. H.

A2 - Schmidt, Renate A.

PB - Springer

T2 - 12th International Joint Conference on Automated Reasoning, IJCAR 2024

Y2 - 3 July 2024 through 6 July 2024

ER -

Lammich P. Fast and Verified UNSAT Certificate Checking. In Benzmüller C, Heule MJH, Schmidt RA, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Proceedings. Springer. 2024. p. 439-457. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-63498-7_26