ABSTRACT. The implicit hitting set (IHS) approach offers a general framework for solving computationally hard combinatorial optimization problems declaratively by iterating between a decision oracle used for extracting sources of inconsistency and an optimizer for computing so-called hitting sets (HSs) over the accumulated sources of inconsistency. While the decision oracle is language-specific, the optimizer is usually instantiated through an (often commercial, closed-source) integer programming (IP) solver. This makes proof logging in implicit hitting set solvers challenging. Moreover, IP solvers are known to give incorrect results, mostly due to numerical instability. The presented work deals with obtaining reliable hitting set computation in the context of pseudo-Boolean (0--1 IP) optimization. We explore alternative algorithmic techniques for hitting set optimization based on different ways of employing pseudo-Boolean reasoning as well as stochastic local search. Based on earlier work on proof logging for pseudo-Boolean solving using the VeriPB proof system, we obtain the first implicit hitting set solver that is able to produce proofs of optimality of its solution. Our experimental evaluation highlights a trade-off between efficiency and reliability: replacing a commercial IP solver with a pseudo-Boolean solver enhances reliability and gives proof logging possibilities, at the cost of solving efficiency. To mitigate this trade-off, we experimented with different hybrid approaches that differ in when to replace the IP solver by a more reliable, certifying solver.

ABSTRACT. Modern combinatorial solvers are very efficient but also highly complex and therefore error-prone. The most successful approach to ensure correctness is proof logging, now an accepted standard for Boolean satisfiability~(SAT) solving, where solvers emit a machine-verifiable certificate alongside each result. An important technique to make formally verified proof checking efficient is proof trimming: starting from the final verdict and reading the proof backwards, a checker retains only those steps that actually contribute to the conclusion, discarding the rest. Trimming for richer proof systems beyond SAT, however, remains a challenge. In this presentation, we introduce the first trimmer for the full VeriPB proof system, which uses 0-1 integer linear inequalities and enables certification of correctness for a broad range of combinatorial paradigms, including MaxSAT, pseudo-Boolean optimisation, subgraph solving, and constraint programming. Trimming pseudo-Boolean proofs is significantly harder than trimming clausal SAT proofs. For instance, constraints are not always listed explicitly (cutting planes derivations specify how a constraint is derived, but not what it looks like); proof line deletion can be restricted by the proof format; and the redundance-based strengthening rule induces global proof dependencies that can propagate during the backwards pass. Our algorithm proceeds in three passes. A lightweight decoration pass makes implicit proof information explicit, enabling a subsequent backward trimming pass to identify necessary constraints. A final compaction pass writes the trimmed proof. The central novelty is conditional marking: rather than immediately deciding which constraints to keep, the trimmer collects deferred conditions of the form "if C is ultimately needed, then D must be kept too", resolving them lazily at the end of the backwards pass. This cleanly handles the cascading dependencies introduced by strengthening rules without over-approximating the set of required constraints. We evaluate our trimmer on 2656 proof files generated by six solvers, covering SAT solving with symmetry breaking, MaxSAT, pseudo-Boolean optimisation, subgraph solving, and constraint programming. The results demonstrate a 6.37x reduction in proof size and a 1.81x speedup in total checking time, including the overhead of formally verified checking via CakePB. The benefits are particularly pronounced for constraint programming and pseudo-Boolean optimisation proofs, which shrink by factors of 17 and 11 respectively. These results invite further refinement: the marking heuristics used during unit propagation steps are currently using marked propagation first and trail saving. Better strategies (for instance, preferring earlier or stronger constraints, or those with explicit derivations) could yield tighter trimmed proofs. For applications such as proof storage or UNSAT core extraction, one may wish to trade trimming speed for proof minimality, and we discuss the cost-quality tradeoffs that arise in this setting.

