10
There are many related ways you can mechanise your logic.
Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using the embedded logic awkward.
Shallow embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is only possible when the embedded ...
7
I would say that the classic distinction of "automated theorem proving" (ATP) vs. "interactive theorem proving" (ITP) needs to be reconsidered. If you take a well-known ITP system like Isabelle/HOL today (Isabelle2013 from February 2013), it integrates quite a lot of add-on tools from the ATP portfolio:
On-board generic automated proof tools: old-school ...
6
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 find values for $x,y$ that make this formula true. If it finds such a value, then it knows the assume(false) statement is reachable. (I am guessing you meant to ...
5
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 the other hand, is a method of analyzing programs. Symbolic execution usually relies on SAT and SMT solvers, but not the other way around.
SAT and SMT solvers ...
4
Let $\varphi(x)$ be the SMT instance, so the task is to find $x$ such that $\varphi(x)$ is true.
One approach is to fix a hash function $h$ that maps a value of $x$ to an element of some small set $S$. Then, you randomly select a value $s \in S$, and ask your SMT solver to find a satisfying assignment for the formula $\varphi(x) \land h(x)=s$.
If you want ...
4
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 $y=(b_5,b_6)$ and $z=(b_7,b_8)$, then $y|2$ translates to $(b_5|1,b_6)$, which simplifies to $(1,b_6)$ (if you are doing simplification). Now $(1,b_6) = (b_7,...
3
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 identify with boolean variables: $X_1 \equiv x \in(-\infty, 0.25)$, $X_2 \equiv x = 0.25$, $X_3 \equiv x \in (0.25, 0.91)$, $X_4 \equiv x = 0.91$, $X_5 \equiv x \in ...
3
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 situation. There are no guarantees, and the only way to tell is to try it.
3
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 problem is known as minimum feedback arc set problem and is one of Karp's 21 NP-complete problems
3
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 implement the theory as an add-on to a logic program. Most decent Prolog implementations, for example, have a CLP(R) or CLP(Q) library which can solve equality and ...
3
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 equations:
$$ 0 \leq x_1, \dots, x_n $$
$$ a_{11} x_1 + \dots + a_{1n} x_n \leq b_1 $$
$$ a_{21} x_2 + \dots + a_{2n} x_n \leq b_2 $$
$$ \dots $$
$$ a_{n1} x_1 + \...
2
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 to many solvers, Z3 itself providing a Python interface, for instance.
For this problem, I'll use the Haskell SBV library, which translates your constraints ...
2
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 in first-order logic (with quantifiers and array expressions), and that's undecidable.
It might be feasible often enough in practice to be useful, especially ...
2
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 alarming name of agony, can actually be computed in just $O(m^2)$ time, where $m$ is the number of edges. The agony of a graph is essentially a weighted form of ...
2
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$) instead of simple comparisons between a single variable and a constant (e.g., $a \le 1.6$), so it might be more powerful than you need, so if you don't have any ...
1
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 edge $v \to w$ corresponds to the inequality $v < w$. Then you can answer queries by doing a straightforward reachability check. (If you see the equality $v=...
1
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$ becomes 1-inductive but not 0-inductive. I suspect the author was looking for a simple example of a property that is 1-inductive but not 0-inductive, and missed a ...
1
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 number of possible types). Then each constraint you mention should translate directly into a simple formula on a few of these boolean variables.
I like Z3 for ...
1
I don't see any problem with modeling this as an integer linear program, for example:
maximize V.x
st:
1) s.x < 80
2) 20 <= e.x <= 35
3) FR.x >= 5
4a) Wood.x + 2 - 2W >= 2
4b) Stone.x + 2W >= 2
5) Gold.x - Stone.x < 0
6) Size10p.x <= 5
x[i] ∈ {0, 1}
W ∈ {0, 1}
Where . is the dot product, x is a binary vector indicating which items ...
1
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 often contain cycles, minimizing the number of inconsistently-oriented edges is NP-hard, and minimizing the number of crossings is also NP-hard.
source: ...
1
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 for. If you have a concrete example, we can surely see if one can be coded up using Z3.
1
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 allSat function to generate "different" assignments. Here's an example; not quite the same question as yours but somewhat similar, coded in that style: https://...
Only top voted, non community-wiki answers of a minimum length are eligible
