Skip to main content

Questions tagged [smt-solvers]

Solver programs for the Satisfiability Modulo Theories (SMT). The SMT problem is a decision problem for logical formulas with combinations of background theories expressed in classical first-order logic with equality.

Filter by
Sorted by
Tagged with
18 votes
3 answers
4k views

Why is unification so important to inference engines?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. I keep reading about the Unification Algorithm. ...
Guy Coder's user avatar
  • 5,101
5 votes
2 answers
497 views

Using SMT solvers to generate random solutions to given predicate

I am interested in generating random solutions to predicates. I only need SMT for integers with the following predicates/functions <, >, <=, >=, ==, !=, +, * The algorithm I want should produce ...
Jake's user avatar
  • 3,800
16 votes
2 answers
464 views

Why do some inference engines need human assistance while others don't?

I am learning Automated Theorem Proving / SMT solvers / Proof Assistants by myself and post a series of questions about the process, starting here. Why is it that automated theorem provers, i.e. ACL2,...
Guy Coder's user avatar
  • 5,101
-2 votes
1 answer
297 views

How a SMT / SAT Solver Generates Valuations for this Example

First, an example of a set of constraints which turned out not to be solvable (I don't think): ...
Lance's user avatar
  • 2,243