6
votes
Accepted
How could an SMT solver be implemented as simple as possible?
What happens next is that we invoke a SMT solver to try to check whether the formula
$$x+y < 20 \quad \land \quad x > 10 \quad \land \quad y > 10$$
is satisfiable. The solver tries to ...
D.W.♦
- 166k
6
votes
Accepted
What are the differences between symbolic execution and SAT solvers?
TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on ...
- 7,248
4
votes
Accepted
Bit Blasting Algorithm
I assume the formula is
$$(x \ne 0) \land (y|2 = z) \land (1<3).$$
We can handle each clause of the conjunction separately. If $x=(b_3,b_4)$, then $x \ne 0$ translates to
$$b_3 \lor b_4.$$
If $...
D.W.♦
- 166k
3
votes
Accepted
What is the difference in heap configurations? Separation logic with CVC5 SMT solver
Thanks for the question. The model construction for the separation logic heap in cvc5 was wrong in this case. This will be fixed by https://github.com/cvc5/cvc5/pull/9574.
3
votes
How could an SMT solver be implemented as simple as possible?
You may not need a general SMT solver. In this case, you have a bunch of inequalities conjoined together, which you can solve as a linear program.
A simpler alternative to an SMT solver is to ...
- 23.8k
3
votes
Accepted
How a SMT / SAT Solver Generates Valuations for this Example
The Simplex algorithm solves the linear programming problem.
Linear programming is the problem of optimizing a linear function with inputs $x_1, x_2, \dots, x_n$ subject to a system of linear ...
- 1,043
3
votes
Automated reasoning with real numbers
In your case, the simplest solution may be to use SAT.
Your first clause includes $x \le 0.25$ and $x > 0.91$. This means that there are five regions of interest for the variable $x$, which we ...
- 23.8k
3
votes
How to leverage the fact that I'm solving 1000's of very similar SMT instances?
Some SAT solvers and SMT solvers offer an interface that lets you push clauses, and then later pop/retract them and push some new ones. You could explore to see whether this offers a speedup in your ...
D.W.♦
- 166k
3
votes
Is the optimal order of graph vertices s.t. minimizes edges to later vertices a well-known problem?
Your problem can be mapped to problem of finding minimal set of edges $F$ such that $G\backslash F$ is a DAG (each solution for your problem is a solution for this problem and vice versa). This ...
2
votes
Using SMT Solvers in formula checking
Yes, absolutely. SMT solvers are actually quite well suited for such problems. Unfortunately, the input language to them (SMTLib) is rather machine-oriented, but there are many "high-level" interfaces ...
- 211
2
votes
Verification condition in case of array theory
Sure, if the user provides inductive invariants, you can try to check the validity of the verification conditions. However, this remains undecidable, as it requires checking the validity of a formula ...
D.W.♦
- 166k
2
votes
Accepted
Is the optimal order of graph vertices s.t. minimizes edges to later vertices a well-known problem?
Szymon Stankiewicz is right -- this problem is basically Feedback Arc Set, which is unfortunately NP-complete. But I have to mention that a very similar graph property, which goes by the slightly ...
- 5,509
2
votes
Accepted
Are there any solvers that can handle non-linearity?
You can't. There is no solver that can handle all constraints over the natural numbers and always finds a solution if one exists. The problem is undecidable, even without allowing variables in the ...
D.W.♦
- 166k
2
votes
Accepted
How to represent bottom element (integer domains) in SMT formula
First, you need to figure out the semantics of your language: does divide-by-zero cause the program to abort/halt/throw an exception, or does execution proceed and the divide-by-zero returns a NaN?
If ...
D.W.♦
- 166k
2
votes
Accepted
Automated reasoning with real numbers
Yes, you could solve this with a SMT solver that supports linear real arithmetic. However SMT supports more general inequalities where you can have linear sums of variables (e.g., $2a+3x \le 5.7$) ...
D.W.♦
- 166k
1
vote
Is stable infinity required of theories combined with model-based theory combination?
A possible indirect answer can be found in slides (1) for a presentation for the 2008 Oregon Summer School on Logic and Theorem Proving by Leonardo de Moura, who worked on Z3 extensively:
Essentially,...
- 163
1
vote
A Fast Linear-Arithmetic Solver: How can Gaussian elimination be used to simplify matrix A?
The idea here is that if you have a solution for $x$, $s_1$, and $s_2$, then from this you can find $y$ and $z$.
The way you can solve this is to solve the linear system:
$$\begin{eqnarray*}
y + 0z &...
- 23.8k
1
vote
How does the SMT solver Z3 handle conditional statements in a constraint?
A minimum expression $min(x_1, x_2)$ can be transformed by introducing a new variable $m$ replacing the expression and adding the following formula to the set of boolean combinations of (in/dis)...
- 33
1
vote
Accepted
How does the SMT solver Z3 handle conditional statements in a constraint?
I can't answer how Z3 works. I can only speculate on some possible ways one could build a solver for this type of constraints, if one wanted.
It appears all of your inequalities have the form
$$A \le ...
D.W.♦
- 166k
1
vote
Accepted
Domain of discourse vs First-order theory
Unless I'm missing something, you're simply asking a different question than the previous questioner did.
The previous question is asking an abstract question about predicate logic, so all axioms are ...
- 23.8k
1
vote
Which of these properties hold for all FO theories? (but not regarding fragments thereof)
Your answers to (a) and (c) are correct. To tell whether (b) is correct we need a precise notion of expressiveness.
The issue is that propositional logic and first-order logic have totally different ...
- 2,989
1
vote
Accepted
Constraint satisfaction problem: solve system, then evaluate whether many additional constraints are satisfied one at a time
If the constraints you have are of the form $a < b$ and $a=b$ (i.e., only unconditional inequality constraints), you can model them with a directed graph: each node represents a variable, and an ...
D.W.♦
- 166k
1
vote
Accepted
Proving that a property is k-inductive with an SMT solver (parametric resettable counter)
I don't see any gap in your understanding. What you wrote looks correct to me.
Perhaps the author meant to use the property $P := c \le n+1 \land n \ge 1$. I think with that modification, $P$ ...
D.W.♦
- 166k
1
vote
Generating graph with complex structure
I would use a SAT solver. Use one boolean variable per edge to encode whether that edge is present or not. Encode the type of a node via a one-hot encoding ($k$ variables per node, where $k$ is the ...
D.W.♦
- 166k
1
vote
Accepted
Objective function and constraint satisfaction over a set of multi-attributes elements
I don't see any problem with modeling this as an integer linear program, for example:
...
- 2,103
1
vote
Is the optimal order of graph vertices s.t. minimizes edges to later vertices a well-known problem?
Layered graph drawing
Layered graph drawing is a graph in which the vertices of a directed graph are drawn in horizontal rows or layers with the edges generally directed downwards.
. However, graphs ...
- 315
1
vote
SMT solves with functions for free varibles
SMT solvers do support uninterpreted-functions as part of many logics. If there's a counter-example, then they will also print a "counter-example" function, which will be the predicate you're looking ...
- 211
1
vote
Using SMT solvers to generate random solutions to given predicate
A simple approach would be to simply generate a solution, and then ask for a "different" one, surely? Since you mentioned Haskell, you can use the SBV library to implement this easily, and use the <...
- 211
Only top scored, non community-wiki answers of a minimum length are eligible