ABSTRACT. Modern proof systems for SAT are based on redundancy notions, which ascertain that clauses are safe to derive through a check involving the whole formula currently held by the solver. This global dependency phenomenon, called interference, presents fundamental issues in proof logging within distributed and incremental settings. Recent work leveraged a close connection between redundancy notions and propositional dynamic logic to propose a logical framework that eliminates the issues posed by interference in unsatisfiability proofs. Proofs in this framework, called dynamic proofs, are freely composable, a feature theretofore missing in state-of-the-art proof systems such as DRAT. However, composability is attained by only allowing implicational proofs, which ostensibly forgoes reasoning about satisfiability, a capability required to capture incremental SAT solving. In this work, we overcome this limitation by showing that dynamic proofs can also witness satisfiability without losing composability; in fact, this can be done without augmenting the framework with new rules. To showcase the expressivity of this proof framework, we provide proofs capturing equisatisfiability in models of both incremental and non-incremental SAT. Furthermore, we present an extension through solution programs. With this extension, proofs of equioptimality can be captured as well.

ABSTRACT. Modern proof logging has been highly successful for discrete reasoning, but scientific computation still relies heavily on complex numerical pipelines whose outputs are rarely independently checkable. This talk uses a recent Keller-box computation arising from a Falkner–Skan thermal-flow model by Anwar et al. (2025) as a focused case study for this certification gap. After similarity reduction, the governing equations become a coupled nonlinear boundary-value problem; the final numerical solution is then produced through first-order reformulation, implicit box discretization, Newton linearization and repeated solution of block-tridiagonal linear systems. In such a setting, correctness is not a purely analytic matter: it depends on the fidelity of discretization, the consistency of boundary treatment, the soundness of linearization and the actual convergence behavior of the iterative solver. The talk argues that this solver layer is a natural target for proof logging. Rather than attempting to certify the entire physical model at once, we isolate the computational core and propose a certificate structure for it: logs for the reduced boundary-value problem, machine-checkable witnesses for each discretized system, residual certificates for Newton iterations, explicit verification of boundary-condition satisfaction and auditable checks for the numerical quantities ultimately reported from the computation. The case study also highlights challenges that are specific to numerical reasoning: floating-point effects, truncation of infinite domains, dependence on mesh choice and the need to distinguish empirical convergence from certifiable correctness. The broader aim is to help articulate what a proof-logging discipline for nonlinear scientific solvers should look like. We suggest that numerical workflows of this kind are both important and structurally rich enough to serve as realistic benchmarks for the next generation of certifying algorithms.

