# 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 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 ... 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