11 Search Results for "Preiner, Mathias"

Document
DOI: 10.4230/LIPIcs.ITP.2025.1
A Certified Proof Checker for Deep Neural Network Verification in Imandra

Authors: Remi Desmartin, Omri Isac, Grant Passmore, Ekaterina Komendantskaya, Kathrin Stark, and Guy Katz

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Recent advances in the verification of deep neural networks (DNNs) have opened the way for a broader usage of DNN verification technology in many application areas, including safety-critical ones. However, DNN verifiers are themselves complex programs that have been shown to be susceptible to errors and numerical imprecision; this, in turn, has raised the question of trust in DNN verifiers. One prominent attempt to address this issue is enhancing DNN verifiers with the capability of producing certificates of their results that are subject to independent algorithmic checking. While formulations of Marabou certificate checking already exist on top of the state-of-the-art DNN verifier Marabou, they are implemented in C++, and that code itself raises the question of trust (e.g., in the precision of floating point calculations or guarantees for implementation soundness). Here, we present an alternative implementation of the Marabou certificate checking in Imandra - an industrial functional programming language and an interactive theorem prover (ITP) - that allows us to obtain full proof of certificate correctness. The significance of the result is two-fold. Firstly, it gives stronger independent guarantees for Marabou proofs. Secondly, it opens the way for the wider adoption of DNN verifiers in interactive theorem proving in the same way as many ITPs already incorporate SMT solvers.
Cite as

