Skip to main content

Questions tagged [smt-solvers]

Solver programs for the Satisfiability Modulo Theories (SMT). The SMT problem is a decision problem for logical formulas with combinations of background theories expressed in classical first-order logic with equality.

15 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
6 votes
1 answer
805 views

Exponential example for simplex used in SMT solvers

The original simplex algorithm requires an exponential number of pivot operations in the worst case, e.g., if run on the Klee-Minty example [3,4]. What about the simplex algorithm used in SMT solvers ...
Ayrat's user avatar
  • 1,085
5 votes
0 answers
190 views

Introduction to bounded model checking that describes model generation

Most of the tutorials I have found on model checking and bounded model checking start with, the model is given as a Kripke Structure M = (S,I,T,L) where S is a set of states, I is a set of initial ...
Jonathan Gallagher's user avatar
4 votes
0 answers
51 views

How the $EX(f)$ is evaluated in symbolic model checking?

I was reading the symbolic model checking, So there it has mentioned that we can represent the set of states and transition relations of any transition system with the help of ROBDDs. I was trying to ...
Sujit Kumar Muduli's user avatar
2 votes
0 answers
187 views

Passing arrays vs functions as arguments in SMT?

In SAT Modulo Theories (SMT), with the theory of uninterpreted functions, all functions are first order, that is, they don't take functions as arguments or return functions. In the theory of arrays, ...
Joey Eremondi's user avatar
1 vote
1 answer
92 views

A Fast Linear-Arithmetic Solver: How can Gaussian elimination be used to simplify matrix A?

I am working on an LRA Theory solver for SymPy, an open source python library for symbolic computations. You can find my work here. Currently I'm trying to optimize it to run faster. My implementation ...
Tilo RC's user avatar
  • 11
1 vote
0 answers
95 views

SMT solver gives up on seemingly trivial problem

I expected CVC5 to produce a proof given the following problem in TPTP format. Why does CVC5 give up on the TPTP problem, but works just fine on the same problem given in SMT-LIB2? In human words, the ...
Max Nowak's user avatar
1 vote
1 answer
101 views

Is there an SMT/SAT algorithm for General Predicate Logic (FOL)?

I'm learning how to write my own theorem prover. After skimming Decision Procedures (Kroening & Strichman, 2016), I didn't find any SMT algorithms for solving quantified n-ary predicate formulas. ...
Vivek Joshy's user avatar
1 vote
0 answers
98 views

SMT validity solvers/ quantifier elimination in Ocaml

I am working on my own expression package in Ocaml and have to perform both validity queries and quantifier elimination. I have already implemented Cooper's procedure (for Presburger and Linear ...
Theo Deep's user avatar
  • 113
1 vote
0 answers
176 views

General Understanding of SMT Solving Across Multiple Theories

My first question was a little too simplified in that it turned out to be an integer linear programming problem solvable with the Simplex Method. However, what I think I am wondering about is how to ...
Lance's user avatar
  • 2,243
0 votes
0 answers
15 views

Common clauses in two CNF formulas

How to identify the number of common clauses in two CNF formulas? For example, for formulas: (x1∨¬x2)∧(¬x1∨x3)∧(x2∨¬x3) and (x1∨¬x2)∧(x2∨¬x3)∧(x1∨x3), the common clauses are (x1∨¬x2) and (x2∨¬x3). ...
andre_c's user avatar
0 votes
0 answers
16 views

How do static analysis tools automate separation logic?

I understand separation logic as a form of verification method, similar to Hoare logic. That is, they allow to reason about statements of the form $\{P\} C \{Q\}$, where $C$ is an instruction, and $P$ ...
BlockchainThomas's user avatar
0 votes
0 answers
39 views

Specific quantifier elimination for real algebraic numbers

It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
Theo Deep's user avatar
  • 113
0 votes
0 answers
59 views

SAT solvers that can compute prime implicants and/or minimization

I'm looking into computing the prime implicants of a Boolean function. I have found many different algorithms in the literature, many of them relying on SAT solvers. However, I have not been able to ...
Noel Arteche's user avatar
0 votes
0 answers
60 views

Program synthesis based on function properties

I am fairly new at program synthesis and the use of SMT solvers for this purpose. Given a function g, I want to generate all the functions f and h such that the following holds: f . g = h . f Are ...
user5803465's user avatar
0 votes
0 answers
178 views

When to use SAT vs solving?

Are there any guidelines for how to recognize, for a given problem, which approach is more likely to yield good results? SAT solver or SMT solver? Is there any guidance anyone can offer about which ...
sepideha's user avatar
  • 101