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.

9 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
5
votes
0answers
144 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 ...
5
votes
1answer
467 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 ...
4
votes
0answers
46 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 ...
2
votes
0answers
118 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, ...
1
vote
0answers
114 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 ...
0
votes
0answers
27 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 ...
0
votes
0answers
33 views

Can numbers (not sets of numbers) in Linear Integer Arithmetic form a Boolean algebra?

As far as I understood, Boolean algebra is just one of the many first-order theories (1). It has the signature $\{\sqcap, \sqcup, \neg, \bot, \top\}$ and the axioms: associativity, commutativity, ...
0
votes
0answers
8 views

Optimization palletizing and dispatch

I have the following situation: I have to find the most optimal days to palletize and to dispatch pallets to 22 different destination. The demand for each destination varies, ranging from 3 to 12 ...
0
votes
0answers
116 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 ...