The Stack Overflow podcast is back! Listen to an interview with our new CEO.

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.

Filter by
Sorted by
Tagged with
0
votes
0answers
26 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
30 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 ...
5
votes
1answer
202 views

Check if two items are equal after replacing

Let's say that an item is either a natural number or a list of items. Examples of items are: 1 [2] [4, [3, 1], 3, 4] A rule states that two items are equal. For example: 1 = 2 3 = [3, 1] [4, 3] = [...
0
votes
1answer
13 views

Generating graph with complex structure

I want to generate a bunch of graphs of about 100 nodes, where each node is a categorial variable. I want the graphs to satisfy complex properties, like, "if a node of type A is connected to a node ...
1
vote
0answers
109 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 ...
-2
votes
1answer
110 views

How a SMT / SAT Solver Generates Valuations for this Example

First, an example of a set of constraints which turned out not to be solvable (I don't think): ...
2
votes
0answers
103 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, ...
0
votes
1answer
61 views

Objective function and constraint satisfaction over a set of multi-attributes elements

I'm looking for an approach to solve a problem consisting of maximizing an objective function over a set of discrete elements, while respecting a set of constraints. To illustrate my point, I'll try ...
2
votes
1answer
709 views

Bit Blasting Algorithm

I found a pseudo algorithm which describes bit blasting: click (page 156,157). I am trying to implement it in C, but I don't understand it yet completely. Let's make an example: Assume our bit-...
4
votes
2answers
443 views

How could an SMT solver be implemented as simple as possible?

I'm trying to figure out how an SMT solver works as simple as possible. Let's assume we have a simple input program with symbolic values x and ...
0
votes
0answers
110 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 ...
0
votes
1answer
51 views

Verification condition in case of array theory

As far as i can understand the problem of checking safety property, can be reduce to solving for inductive invariants in VC's and there is following parts to it: Generate VC's from the program. Solve ...
3
votes
3answers
119 views

Is the optimal order of graph vertices s.t. minimizes edges to later vertices a well-known problem?

I'm a little unfamiliar with graph theory, and I found an interesting problem in my work that I do not know if its already well-known or can be easily mapped to another one. If I were to express the ...
4
votes
0answers
45 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 ...
6
votes
1answer
196 views

Framework or tools to generate theorem prover/solver/reasoner for new logic

I have new logic which has syntax and semantics in usual natural languages and I have to create theorem prover/solver/reasoner for this logic. Is there framework or tool set that can generate such ...
1
vote
1answer
116 views

Using SMT Solvers in formula checking

I'm currently working on a static analysis work in which I need to check whether a given formula is met or not. I hope the following example clarifies my requirement. Suppose we have a list of three-...
5
votes
1answer
448 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 ...
2
votes
1answer
43 views

SMT solves with functions for free varibles

So this sounds like this might lead to an undecidable theory but I thought I would give it a try and ask about it after I found nothing on the subject. I am somewhat interested in finding functions ...
5
votes
2answers
231 views

Using SMT solvers to generate random solutions to given predicate

I am interested in generating random solutions to predicates. I only need SMT for integers with the following predicates/functions <, >, <=, >=, ==, !=, +, * The algorithm I want should produce ...
5
votes
0answers
137 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 ...
15
votes
3answers
3k views

Why is unification so important to inference engines?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. I keep reading about the Unification Algorithm. ...
16
votes
2answers
360 views

Why do some inference engines need human assistance while others don't?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Why is it that automated theorem provers, i.e. ACL2,...