Tag Info

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