ABSTRACT. Reasoning about nonlinear real arithmetic (NRA) is pervasive in safety-critical applications. The applications range from robot motion planning to digital signal processing. Nevertheless, the decision procedures involved are usually highly intricate. The fastest complete algorithms have a doubly exponential lower bound, their implementations are notoriously delicate, and even mature tools occasionally return incorrect results. Given that many applications cannot tolerate unsound answers, it is necessary to develop means for certifying the answers of such algorithms. Two routes are commonly pursued: building a formally verified implementation, or instrumenting an existing solver to produce a machine-checkable proof certificate for every answer. The latter is considerably less intrusive, can be adapted more easily to changes in the solver, and is already the path taken by proof-producing SMT solvers such as cvc5 for theories like linear arithmetic and bit-vectors. Extending this treatment to NRA, however, has remained largely open. In this talk we report on ongoing work to bring proof production --- and independent proof reconstruction --- to four NRA algorithms with very different flavours, all in the context of cvc5 and lean-smt, a Lean tactic capable of reconstructing such proofs in the ITP: - Incremental Linearization (Cimatti et al.). An abstraction-refinement procedure that approximates multiplication by its tangent plane and transcendental functions by their Taylor polynomials. We have instrumented cvc5 to produce proofs for this algorithm, formalized the solver's proof calculus in Lean and extended lean-smt to reconstruct its proofs. The mechanization exposed several missing hypotheses and unsound corner cases in the documented calculus, which the cvc5 team has since addressed. - Cylindrical Algebraic Decomposition (Collins). The fastest known complete decision procedure for NRA, but also the most complex to instrument. We have instrumented cvc5's CAD to to produce proofs for the univariate case, and extended lean-smt so that it is capable of reconstructing such proofs. For achieving this, we had to implement a library of computable real algebraic numbers and to prove Sturm's theorem in Lean. This was inspired by a prior work done in the ITP Isabelle/HOL. We are currently working on the multivariate case. This generalization poses several challenges: formalizing complex proofs of the theorems on which the algorithm is based on; certifying that certain computations were done correctly by cvc5; instrumenting cvc5 to log its reasoning following a novel proof calculus. - Sums of Squares (Parrilo). This method reduces the unsatisfiability of a universally quantified nonlinear formula to finding sums-of-squares decompositions of polynomials via semidefinite programming. Although incomplete, the approach naturally produces a certificate in the form of a polynomial identity, which is very cheap to verify. The main challenge is that semidefinite programming solvers often suffer from numerical imprecision due to floating-point arithmetic; the proof checker must therefore attempt to repair any incorrect certificate. Such certificates have already been explored in prior work within HOL Light. We are investigating this technique as a solver for QF_NRA in cvc5. - Gröbner Basis (Tiwari). Similarly to Sums of Squares, this method aims to find a polynomial that certifies the unsatisfiability of the input formula. The result known as Positivstellensatz guarantees that, under certain conditions, such polynomial must be present in the elements of the Gröbner Basis of the input. This method uses a set of extension rules to force such conditions to be met. It is thus a method complete relative to an oracle, which would decide which extension rule to apply in a given state. Checking the certificate produced by this method also requires tracking the variables introduced by the extension rules and proving a relationship between the produced polynomial (which may have fresh variables) and the input polynomials. We are likewise prototyping it inside cvc5. The four algorithms span a useful dichotomy: incremental linearization and CAD are well-established inside SMT solvers but there are real challenges to check its results; the witness-based methods are more exploratory on the solver side, but the produced certificates have a cheap overhead to be computed and are straightforward to verify.

ABSTRACT. Bit-vector solving is essential to many practical applications of Satisfiability Modulo Theories (SMT) solvers. Currently, most state-of-the-art SMT solvers handle this theory by means of bit-blasting: After simplifications, the input formula is converted into an equisatisfiable formula in propositional logic, which has its satisfiability decided by a SAT solver based on resolution, which is known to handle counting and modular reasoning poorly. Unfortunately, arithmetic bit-vector operators produce large CNF encodings, especially for multiplication, whose refutations can be exponential in size. One alternative is to reason at the word level via polynomial constraints, solved using computer algebra techniques, that can be captured by the Polynomial Calculus (PC). However, this approach does not handle general reasoning well. Pseudo-Boolean (PB) solvers reason with cutting planes, a proof system that can polynomially simulate resolution and is exponentially stronger on some of the arithmetic structure of bit-vectors, while avoiding the difficulties PC has with bit-level reasoning. This suggests that converting bit-vector constraints into PB constraints rather than propositional clauses could yield smaller proofs and potentially faster solving. An analogous strategy of translating bit-vectors into integer arithmetic has already shown such gains on increasing bit-widths. Liew et al. proposed an approach to verify properties of bit-vector multiplication based on pseudo-Booleans, via cutting-planes proofs, presenting a construction of optimal polynomial-size proofs for a class of bit-vector multiplicative identities. In this work, we plan to extend this approach to the context of SMT solving by developing a novel proof-producing decision procedure based on blasting to PB constraints, leveraging external PB solvers. We are implementing this in the cvc5 SMT solver, building on its extensive infrastructure for proof logging, which produces proofs in the Cooperating Proof Calculus (CPC) and Alethe proof formats; as the PB solver we use RoundingSat, which produces cutting-planes proofs in the veriPB format. So far we translate all operators of the fixed-size bit-vector theory of SMT-LIB except bit-shifts, division and remainder, discharging the resulting constraints to RoundingSat. Proofs of the decision procedure will combine cutting-planes reasoning with a justification of each translation step to PB constraints; we are extending Alethe and CPC to capture them, and their respective proof checkers Carcara and Ethos to verify them. In the talk we will detail the encoding strategy used for the operators we already cover, the obstacles posed by bit-shifts, division and remainder, and how the cutting-planes proofs produced by RoundingSat can be lifted into Alethe and CPC for checking by Carcara and Ethos.

