3 ms·
Hmmm.. but how did the theorem prover find the solution? Probably by heuristics + brute force.
by arghbleargh 12y ago
Hmmm.. but how did the theorem prover find the solution? Probably by heuristics + brute force.
- kaeso 12y ago"Z3 integrates a modern DPLL-based SAT solver, a core theory solver that handles equalities and uninterpreted functions, satellite solvers (for arithmetic, arrays, etc.), and an E-matching abstract machine (for quantifiers)" From http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.pdf http://research.microsoft.com/en-us/um/redmond/projects/z3/z...
- q3k 12y agoI'm not sure which one exactly, but it's a SAT solver, so it uses a SAT solving algorithm [1]. 1 - http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Algorithms_for_solving_SAT http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#...
- benjamincburns 12y agoI'm not well-versed on this topic, but I believe this [1] is presently the state of the art. I'd be curious to know whether or not Z3 performance beats GNU's prolog implementation for similar problem sets. 1: http://www.gprolog.org/#TOChead http://www.gprolog.org/#TOChead