Skip to main content
OverflowAI is here! AI power for your Stack Overflow for Teams knowledge community. Learn more
10 votes
Accepted

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

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 ...
Martin Berger's user avatar
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.'s user avatar
  • 160k
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 ...
Caleb Stanford's user avatar
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.'s user avatar
  • 160k
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.
Andrew Reynolds's user avatar
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 ...
Szymon Stankiewicz's user avatar
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 ...
Pseudonym's user avatar
  • 22.2k
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 ...
Curtis F's user avatar
  • 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 ...
Pseudonym's user avatar
  • 22.2k
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.'s user avatar
  • 160k
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 ...
alias's user avatar
  • 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.'s user avatar
  • 160k
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 ...
j_random_hacker's user avatar
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.'s user avatar
  • 160k
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.'s user avatar
  • 160k
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.'s user avatar
  • 160k
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)...
MvB's user avatar
  • 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.'s user avatar
  • 160k
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 ...
Pseudonym's user avatar
  • 22.2k
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 ...
Noah Schweber's user avatar
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.'s user avatar
  • 160k
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.'s user avatar
  • 160k
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.'s user avatar
  • 160k
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: ...
user555045's user avatar
  • 2,053
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 ...
MysticForce's user avatar
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 ...
alias's user avatar
  • 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 <...
alias's user avatar
  • 211

Only top scored, non community-wiki answers of a minimum length are eligible