A novel way to use SMT (Satisfiability Modulo Theories) solvers to compute the tropical prevariety (resp. equilibrium) of a polynomial system is presented. The new method is benchmarked against a naive approach that uses purely polyhedral methods. It turns out that the SMT approach is faster than the polyhedral approach for models that would otherwise take more than one minute to compute, in many cases by a factor of 60 or more, and in the worst case is only slower by a factor of two. Furthermore, the new approach is an anytime algorithm, thus offering a way to compute parts of the solution when the polyhedral approach is infeasible.
We introduce an approach that aims to combine the usage of satisfiability modulo theories (SMT) solvers with the Combinatory Logic Synthesizer (CL)S framework. (CL)S is a tool for the automatic composition of software components from a user-specified repository. The framework yields a tree grammar that contains all composed terms that comply with a target type. Type specifications for (CL)S are based on combinatory logic with intersection types. Our approach translates the tree grammar into SMT functions, which allows the consideration of additional domain-specific constraints. We demonstrate …
Satisfiability modulo theory (SMT) consists in testing the satisfiability of first-order formulas over linear integer or real arithmetic, or other theories. In this survey, we explain the combination of propositional satisfiability and decision procedures for conjunctions known as DPLL(T), and the alternative "natural domain" approaches. We also cover quantifiers, Craig interpolants, polynomial arithmetic, and how SMT solvers are used in automated software analysis.
Quantifier-free nonlinear arithmetic (QF_NRA) appears in many applications of satisfiability modulo theories solving (SMT). Accordingly, efficient reasoning for corresponding constraints in SMT theory solvers is highly relevant. We propose a new incomplete but efficient and terminating method to identify satisfiable instances. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of single very large multivariate polynomials. Our method takes as input conjunctions of strict polynomial inequalities, which represent …
University of Edinburgh（爱丁堡大学）；UC Berkeley（加州大学伯克利分校）；University of Iowa（爱荷华大学）
In classic program synthesis algorithms, such as counterexample-guided inductive synthesis (CEGIS), the algorithms alternate between a synthesis phase and an oracle (verification) phase. Many synthesis algorithms use a white-box oracle based on satisfiability modulo theory (SMT) solvers to provide counterexamples. But what if a white-box oracle is either not available or not easy to work with? We present a framework for solving a general class of oracle-guided synthesis problems which we term synthesis modulo oracles. In this setting, oracles may be black boxes with a query-response interface …
Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols
Institute of Computer Science, The Czech Academy of Sciences（捷克科学院计算机研究所）；Faculty of Information Technology, Czech Technical University in Prague（布拉格捷克理工大学信息技术学院）；Czech Institute of Informatics, Robotics and Cybernetics, Czech Technical University in Prague（布拉格捷克理工大学信息学、机器人学与控制论捷克研究所）
In this paper, we present Bitwuzla, our Satisfiability Modulo Theories (SMT) solver for the theories of bit-vectors, floating-points, arrays and uninterpreted functions and their combinations. We discuss selected features and provide details of its configuration and participation in the 2020 edition of the annual SMT competition.
The problem of finding small unsatisfiable cores for SAT formulas has recently received a lot of interest, mostly for its applications in formal verification. However, propositional logic is often not expressive enough for representing many interesting verification problems, which can be more naturally addressed in the framework of Satisfiability Modulo Theories, SMT. Surprisingly, the problem of finding unsatisfiable cores in SMT has received very little attention in the literature. In this paper we present a novel approach to this problem, called the Lemma-Lifting approach. The main idea is …
Satisfiability Modulo the Theory of Nonlinear Real Arithmetic, SMT(NRA) for short, concerns the satisfiability of polynomial formulas, which are quantifier-free Boolean combinations of polynomial equations and inequalities with integer coefficients and real variables. In this paper, we propose a local search algorithm for a special subclass of SMT(NRA), where all constraints are strict inequalities. An important fact is that, given a polynomial formula with $n$ variables, the zero level set of the polynomials in the formula decomposes the $n$-dimensional real space into finitely many component…
The problem of computing Craig interpolants in SAT and SMT has recently received a lot of interest, mainly for its applications in formal verification. Efficient algorithms for interpolant generation have been presented for some theories of interest ---including that of equality and uninterpreted functions, linear arithmetic over the rationals, and their combination--- and they are successfully used within model checking tools. For the theory of linear arithmetic over the integers (LA(Z)), however, the problem of finding an interpolant is more challenging, and the task of developing efficient …
This report describes several approaches for handling synthesis conjectures within an Satisfiability Modulo Theories (SMT) solver. We describe approaches that primarily focus on determining the unsatisfiability of the negated form of synthesis conjectures using new techniques for quantifier instantiation.
In this paper, we compare two alternative mechanisms for deciding the validity of first-order formulas over finite domains supported by the mathematical model checker RISCAL: first, the original approach of semantic evaluation (based on an implementation of the denotational semantics of the RISCAL language) and, second, the later approach of SMT solving (based on satisfiability preserving translations of RISCAL formulas to SMT-LIB formulas as inputs for SMT solvers). After a short presentation of the two approaches and a discussion of their fundamental pros and cons, we quantitatively evaluate…
We give an overview of recent techniques for implementing syntax-guided synthesis (SyGuS) algorithms in the core of Satisfiability Modulo Theories (SMT) solvers. We define several classes of synthesis conjectures and corresponding techniques that can be used when dealing with each class of conjecture.
We introduce the notion of "δ-complete decision procedures" for solving SMT problems over the real numbers, with the aim of handling a wide range of nonlinear functions including transcendental functions and solutions of Lipschitz-continuous ODEs. Given an SMT problem φand a positive rational number δ, a δ-complete decision procedure determines either that φis unsatisfiable, or that the "δ-weakening" of φis satisfiable. Here, the δ-weakening of φis a variant of φthat allows δ-bounded numerical perturbations on φ. We prove the existence of δ-complete decision procedures for bounded SMT over rea…
Many state-of-the-art Satisfiability Modulo Theories (SMT) solvers for the theory of fixed-size bit-vectors employ an approach called bit-blasting, where a given formula is translated into a Boolean satisfiability (SAT) problem and delegated to a SAT solver. Consequently, producing bit-vector proofs in an SMT solver requires incorporating SAT proofs into its proof infrastructure. In this paper, we describe three approaches for integrating DRAT proofs generated by an off-the-shelf SAT solver into the proof infrastructure of the SMT solver CVC4 and explore their strengths and weaknesses. We impl…
Satisfiability modulo theories (SMT) solvers have throughout the years been able to cope with increasingly expressive formulas, from ground logics to full first-order logic modulo theories. Nevertheless, higher-order logic within SMT is still little explored. One main goal of the Matryoshka project, which started in March 2017, is to extend the reasoning capabilities of SMT solvers and other automatic provers beyond first-order logic. In this preliminary report, we report on an extension of the SMT-LIB language, the standard input format of SMT solvers, to handle higher-order constructs. We al…
Two important requirements when aggregating the preferences of multiple agents are that the outcome should be economically efficient and the aggregation mechanism should not be manipulable. In this paper, we provide a computer-aided proof of a sweeping impossibility using these two conditions for randomized aggregation mechanisms. More precisely, we show that every efficient aggregation mechanism can be manipulated for all expected utility representations of the agents' preferences. This settles an open problem and strengthens a number of existing theorems, including statements that were shown…
University of Maryland, College Park（马里兰大学帕克分校）；University of Nebraska at Omaha（内布拉斯加大学奥马哈分校）
Constraint answer set programming integrates answer set programming with constraint processing. System EZSMT+ is a constraint answer set programming tool that utilizes satisfiability modulo theory solvers for search. Its theoretical foundation lies on generalizations of Niemela's characterization of answer sets of a logic program via so called level rankings.
Fundamentally, every static program analyser searches for a proof through a combination of heuristics providing candidate solutions and a candidate validation technique. Essentially, the heuristic reduces a second-order problem to a first-order/propositional one, while the validation is often just a call to a SAT/SMT solver. This results in a monolithic design of such analyses that conflates the formulation of the problem with the solving process. Consequently, any change to the latter causes changes to the whole analysis. This design is dictated by the state of the art in solver technology. W…
We present our extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers using ACL2's trusted clause processor mechanism. We are particularly interested in the verification of physical systems including Analog and Mixed-Signal (AMS) designs. ACL2 offers strong induction abilities for reasoning about sequences and SMT complements deduction methods like ACL2 with fast nonlinear arithmetic solving procedures. While SAT solvers have been integrated into ACL2 in previous work, SMT methods raise new issues because of their support for a broader range of domains including real numbers and u…
Given a formula $F$ of satisfiability modulo theory (SMT), the classical SMT solver tries to (1) abstract $F$ as a Boolean formula $F_B$, (2) find a Boolean solution to $F_B$, and (3) check whether the Boolean solution is consistent with the theory. Steps~{(2)} and (3) may need to be performed back and forth until a consistent solution is found. In this work, we develop a quantum SMT solver for the bit-vector theory. With the characteristic of superposition in quantum system, our solver is able to consider all the inputs simultaneously and check their consistency between Boolean and the theory…
Arizona State University（亚利桑那州立大学）；Houzz Inc.（Houzz 公司）
Both hybrid automata and action languages are formalisms for describing the evolution of dynamic systems. This paper establishes a formal relationship between them. We show how to succinctly represent hybrid automata in an action language which in turn is defined as a high-level notation for answer set programming modulo theories (ASPMT) --- an extension of answer set programs to the first-order level similar to the way satisfiability modulo theories (SMT) extends propositional satisfiability (SAT). We first show how to represent linear hybrid automata with convex invariants by an action langu…
We present a new model-based interpolation procedure for satisfiability modulo theories (SMT). The procedure uses a new mode of interaction with the SMT solver that we call solving modulo a model. This either extends a given partial model into a full model for a set of assertions or returns an explanation (a model interpolant) when no solution exists. This mode of interaction fits well into the model-constructing satisfiability (MCSAT) framework of SMT. We use it to develop an interpolation procedure for any MCSAT-supported theory. In particular, this method leads to an effective interpolation…
Smtlink is an extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers. We presented an earlier version at ACL2'2015. Smtlink 2.0 makes major improvements over the initial version with respect to soundness, extensibility, ease-of-use, and the range of types and associated theory-solvers supported. Most theorems that one would want to prove using an SMT solver must first be translated to use only the primitive operations supported by the SMT solver -- this translation includes function expansion and type inference. Smtlink 2.0 performs this translation using a sequence of steps perfo…
Logical reasoning about program data often requires dealing with heap structures as well as scalar data types. Recent advances in Satisfiability Modular Theory (SMT) already offer efficient procedures for dealing with scalars, yet they lack any support for dealing with heap structures. In this paper, we present an approach that integrates Separation Logic---a prominent logic for reasoning about list segments on the heap---and SMT. We follow a model-based approach that communicates aliasing among heap cells between the SMT solver and the Separation Logic reasoning part. An experimental evaluati…
We report on work in progress on automatic procedures for proving properties of programs written in higher-order functional languages. Our approach encodes higher-order programs directly as first-order SMT problems over Horn clauses. It is straight-forward to reduce Hoare-style verification of first-order programs into satisfiability of Horn clauses. The presence of closures offers several challenges: relatively complete proof systems have to account for closures; and in practice, the effectiveness of search procedures depend on encoding strategies and capabilities of underlying solvers. We he…
The Why3 IDE and verification system facilitates the use of a wide range of Satisfiability Modulo Theories (SMT) solvers through a driver-based architecture. We present Where4: a portfolio-based approach to discharge Why3 proof obligations. We use data analysis and machine learning techniques on static metrics derived from program source code. Our approach benefits software engineers by providing a single utility to delegate proof obligations to the solvers most likely to return a useful result. It does this in a time-efficient way using existing Why3 and solver installations - without requiri…
Neuro Symbolic Reasoning for Planning: Counterexample Guided Inductive Synthesis using Large Language Models and Satisfiability Solving
Florida International University（佛罗里达国际大学）；SRI International（SRI国际（斯坦福国际研究院））；United States Military Academy（美国军事学院（西点军校））；University of Colorado Boulder（科罗拉多大学博尔德分校）；University of Central Florida（中佛罗里达大学）；Vanderbilt University（范德堡大学）
Max Planck Institute for Software Systems (MPI-SWS)（马克斯·普朗克软件系统研究所）
#SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tasks as counting the number of satisfying assignments to a Boolean formula and computing the volume of a polytope. In the realm of satisfiability modulo theories (SMT) there is a growing need for model counting solvers, coming from several application domains (quantitative information flow, static analysis of probabilistic programs). In this paper, we show a reduction from an approximate version of #SMT to SMT. We focus on the theories of integer arithmetic and linear real arithmetic. We propose m…
Satisfiability Modulo Theories (SMT) solvers have been successfully applied to solve many problems in formal verification such as bounded model checking (BMC) for many classes of systems from integrated circuits to cyber-physical systems. Typically, BMC is performed by checking satisfiability of a possibly long, but quantifier-free formula. However, BMC problems can naturally be encoded as quantified formulas over the number of BMC steps. In this approach, we then use decision procedures supporting quantifiers to check satisfiability of these quantified formulas. This approach has previously b…
The problem of computing Craig Interpolants has recently received a lot of interest. In this paper, we address the problem of efficient generation of interpolants for some important fragments of first order logic, which are amenable for effective decision procedures, called Satisfiability Modulo Theory solvers. We make the following contributions. First, we provide interpolation procedures for several basic theories of interest: the theories of linear arithmetic over the rationals, difference logic over rationals and integers, and UTVPI over rationals and integers. Second, we define a novel ap…
Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combinat…
We present here a new explicit reasoning framework for linear temporal logic (LTL), which is built on top of propositional satisfiability (SAT) solving. As a proof-of-concept of this framework, we describe a new LTL satisfiability tool, Aalta\_v2.0, which is built on top of the MiniSAT SAT solver. We test the effectiveness of this approach by demonnstrating that Aalta\_v2.0 significantly outperforms all existing LTL satisfiability solvers. Furthermore, we show that the framework can be extended from propositional LTL to assertional LTL (where we allow theory atoms), by replacing MiniSAT with t…
We propose a model-based procedure for automatically preventing security threats using formal models. We encode system models and potential threats as satisfiability modulo theory (SMT) formulas. This model allows us to ask security questions as satisfiability queries. We formulate threat prevention as an optimization problem over the same formulas. The outcome of our threat prevention procedure is a suggestion of model attribute repair that eliminates threats. Whenever threat prevention fails, we automatically explain why the threat happens. We implement our approach using the state-of-the-ar…
We present a novel approach for solving quantified bit-vector formulas in Satisfiability Modulo Theories (SMT) based on computing symbolic inverses of bit-vector operators. We derive conditions that precisely characterize when bit-vector constraints are invertible for a representative set of bit-vector operators commonly supported by SMT solvers. We utilize syntax-guided synthesis techniques to aid in establishing these conditions and verify them independently by using several SMT solvers. We show that invertibility conditions can be embedded into quantifier instantiations using Hilbert choice…
In the contexts of automated reasoning and formal verification, important decision problems are effectively encoded into Satisfiability Modulo Theories (SMT). In the last decade efficient SMT solvers have been developed for several theories of practical interest (e.g., linear arithmetic, arrays, bit-vectors). Surprisingly, very few work has been done to extend SMT to deal with optimization problems; in particular, we are not aware of any work on SMT solvers able to produce solutions which minimize cost functions over arithmetical variables. This is unfortunate, since some problems of interest …
Chennai Mathematical Institute, India IAI, TCG CREST, Kolkata, India（钦奈数学研究所，印度 IAI，TCG CREST，科利尔，印度）；Georgia Institute of Technology, USA University of Toronto, Canada（佐治亚理工学院，美国 蒙特利尔大学，加拿大）
In various areas of computer science, we deal with a set of constraints to be satisfied. If the constraints cannot be satisfied simultaneously, it is desirable to identify the core problems among them. Such cores are called minimal unsatisfiable subsets (MUSes). The more MUSes are identified, the more information about the conflicts among the constraints is obtained. However, a full enumeration of all MUSes is in general intractable due to the large number (even exponential) of possible conflicts. Moreover, to identify MUSes algorithms must test sets of constraints for their simultaneous satis…
