Satisfiability modulo theories

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality (often disallowing quantifiers). SMT solvers are tools which aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing. Since Boolean satisfiability is already NP-complete, the SMT problem is typically NP-hard, and for many theories it is undecidable. Researchers

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related publications (10)

Related publications

Related people (2)

Related people

Related units (2)

Related units

Related concepts (18)

Related concepts

Related courses (1)

Related courses

Related lectures (1)

Related lectures

A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Joseph Reynolds

We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identifies observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson-Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from theories developed with Isabelle demonstrates the potential of the procedure.

Springer-Verlag Berlin2015

A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings

Andrew Joseph Reynolds

We prove that the quantifier-free fragment of the theory of character strings with regular language membership constraints and linear integer constraints over string lengths is decidable. We do that by describing a sound, complete and terminating tableaux calculus for that fragment which uses as oracles a decision procedure for linear integer arithmetic and a number of computable functions over regular expressions. A distinguishing feature of this calculus is that it provides a completely algebraic method for solving membership constraints which can be easily integrated into multi-theory SMT solvers. Another is that it can be used to generate symbolic solutions for such constraints, that is, solved forms that provide simple and compact representations of entire sets of complete solutions. The calculus is part of a larger one providing the theoretical foundations of a high performance theory solver for string constraints implemented in the SMT solver CVC4.

Springer-Verlag Berlin2015

ShapeOp - A Robust and Extensible Geometric Modelling Paradigm

Sofien Bouaziz, Anders Holden Deleuran, Bailin Deng, Mario Moacir Deuss, Mark Pauly

We present ShapeOp, a robust and extensible geometric modelling paradigm. ShapeOp builds on top of the state-of-the-art physics solver (Bouaziz et al. in ACM Trans Graph 33:154:1–154:11, 2014). We discuss the main theoretical advantages of the underlying solver and how this influences our modelling paradigm. We provide an efficient open-source C++ implementation (www.shapeop.org) together with scripting interfaces to enable ShapeOp in Rhino/Grasshopper and potentially other tools. This implementation can also act as a template for future integration of computer graphics research. To evaluate the potential of ShapeOp we present various examples using our implementation and discuss potential implications on the design process.

Springer 2015

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

Automated theorem proving

Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Autom

Boolean satisfiability problem

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining i

Constraint satisfaction problem

Constraint satisfaction problems (CSPs) are mathematical questions defined as a set of objects whose state must satisfy a number of constraints or limitations. CSPs represent the entities in a problem