# Difference between revisions of "Solvers"

m (→SMT Solvers) |
m (→SMT Solvers) |
||

Line 18: | Line 18: | ||

* [https://rise4fun.com/z3/tutorial z3Tutorial with online solver] | * [https://rise4fun.com/z3/tutorial z3Tutorial with online solver] | ||

* https://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models | * https://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models | ||

+ | SMT-LIB standard (read this): | ||

+ | * http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf | ||

I have put together a git repo of some of my very simple z3 scripts: | I have put together a git repo of some of my very simple z3 scripts: | ||

− | * https://github.com/simsong/ | + | * https://github.com/simsong/z3slg |

=Optimizers= | =Optimizers= | ||

Optimizers are special kinds of solvers that can optimize an objective function. Convex linear optimizers that can work with floating point numbers are relatively fast, as linear programming is in P, but requiring an integer solution makes finding some problems tricky and creates an NP-hard problem. [https://cs.stackexchange.com/questions/40366/why-is-linear-programming-in-p-but-integer-programming-np-hard|Ref] | Optimizers are special kinds of solvers that can optimize an objective function. Convex linear optimizers that can work with floating point numbers are relatively fast, as linear programming is in P, but requiring an integer solution makes finding some problems tricky and creates an NP-hard problem. [https://cs.stackexchange.com/questions/40366/why-is-linear-programming-in-p-but-integer-programming-np-hard|Ref] |

## Revision as of 20:17, 4 December 2019

# SAT Solvers

SAT Solvers are programs that can solve SAT (Satisfiability), an NP-complete program. SAT solvers typically take their input in the DIMACS format. That's hard to work with, so there are pre-processors that will convert a problem into DIMACS, give it to a SAT solver, and then convert the solution back to a specific problem domain. Such conversions are in P.

I've used the following SAT solvers successfully:

- picosat - easy to get working, but not very fast. Has the advantage that it can produce a list of all possible solutions out-of-the-box.
- glucose - like picosat, but fast. Does not have the ability to produce all possible solutions.
- Z3 - Can process DIMACS files.

# SMT Solvers

SMT solvers can work with higher level "theories" in math or logic. Because they can operate on logic directly, rather than converting everything into SAT, their models can be much more compact. More compact models may solve faster or slower, depending on the heuristics of the particular solver.

Most SMT solvers will take an input file in the SMT-LIB file format.

Getting started with SMT-LIB:

- Start with Z3. You can download it and run it with SMT-LIB files, or install z3-solver with pip.
- https://github.com/Z3Prover/z3/wiki
- z3Tutorial with online solver
- https://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models

SMT-LIB standard (read this):

I have put together a git repo of some of my very simple z3 scripts:

# Optimizers

Optimizers are special kinds of solvers that can optimize an objective function. Convex linear optimizers that can work with floating point numbers are relatively fast, as linear programming is in P, but requiring an integer solution makes finding some problems tricky and creates an NP-hard problem. [1]