Remi Desmartin, Omri Isac, Grant Passmore, Ekaterina Komendantskaya, Kathrin Stark, and Guy Katz. A Certified Proof Checker for Deep Neural Network Verification in Imandra. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{desmartin_et_al:LIPIcs.ITP.2025.1,
  author =	{Desmartin, Remi and Isac, Omri and Passmore, Grant and Komendantskaya, Ekaterina and Stark, Kathrin and Katz, Guy},
  title =	{{A Certified Proof Checker for Deep Neural Network Verification in Imandra}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{1:1--1:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.1},
  URN =		{urn:nbn:de:0030-drops-246000},
  doi =		{10.4230/LIPIcs.ITP.2025.1},
  annote =	{Keywords: Neural Network Verification, Farkas Lemma, Proof Certification}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.26
Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL

Authors: Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Sledgehammer is a tool that increases the level of automation in the Isabelle/HOL proof assistant by asking external automatic theorem provers (ATPs), including SMT solvers, to prove the current goal. When the external ATP succeeds it must provide enough evidence that the goal holds for Isabelle to be able to reprove it internally based on that evidence. In particular, Isabelle can do this by replaying fine-grained proof certificates from proof-producing SMT solvers as long as they are expressed in the Alethe format, which until now was supported only by the veriT SMT solver. We report on our experience adding proof reconstruction support for the cvc5 SMT solver in Isabelle by extending cvc5 to produce proofs in the Alethe format and then adapting Isabelle to reconstruct those proofs. We discuss several difficulties and pitfalls we encountered and describe a set of tools and techniques we developed to improve the process. A notable outcome of this effort is that Isabelle can now be used as an independent proof checker for SMT problems written in the SMT-LIB standard. We evaluate cvc5’s integration on a set of SMT-LIB benchmarks originating from Isabelle as well as on a set of Isabelle proofs. Our results confirm that this integration complements and improves Sledgehammer’s capabilities.
Cite as

Hanna Lachnitt, Mathias Fleury, Haniel Barbosa, Jibiana Jakpor, Bruno Andreotti, Andrew Reynolds, Hans-Jörg Schurr, Clark Barrett, and Cesare Tinelli. Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 26:1-26:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{lachnitt_et_al:LIPIcs.ITP.2025.26,
  author =	{Lachnitt, Hanna and Fleury, Mathias and Barbosa, Haniel and Jakpor, Jibiana and Andreotti, Bruno and Reynolds, Andrew and Schurr, Hans-J\"{o}rg and Barrett, Clark and Tinelli, Cesare},
  title =	{{Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{26:1--26:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.26},
  URN =		{urn:nbn:de:0030-drops-246243},
  doi =		{10.4230/LIPIcs.ITP.2025.26},
  annote =	{Keywords: interactive theorem proving, proof assistants, Isabelle/HOL, SMT, certification, proof certificates, proof reconstruction, proof automation}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.ITP.2025.38
Sledgehammering Without ATPs (Short Paper)

Authors: Martin Desharnais and Jasmin Blanchette

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
We describe an alternative architecture for "hammers," inspired by Magnushammer, in which proofs are found by the proof assistant’s built-in automation instead of by external automatic theorem provers (ATPs). We implemented this approach in Isabelle’s Sledgehammer and evaluated it. The new ATP-free approach nicely complements the traditional Sledgehammer. The two approaches in combination solve more goals than the traditional ATP-based approach alone.
Cite as

Martin Desharnais and Jasmin Blanchette. Sledgehammering Without ATPs (Short Paper). In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 38:1-38:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{desharnais_et_al:LIPIcs.ITP.2025.38,
  author =	{Desharnais, Martin and Blanchette, Jasmin},
  title =	{{Sledgehammering Without ATPs}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{38:1--38:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.38},
  URN =		{urn:nbn:de:0030-drops-246366},
  doi =		{10.4230/LIPIcs.ITP.2025.38},
  annote =	{Keywords: Interactive theorem proving, proof assistants, proof automation}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2025.56
Negated String Containment Is Decidable

Authors: Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál

Published in: LIPIcs, Volume 345, 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Abstract
We provide a positive answer to a long-standing open question of the decidability of the not-contains string predicate. Not-contains is practically relevant, for instance in symbolic execution of string manipulating programs. Particularly, we show that the predicate ¬Contains(x₁ … x_n, y₁ … y_m), where x₁ … x_n and y₁ … y_m are sequences of string variables constrained by regular languages, is decidable. Decidability of a not-contains predicate combined with chain-free word equations and regular membership constraints follows.
Cite as

Vojtěch Havlena, Michal Hečko, Lukáš Holík, and Ondřej Lengál. Negated String Containment Is Decidable. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 345, pp. 56:1-56:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{havlena_et_al:LIPIcs.MFCS.2025.56,
  author =	{Havlena, Vojt\v{e}ch and He\v{c}ko, Michal and Hol{\'\i}k, Luk\'{a}\v{s} and Leng\'{a}l, Ond\v{r}ej},
  title =	{{Negated String Containment Is Decidable}},
  booktitle =	{50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)},
  pages =	{56:1--56:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-388-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{345},
  editor =	{Gawrychowski, Pawe{\l} and Mazowiecki, Filip and Skrzypczak, Micha{\l}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2025.56},
  URN =		{urn:nbn:de:0030-drops-241631},
  doi =		{10.4230/LIPIcs.MFCS.2025.56},
  annote =	{Keywords: not-contains, string constraints, word combinatorics, primitive word}
}
Document
DOI: 10.4230/LIPIcs.CP.2025.21
Practically Feasible Proof Logging for Pseudo-Boolean Optimization

Authors: Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Certifying solvers have long been standard for decision problems in Boolean satisfiability (SAT), allowing for proof logging and checking with very limited overhead, but developing similar tools for combinatorial optimization has remained a challenge. A recent promising approach covering a wide range of solving paradigms is pseudo-Boolean proof logging, but this has mostly consisted of proof-of-concept works far from delivering the performance required for real-world deployment. In this work, we present an efficient toolchain based on VeriPB and CakePB for formally verified pseudo-Boolean optimization. We implement proof logging for the full range of techniques in the state-of-the-art solvers RoundingSat and Sat4j, including core-guided search and linear programming integration with Farkas certificates and cut generation. Our experimental evaluation shows that proof logging and checking performance in this much more expressive paradigm is now quite close to the level of SAT solving, and hence is clearly practically feasible.
Cite as

Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals. Practically Feasible Proof Logging for Pseudo-Boolean Optimization. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 21:1-21:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{koops_et_al:LIPIcs.CP.2025.21,
  author =	{Koops, Wietze and Le Berre, Daniel and Myreen, Magnus O. and Nordstr\"{o}m, Jakob and Oertel, Andy and Tan, Yong Kiam and Vinyals, Marc},
  title =	{{Practically Feasible Proof Logging for Pseudo-Boolean Optimization}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{21:1--21:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.21},
  URN =		{urn:nbn:de:0030-drops-238825},
  doi =		{10.4230/LIPIcs.CP.2025.21},
  annote =	{Keywords: proof logging, certifying algorithms, combinatorial optimization, certification, pseudo-Boolean solving, 0-1 integer linear programming}
}
Document
Short Paper
DOI: 10.4230/LIPIcs.CP.2025.42
Towards Modern and Modular SAT for LCG (Short Paper)

Authors: Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Lazy Clause Generation (LCG) is an architecture for building Constraint Programming (CP) solvers using an underlying Boolean Satisfiability (SAT) engine. The CP propagation engine lazily creates clauses that define the integer variables and impose problem restrictions. The SAT engine uses the clausal model to reason and search, including, crucially, the generation of nogoods. However, while SAT solving has made significant advances recently, the underlying SAT technology in most LCG solvers has largely remained the same. Using a new interface to SAT engines, IPASIR-UP, we can construct an LCG solver which can swap out the underlying SAT engine with any that supports the interface. This new approach means we need to revisit many of the design and engineering decisions for LCG solvers, to take maximum advantage of a better underlying SAT engine while adhering to the restrictions of the interface. In this paper, we explore the possibilities and challenges of using IPASIR-UP for LCG, showing that it can be used to create a highly competitive solver.
Cite as

Jip J. Dekker, Alexey Ignatiev, Peter J. Stuckey, and Allen Z. Zhong. Towards Modern and Modular SAT for LCG (Short Paper). In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 42:1-42:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{dekker_et_al:LIPIcs.CP.2025.42,
  author =	{Dekker, Jip J. and Ignatiev, Alexey and Stuckey, Peter J. and Zhong, Allen Z.},
  title =	{{Towards Modern and Modular SAT for LCG}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{42:1--42:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.42},
  URN =		{urn:nbn:de:0030-drops-239038},
  doi =		{10.4230/LIPIcs.CP.2025.42},
  annote =	{Keywords: Lazy Clause Generation, Boolean Satisfiability, IPASIR-UP}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.4
Bit-Precise Reasoning with Parametric Bit-Vectors

Authors: Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
The SMT-LIB theory of bit-vectors is restricted to bit-vectors of fixed width. However, several important applications can benefit from reasoning about bit-vectors of symbolic widths, i.e., parametric bit-vectors. Recent work has introduced an approach for solving formulas over parametric bit-vectors, via an eager translation to quantified integer arithmetic with uninterpreted functions. The approach was shown to be successful for several applications, including the bit-width independent verification of compiler optimizations, invertibility conditions, and rewrite rules. We extend and improve that approach in several aspects. Theoretically, we improve expressiveness by defining a new theory of parametric bit-vectors that supports more operators and allows reasoning about the bit-widths themselves. Algorithmically, we introduce a lazy algorithm that avoids the use of uninterpreted functions and quantified axioms for them. Empirically, we show a significant improvement by implementing and evaluating our approach, and comparing it experimentally to the previous one.
Cite as

Zvika Berger, Yoni Zohar, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett, and Cesare Tinelli. Bit-Precise Reasoning with Parametric Bit-Vectors. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 4:1-4:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{berger_et_al:LIPIcs.SAT.2025.4,
  author =	{Berger, Zvika and Zohar, Yoni and Niemetz, Aina and Preiner, Mathias and Reynolds, Andrew and Barrett, Clark and Tinelli, Cesare},
  title =	{{Bit-Precise Reasoning with Parametric Bit-Vectors}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{4:1--4:24},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.4},
  URN =		{urn:nbn:de:0030-drops-237385},
  doi =		{10.4230/LIPIcs.SAT.2025.4},
  annote =	{Keywords: Satisfiability Modulo Theories, Bit-precise Reasoning, Parametric Bit-vectors}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.25
QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms

Authors: Mark Peyrer and Martina Seidl

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
Q-resolution is a proof system for quantified Boolean formulas (QBFs) that forms the foundation for search-based QBF solvers with clause and cube learning. To derive stronger clauses and cubes, Q-resolution was extended with so-called generalized axioms. The derivation of such generalized axioms relies on solving oracles that could be, for example, SAT solvers or even QBF solvers. While the correctness of results obtained with classical QCDCL-based solving can be efficiently certified by an independent checker, until now, proof generation had to be turned off to benefit from generalized axioms. Consequently, the results obtained with reasoning under generalized axioms could not be certified independently. To overcome this restriction, we present QRP+Gen, a novel framework to automatically generate and check Q-resolution proofs that contain generalized axioms. To this end, we extended the Q-resolution format QRP such that all necessary information is included to verify the correctness of generalized axioms. Our extension allows to integrate certificates produced by any oracle which can produce automatically checkable proofs. Furthermore, we developed a proof checker that orchestrates the proof checking of the core Q-resolution proof and the proofs produced by the oracles. As a case study, we equipped the search-based QBF solver DepQBF with proof-producing oracles for the SAT-based techniques trivial truth and trivial falsity.
Cite as

Mark Peyrer and Martina Seidl. QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 25:1-25:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{peyrer_et_al:LIPIcs.SAT.2025.25,
  author =	{Peyrer, Mark and Seidl, Martina},
  title =	{{QRP+Gen: A Framework for Checking Q-Resolution Proofs with Generalized Axioms}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{25:1--25:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.25},
  URN =		{urn:nbn:de:0030-drops-237592},
  doi =		{10.4230/LIPIcs.SAT.2025.25},
  annote =	{Keywords: Automated Reasoning, Quantified Resolution Proof, Generalized Axioms}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.24
SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints

Authors: Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, and Naoyuki Tamura

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
In this paper, we propose an enhancement to the SAT-based counterexample-guided abstraction refinement (CEGAR) approach for solving the Hamiltonian Cycle Problem (HCP). Many SAT-based methods for HCP have been proposed, including a CEGAR-based method that repeatedly solves a relaxed version of HCP strengthened by counterexamples. However, when the counterexample space - represented by the full set of subcycle partitions - is large, it becomes difficult to find a solution. To address this, we introduce cut-set constraints in the refinement step, replacing traditional subcycle blocking constraints. Our evaluation shows that these cut-set constraints achieve equal or better reduction in the counterexample space, making it easier to find valid solutions. We further assessed performance using all 1001 instances from the FHCP challenge set and confirmed that the proposed method solved 937 instances within 1800 seconds, outperforming both the existing eager and CEGAR encodings (which solved at most 666 instances). This demonstrates the effectiveness of incorporating cut-set constraints into SAT-based CEGAR approaches.
Cite as

Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, and Naoyuki Tamura. SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ohashi_et_al:LIPIcs.SAT.2025.24,
  author =	{Ohashi, Ryoga and Soh, Takehide and Le Berre, Daniel and Nabeshima, Hidetomo and Banbara, Mutsunori and Inoue, Katsumi and Tamura, Naoyuki},
  title =	{{SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{24:1--24:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.24},
  URN =		{urn:nbn:de:0030-drops-237585},
  doi =		{10.4230/LIPIcs.SAT.2025.24},
  annote =	{Keywords: Hamiltonian Cycle Problem, SAT Encoding, CEGAR}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.SAT.2024.2
Scalable Proof Production and Checking in SMT (Invited Talk)

Authors: Cesare Tinelli

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Solvers for Satisfiability Modulo Theories (SMT) have become crucial components in safety- or mission-critical formal methods applications, in particular model checking, verification, and security analysis. Since state-of-the-art SMT solvers are large and complex systems, they are prohibitively difficult to prove correct. Hence, proof production is essential as a way to demonstrate instead the correctness of their responses, making those responses amenable to independent verification. Historically, the main challenges for proof production in SMT have been solver performance and proof coverage, often leading to the disabling of many sophisticated solving techniques when running in proof-production mode, or to coarse-grained, and harder to check, proofs. The first part of this talk presents a flexible proof-production architecture designed to handle the complexity of versatile, industrial-strength SMT solvers, and discusses how it has been leveraged to produce detailed proofs, even for sophisticated reasoning components. The architecture, implemented in the state-of-the-art SMT solver cvc5, allows proofs to be produced modularly, as needed, and with various safeguards for correctness. The architecture supports the generation of textual proof certificates in different formats, for offline proof checking by external tools, as well as a rich API, which is useful for online integration of the SMT solver into other reasoning tools such as, for instance, skeptical proof assistants. Extensive experimental evaluations with both SMT-LIB benchmarks and benchmarks provided by industrial partners have shown that the new architecture results in greater proof coverage than previous approaches, imposes a small runtime overhead, and supports fine-grained proofs in the great majority of cases. The second part of the talk gives an overview of a new generic language for expressing SMT proof certificates that builds on almost two decades of work and experience in proof generation and checking in SMT and combines the benefits of several previous efforts on the topic. While developed to express cvc5’s proof certificates, the language is meant to be useful to other SMT solvers as well. It is in fact a logical framework, based on the syntax and semantics of the upcoming Version 3 of the SMT-LIB standard, that can be customized, as in the case of cvc5, with the specific proof system used by the solver through the definition of new symbols, binders and proof rules. In addition, it features an intuitive syntax for representing natural-deduction-style proofs and the ability to integrate other proof formats (such as, for instance, those currently used by SAT solvers) via the use of oracles. The talk discusses an initial evaluation of the proof language, obtained with a companion checker for it and an instantiation to cvc5’s proof system. The evaluation shows the viability of high-performance, fine-grained proof production and checking for SMT. The talk concludes with a brief overview of future work and new potential applications enabled by scalable proof certificate production and checking.
Cite as

Cesare Tinelli. Scalable Proof Production and Checking in SMT (Invited Talk). In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 2:1-2:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{tinelli:LIPIcs.SAT.2024.2,
  author =	{Tinelli, Cesare},
  title =	{{Scalable Proof Production and Checking in SMT}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{2:1--2:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.2},
  URN =		{urn:nbn:de:0030-drops-205241},
  doi =		{10.4230/LIPIcs.SAT.2024.2},
  annote =	{Keywords: Satisfiability Modulo Theories, Proof generation and certification}
}
Document
DOI: 10.4230/LIPIcs.SAT.2023.8
IPASIR-UP: User Propagators for CDCL

Authors: Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract
Modern SAT solvers are frequently embedded as sub-reasoning engines into more complex tools for addressing problems beyond the Boolean satisfiability problem. Examples include solvers for Satisfiability Modulo Theories (SMT), combinatorial optimization, model enumeration and counting. In such use cases, the SAT solver is often able to provide relevant information beyond the satisfiability answer. Further, domain knowledge of the embedding system (e.g., symmetry properties or theory axioms) can be beneficial for the CDCL search, but cannot be efficiently represented in clausal form. In this paper, we propose a general interface to inspect and influence the internal behaviour of CDCL SAT solvers. Our goal is to capture the most essential functionalities that are sufficient to simplify and improve use cases that require a more fine-grained interaction with the SAT solver than provided via the standard IPASIR interface. For our experiments, we extend CaDiCaL with our interface and evaluate it on two representative use cases: enumerating graphs within the SAT modulo Symmetries framework (SMS), and as the main CDCL(T) SAT engine of the SMT solver cvc5.
Cite as

Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere. IPASIR-UP: User Propagators for CDCL. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 8:1-8:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{fazekas_et_al:LIPIcs.SAT.2023.8,
  author =	{Fazekas, Katalin and Niemetz, Aina and Preiner, Mathias and Kirchweger, Markus and Szeider, Stefan and Biere, Armin},
  title =	{{IPASIR-UP: User Propagators for CDCL}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{8:1--8:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.8},
  URN =		{urn:nbn:de:0030-drops-184709},
  doi =		{10.4230/LIPIcs.SAT.2023.8},
  annote =	{Keywords: SAT, CDCL, Satisfiability Modulo Theories, Satisfiability Modulo Symmetries}
}
  • Refine by Type
  • 11 Document/PDF
  • 9 Document/HTML

  • Refine by Publication Year
  • 9 2025
  • 1 2024
  • 1 2023

  • Refine by Author
  • 3 Tinelli, Cesare
  • 2 Barrett, Clark
  • 2 Le Berre, Daniel
  • 2 Niemetz, Aina
  • 2 Preiner, Mathias
  • Show More...

  • Refine by Series/Journal
  • 11 LIPIcs

  • Refine by Classification
  • 7 Theory of computation → Automated reasoning
  • 5 Theory of computation → Logic and verification
  • 2 Mathematics of computing → Combinatorial optimization
  • 1 Computing methodologies → Discrete space search
  • 1 Computing methodologies → Neural networks
  • Show More...

  • Refine by Keyword
  • 3 Satisfiability Modulo Theories
  • 2 certification
  • 2 proof assistants
  • 2 proof automation
  • 1 0-1 integer linear programming
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact