Abstract The Model Constructing Satisfiability (MCSat) approach to the SMT problem extends the ideas of CDCL from the SAT level to the theory level. Like SAT, its search is driven by incrementally constructing a model by assigning concrete values to theory variables and performing theory-level reasoning to learn lemmas when conflicts arise. Therefore, the selection of values can significantly impact the search process and the solver’s performance. In this work, we propose guiding the MCSat search by utilizing assignment values discovered through local search. First, we present a theory-agnostic framework to seamlessly integrate local search techniques within the MCSat framework. Then, we highlight how to use the framework to design a search procedure for (quantifier-free) Nonlinear Integer Arithmetic ( $$\mathcal {NIA}$$ NIA ), utilizing accelerated hill-climbing and a new operation called feasible-sets jumping . We implement the proposed approach in the MCSat engine of the Yices2 solver, and empirically evaluate its performance over the $$\mathcal {NIA}$$ NIA benchmarks of SMT-LIB.

Abstract The Model Constructing Satisfiability (MCSat) approach to Satisfiability Modulo Theories (SMT) has demonstrated strong performance when handling complex theories such as nonlinear arithmetic. Despite being in development for over a decade, there has been limited research on the heuristics utilized by MCSat solvers as in Yices2. In this paper, we discuss the decision heuristics employed in the MCSat approach of Yices2 and empirically show their significance on QF_NRA and QF_NIA benchmarks. Additionally, we propose new ideas to enhance these heuristics by leveraging theory-specific reasoning and drawing inspiration from recent advancements in SAT solvers. Our new version of the MCSat Yices2 solver not only solves more nonlinear arithmetic benchmarks than before but is also more efficient compared to other leading SMT solvers.

Abstract Deciding the satisfiability of formulas involving both quantifiers and theory defined symbols is a challenge in automated reasoning. This article presents an algorithm, called $$\textsf{QSMA}$$ QSMA (Quantified Satisfiability Modulo Assignment), for the satisfiability of an arbitrary quantified formula modulo a complete theory and an initial assignment. The algorithm is proved partially correct and terminating, so that its total correctness is established. An optimized variant called $$\textsf{OptiQSMA}$$ OptiQSMA is also described and shown to preserve both partial correctness and termination. $$\textsf{OptiQSMA}$$ OptiQSMA is implemented in the YicesQS solver. $$\textsf{OptiQSMA}$$ OptiQSMA enabled YicesQS to achieve top of the line results, especially in linear rational arithmetic, in the 2022, 2023, and 2024 editions of the International Satisfiability Modulo Theories Competition (SMT-COMP). A report on these results in four fragments of arithmetic ( $$\textsf{LRA}$$ LRA —Linear Rational Arithmetic, $$\textsf{LIA}$$ LIA —Linear Integer Arithmetic, $$\textsf{NRA}$$ NRA —Nonlinear Real Arithmetic, and $$\textsf{NIA}$$ NIA —Nonlinear Integer Arithmetic) and in the theory of bitvectors ( $$\textsf{BV}$$ BV ) is included.

Abstract This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits into the model-constructing satisfiability (MCSat) framework and is based on zero decomposition techniques, which find finite basis explanations for theory conflicts over finite fields. As the MCSat solver within Yices2 can support (and combine) several theories via theory plugins, we implemented our reasoning approach as a new plugin for finite fields and extended Yices2 ’s frontend to parse finite field problems, making our implementation the first MCSat-based reasoning engine for finite fields. We present its evaluation on finite field benchmarks, comparing it against cvc5. Additionally, our work leverages the modular architecture of the MCSat solver in Yices2 to provide a foundation for the rapid implementation of further reasoning techniques for this theory.

Abstract This paper presents and proves totally correct a new algorithm, called $$\textsf{QSMA}$$ QSMA , for the satisfiability of a quantified formula modulo a complete theory and an initial assignment. The optimized variant of $$\textsf{QSMA}$$ QSMA implemented in YicesQS is described and shown to preserve total correctness. A report on the performance of YicesQS at the 2022 SMT competition is included. YicesQS ran in the $$\textsf{LIA}$$ LIA , $$\textsf{NIA}$$ NIA , $$\textsf{LRA}$$ LRA , $$\textsf{NRA}$$ NRA , and $$\textsf{BV}$$ BV categories and ranked second for the “largest contribution” award (single queries). It was the only solver to solve all $$\textsf{LRA}$$ LRA instances, where it was about two orders of magnitude faster than the second best solver (Z3).

