ABSTRACT. The Alethe format is a representation of unsatisfiability proofs that has been adopted by several SMT solvers. We describe work in progress for interpreting Alethe proofs and generating corresponding proofs that are accepted by the Lambdapi proof checker, a foundational proof assistant based on dependent type theory and rewriting rules that serve as a pivot for exchanging proofs between several interactive proof assistants. We give an overview of the encoding of SMT logic and Alethe proofs in Lambdapi and present initial results of the evaluation of the checker on benchmark examples.

ABSTRACT. Certifying results by checking proofs and models is an essential feature of modern SAT solving. While incremental solving with assumptions and core extraction is crucial for many applications, support for incremental proof certificates remains lacking. We propose a proof format and corresponding checkers for incremental SAT solving. We further extend it to leverage resolution hints. Experiments on incremental SAT solving for Bounded Model Checking and Satisfiability Modulo Theories demonstrate the feasibility of our approach, further confirming that resolution hints substantially reduce checking time.

(Presentation only submission. This paper has been accepted for LPAR 2024 and will be published in its proceedings).

ABSTRACT. Modern SMT solvers, such as Z3, offer user-controllable strategies, enabling users to tailor solving strategy for their unique set of instances, thus dramatically enhancing the solver performance for their use case. However, this approach of strategy customization presents a significant challenge: handcrafting an optimized strategy for a class of SMT instances remains a complex and demanding task for both solver developers and users alike.

In this paper, we address this problem of automatic SMT strategy synthesis via a novel Monte Carlo Tree Search (MCTS) based method. Our method treats strategy synthesis as a sequential decision-making process, whose search tree corresponds to the strategy space, and employs MCTS to navigate this vast search space. The key innovations that enable our method to identify effective strategies, while keeping costs low, are the ideas of layered and staged MCTS search. These novel heuristics allow for a deeper and more efficient exploration of the strategy space, enabling us to synthesize more effective strategies than the default ones in state-of-the-art (SOTA) SMT solvers. We implement our method, dubbed Z3alpha, as part of the Z3 SMT solver. Through extensive evaluations across six important SMT logics, Z3alpha demonstrates superior performance compared to the SOTA synthesis tool FastSMT, the default Z3 solver, and the CVC5 solver on most benchmarks. Remarkably, on a challenging QF_BV benchmark set, Z3alpha solves 42.7% more instances than the default strategy in Z3.

ABSTRACT. The theory of fixed-size bit-vectors in Satisfiability Modulo Theories is essential in bit-precise reasoning applications. The dominant state-of-the-art approach for solving bit-vector formulas is a technique called bit-blasting, an eager reduction of bit-vectors to SAT. While surprisingly efficient in practice, bit-blasting may not scale for large bit-vectors or if bit-vector arithmetic is involved. In this talk, I will highlight challenges in reasoning over bit-vectors and discuss the current state of bit-level and word-level approaches.

ABSTRACT. In this paper we present a translation from bit-vector formulas to integer formulas. The translation uses the function symbols function symbols bv2nat and nat2bv_k which are both utilized in the theory of fixed-width bit-vectors of the SMT-LIB language to define the semantics of bit-vector operations. Our translation replaces bit-vector operations with their semantic definition. This facilitates a more modular application as bit-vector operations and their semantic definition have the same sort. As a postprocessing our translation replaces the composition of bv2nat and nat2bv_k with a modulo operation, and removes redundant modulo operations from the translation result. The evaluation of our translation shows that we are able to solve 9% more tasks, 10% faster and with 23% less memory usage compared to a closely related, up-to-date translation approach. Additionally, our translation supports the translation of quantified formulas and arrays over bit-vectors.

ABSTRACT. In this paper, we present the support for the (extensional) theory of arrays in the MCSat scheme for SMT solving. We describe its implementation in the (MCSat component of) the Yices2 SMT-solver, allowing Yices2 to solve, for the first time, benchmarks that combine arrays with non-linear arithmetic. Our experimental results show that this implementation outperforms other state-of-the-art SMT solvers when solving such benchmarks (QF-ANIA + QF-AUFNIA), and also demonstrates decent performance on other SMT logics that involve arrays.

ABSTRACT. We make two contributions to the study of theory combination in satisfiability modulo theories. The first is a table of examples for the combinations of the most common model-theoretic properties in theory combination, namely stable infiniteness, smoothness, convexity, finite witnessability, and strong finite witnessability (and therefore politeness and strong politeness as well). All of our examples are sharp, in the sense that we also offer proofs that no theories are available within simpler signatures. This table significantly progresses the current understanding of the various properties and their interactions. The most remarkable example in this table is of a theory over a single sort that is polite but not strongly polite (the existence of such a theory was only known until now for two-sorted signatures). The second contribution is a new combination theorem showing that in order to apply polite theory combination, it is sufficient for one theory to be stably infinite and strongly finitely witnessable, thus showing that smoothness is not a critical property in this combination method. This result has the potential to greatly simplify the process of showing which theories can be used in polite combination, as showing stable infiniteness is considerably simpler than showing smoothness.