ABSTRACT. The effectiveness of SAT solvers depends critically on how constraints are encoded into conjunctive normal form (CNF). Two logically equivalent encodings of the same problem can differ by orders of magnitude in solving performance. However, constructing effective encodings often requires substantial expertise, making SAT technology difficult to use reliably in practice. To address this problem, a wide range of reencoding techniques have been developed that transform formulas into representations exposing stronger propagation, improved simplification opportunities, or additional structural information. Unfortunately, most existing proof systems are designed for clause-level reasoning and provide only limited support for certifying such higher-level transformations. Several examples illustrate the need for proof-producing reencoding. First, the way XOR constraints are encoded as CNF can have a surprisingly large impact on SAT-solving performance. Even subtle changes in recursive encodings can lead to substantial performance differences. In particular, placing auxiliary variables at the beginning versus the end of the recursion, often referred to as linear and pooled encodings, respectively, can strongly affect solver behavior. Such transformations are difficult to justify compactly because they replace one structured encoding by another while preserving equivalence only over the original variables. Second, the effectiveness of cardinality encodings depends not only on the chosen encoding scheme, but also on how literals are ordered within the constraint. Recent work has shown that sorting literals prior to encoding can substantially improve SAT solving performance by exposing additional structure to propagation and simplification. Although such sorting transformations preserve the semantics of the original constraint, they are difficult to validate in existing proof systems because the resulting encoding may differ globally from the original one. In particular, the transformation changes the interaction between auxiliary variables and the input literals while preserving equivalence only over the original variables. This highlights the need for proof systems that can certify semantic-preserving reencodings with higher-level constraints. Third, symmetry breaking in SAT is constrained by what is visible in the CNF formula. When higher-level constraints such as cardinality or XOR constraints are encoded into CNF, auxiliary variables may obscure the symmetries of the original problem. As a consequence, symmetry-breaking techniques operating only at the CNF level may fail to detect important structural symmetries that were present before encoding. This talk argues that the widespread use of CNF as the standard SAT benchmark format creates a fundamental tension between solver performance and trustworthiness. Many effective preprocessing and reencoding techniques rely on recovering higher-level structure from CNF formulas, such as XOR or cardinality constraints, and then transforming these constraints into more solver-friendly representations. However, these transformations raise important certification questions. Should CNF formulas be lifted into richer high-level representations together with corresponding proof objects? If so, how can these high-level representations and proofs be translated back into CNF-level certificates that can be checked independently? Alternatively, should correctness be justified directly at the CNF level without introducing higher-level abstractions? This talk addresses these questions and discusses possible directions for integrating proof logging, reencoding, and high-level reasoning into trustworthy SAT-solving pipelines.

ABSTRACT. Pseudo-Boolean proof logging is now being used for a wide range of problems that are not naturally pseudo-Boolean. This is very useful for verifying complex algorithmic and reasoning steps being carried out by solvers, but there is still an encoding gap: why should we trust that the pseudo-Boolean model means the same thing as whatever problem the user cares about? And, for that matter, does the solution as expressed over Boolean variables correspond to the high-level solution that we claim? For a variety of subgraph-finding problems, Gocht et al. introduced end-to-end verification, starting with a HOL description of the problem and verifying the meaning of the output in graph terms. There, the final verification theorem does not mention the pseudo-Boolean intermediaries or how the VeriPB proof system works. In this talk, we discuss what it would take to get a similar process to work for constraint programming, building upon the VeriPB proof logging methodology introduced in the Glasgow Constraint Solver. We will explain what we are aiming for and why we want it; why the problem is complicated; how we've chosen to try to address it; and what remains to be done. Ultimately, we would like to be able to go from human-understandable problem statements written in several domain-specific languages, all the way to solutions, whilst having extremely strong guarantees that the solutions are correct.