Despite the notable advances in the development of high-assurance, verified implementations of cryptographic protocols, such implementations typically face significant performance overheads, particularly due to the penalties induced by formal verification and automated extraction of executable code. In this paper, we address some core performance challenges facing computer-aided cryptography by presenting a formal treatment for accelerating such verified implementations based on multiple generic optimizations covering parallelism and memory access. We illustrate our techniques for addressing such performance bottlenecks using the Line-Point Zero-Knowledge (LPZK) protocol as a case study. Our starting point is a new verified implementation of LPZK that we formalize and synthesize using EasyCrypt; our first implementation is developed to reduce the proof effort and without considering the performance of the extracted executable code. We then show how such (automatically) extracted code can be optimized in three different ways to obtain a 3000x speedup and thus matching the performance of the manual implementation of LPZK of lpzkv2.[13] We obtain such performance gains by first modifying the algorithmic specifications, then by adopting a provably secure parallel execution model, and finally by optimizing the memory access structures. All optimizations are first formally verified inside EasyCrypt, and then executable code is automatically synthesized from each step of the formalization. For each optimization, we analyze performance gains resulting from it and also address challenges facing the computer-aided security proofs thereof, and challenges facing automated synthesis of executable code with such an optimization.

Abstract Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input.Conflict-drivenprocedures perform non-trivial inferences only when resolving conflicts between formulæ and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning inunions of theories. It combines inference systems for individual theories astheory moduleswithin a solver for the union of the theories. This article augments CDSAT with a more generallemma learningcapability and withproof generation. Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements forcompletenessandterminationof CDSAT. Proof generation is accomplished by aproof-carryingversion of the CDSAT transition system that producesproof objectsin memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT theLCF approach to proofsfrom interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs.

MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH.

Abstract Multi types – aka non-idempotent intersection types – have been used. to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of the result. Recent results show that the number of steps can be taken as a reasonable time complexity measure. At the same time, however, these results suggest that multi types provide quite lax complexity bounds, because the size of the result can be exponentially bigger than the number of steps. Starting from this observation, we refine and generalise a technique introduced by Bernadet and Graham-Lengrand to provide exact bounds. Our typing judgements carry counters, one measuring evaluation lengths and the other measuring result sizes. In order to emphasise the modularity of the approach, we provide exact bounds for four evaluation strategies, both in the λ -calculus (head, leftmost-outermost, and maximal evaluation) and in the linear substitution calculus (linear head evaluation). Our work aims at both capturing the results in the literature and extending them with new outcomes. Concerning the literature, it unifies de Carvalho and Bernadet & Graham-Lengrand via a uniform technique and a complexity-based perspective. The two main novelties are exact split bounds for the leftmost strategy – the only known strategy that evaluates terms to full normal forms and provides a reasonable complexity measure – and the observation that the computing device hidden behind multi types is the notion of substitution at a distance, as implemented by the linear substitution calculus.

Search-based satisfiability procedures try to construct a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. When the formulae are satisfiable, these procedures generate a model as a witness. Dually, it is desirable to have a proof when the formulae are unsatisfiable. Conflict-driven procedures perform nontrivial inferences only when resolving conflicts between the formulae and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in combinations of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this paper we endow CDSAT with lemma learning and proof generation. For the latter, we present two techniques. The first one produces proof objects in memory: it assumes that all theory modules produce proof objects and it accommodates multiple proof formats. The second technique adapts the LCF approach to proofs from interactive theorem proving to conflict-driven SMT-solving and theory combination, by defining a small kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction.

Multi types—aka non-idempotent intersection types—have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of the result. Recent results show that the number of steps can be taken as a reasonable time complexity measure. At the same time, however, these results suggest that multi types provide quite lax complexity bounds, because the size of the result can be exponentially bigger than the number of steps. Starting from this observation, we refine and generalise a technique introduced by Bernadet & Graham-Lengrand to provide exact bounds for the maximal strategy. Our typing judgements carry two counters, one measuring evaluation lengths and the other measuring result sizes. In order to emphasise the modularity of the approach, we provide exact bounds for four evaluation strategies, both in the λ-calculus (head, leftmost-outermost, and maximal evaluation) and in the linear substitution calculus (linear head evaluation). Our work aims at both capturing the results in the literature and extending them with new outcomes. Concerning the literature, it unifies de Carvalho and Bernadet & Graham-Lengrand via a uniform technique and a complexity-based perspective. The two main novelties are exact split bounds for the leftmost strategy—the only known strategy that evaluates terms to full normal forms and provides a reasonable complexity measure—and the observation that the computing device hidden behind multi types is the notion of substitution at a distance, as implemented by the linear substitution calculus.

Didier Galmiche, Stéphane Graham-Lengrand; Special Issue on Computational Logic in Honour of Roy Dyckhoff, Journal of Logic and Computation, Volume 26, Iss

LJQ is a focused sequent calculus for intuitionistic logic, with a simple restriction on the first premiss of the usual left introduction rule for implication. In a previous paper we discussed its history (going back to about 1950, or beyond) and presented its basic theory and some applications; here we discuss in detail its relation to call-by-value reduction in lambda calculus, establishing a connection between LJQ and the CBV calculus λC of Moggi. In particular, we present an equational correspondence between these two calculi forming a bijection between the two sets of normal terms, and allowing reductions in each to be simulated by reductions in the other.