ABSTRACT. Recently, we have seen many advances in proof logging methods for CP solvers. However, by design, proof logging is agnostic to how the solver produces a proof. For example, it does not verify that an individual propagator achieves its advertised level of consistency. This potential source of bugs may lead to misleading empirical conclusions about new propagation algorithms. We propose a runtime certification framework to address this gap. Propagators emit certificates that justify both the retention and the removal of values in domains. These certificates are checked at runtime by checkers that are significantly simpler than the propagation algorithms. We make the existential definitions of consistency levels constructive. At fixpoint, a propagator must be able to produce a witness for any relevant value (bounds for bounds-consistency; domain values for domain-consistency). If it cannot provide a witness for a specific value, it did not propagate to its advertised consistency level. To certify removal of values, every value removal and conflict must be accompanied by an explanation. Explanations are checked for soundness and applicability (i.e., whether they are applicable in the current state). This is closely related to checking a proof step, but done at runtime against the live solver state rather than post-hoc. Finally, we introduce the notion of weak consistency for propagators that are neither bounds- nor domain-consistent (e.g., timetabling for cumulative, prevent-and-check for circuit). A weakly-consistent propagator removes those values that, when assigned to a variable, trigger a detectable conflict. This gives us a verifiable property applicable to many practical propagators that previously lacked consistency properties. We implemented propagation certificates in Pumpkin, with checkers for linear inequality, maximum, element, cumulative (timetabling), and circuit (prevent-and-check). Enabling all checkers results in a 1–2 order-of-magnitude slowdown in our experiments. However, only running checkers for a single propagator type (the realistic development scenario) substantially reduces this overhead. Using this framework, we identified and fixed several consistency bugs in propagators in Pumpkin. In addition, manually injected off-by-one mutations were also caught within one second of solve time.

ABSTRACT. In this talk, I will present a generalisation of conflict-driven clause learning (CDCL) for constraint programming over abstract domains. A core idea in constraint programming is propagation: each constraint has an associated algorithm that during search prunes potential non-solutions. The abstract theory of constraint propagators as idempotent, monotonic, contracting functions over partial orders has led to the development of propagators and solvers over non-integer domains, such as strings, sets or floating point numbers. Building on this theory, I introduce a generalisation of reasons, explanations, and implication graphs from CDCL to propagation-based solving over abstract domains. A central result shows that cuts in the implication graph are no-goods. An abstract scheme is presented that unifies CDCL solving from SAT and lazy-clause search from constraint programming. This work is a first step to generalising proof logging for abstract domains in constraint programming.

ABSTRACT. A constraint programming (CP) solver that implements proof logging will output a machine-checkable certificate of correctness alongside any result it obtains. This is useful for trusting claims of unsatisfiability or optimality, as well as for debugging and auditing solver implementations. Proofs can be constructed by having the solver log justifications for each inference it makes, and previous work has shown that many standard CP reasoning techniques can be efficiently justified using a pseudo-Boolean (PB) proof format. Multiplication constraints of the form $X \times Y = Z$ are a fundamental primitive for CP modelling, but they pose a unique challenge for PB proof logging, given their non-linear nature. In this talk, I will present an overview of how multiplication constraints can be encoded as $0$-$1$-linear inequalities, and then how bounds-consistent reasoning can be justified using the \emph{VeriPB} proof format. We will see that this is possible to achieve, but comes with significant costs in terms of proof logging and checking overhead. I will then discuss what this means for certified CP more broadly, and some ideas for making PB proofs of this nature more usable and efficiently checkable in practice. This talk will be mostly based on the previously published paper, "Certifying Bounds Propagation for Integer Multiplication Constraints" and a short version was presented at AAAI in 2025.