Solvers - Revision history

Simson: /* Other solvers */

2019-12-05T14:16:16Z

Other solvers

← Older revision		Revision as of 07:16, 5 December 2019
Line 35:		Line 35:
	==Other solvers==		==Other solvers==

	Yices is another solver worth looking at. I’ll be doing that shortly:		''Yices'' is another solver worth looking at. I’ll be doing that shortly:
	* http://smt2015.csl.sri.com/wp-content/uploads/2015/06/2015-Dutertre-Solving-Exists-Forall-Problems-With-Yices.pdf		* http://smt2015.csl.sri.com/wp-content/uploads/2015/06/2015-Dutertre-Solving-Exists-Forall-Problems-With-Yices.pdf

			''CVC4''

			''MathSAT''

			''veriT'' is a prototype server currently under development

	=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]

Simson: /* SMT Solvers */

2019-12-05T14:15:11Z

SMT Solvers

← Older revision		Revision as of 07:15, 5 December 2019
Line 16:		Line 16:
	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.		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.		Most SMT solvers will take an input file in the SMT-LIB file format, which looks a lot like LISP. However, several of the SMT solvers also have a higher level API in Python or another language. People who are not familiar with LISP may find these APIs easier to work with

	Getting started with SMT-LIB:		Getting started with SMT-LIB:

	* ~~Start~~ with Z3. ~~You can~~ download it and ~~run it with SMT-LIB files, or install~~ [~~https~~://~~pypi~~.~~org~~/~~project~~/z3-~~solver/ z3~~-~~solver with pip~~].		* First, start by looking at the [https://rise4fun.com/z3/tutorial Rise4Fun z3Tutorial with online solver].
	* https://github.com/Z3Prover/z3/wiki
	* [https://~~rise4fun~~.~~com~~/z3/~~tutorial z3Tutorial~~ with ~~online solver]~~		* Next, download and skim the [http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf SMT-LIB Reference Manual]. Most of it won't make sense for now, as it is very dense, but after you have read it a few times it begins to make sense.

			* Next install a solver on your computer. I have found the Z3 is the easiest to use out of the box. You can download it [https://github.com/Z3Prover/z3/wiki from github], or you can install it for Python [https://pypi.org/project/z3-solver/ using pip].

			One of the things you might want to do with an SMT-LIB file is to get the model (that is, the satisfying solution). You do that with the '''(get-model)''' command. One of the things that I want to do is to get all satisfying models. I have found these links useful for that:

	* 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:
			* https://github.com/simsong/z3slg

			==Other solvers==

	Yices is another solver worth looking at. I’ll be doing that shortly:		Yices is another solver worth looking at. I’ll be doing that shortly:
	* http://smt2015.csl.sri.com/wp-content/uploads/2015/06/2015-Dutertre-Solving-Exists-Forall-Problems-With-Yices.pdf		* http://smt2015.csl.sri.com/wp-content/uploads/2015/06/2015-Dutertre-Solving-Exists-Forall-Problems-With-Yices.pdf

	~~I have put together a git repo of some of my very simple z3 scripts:~~
	* 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]

Simson: /* SAT Solvers */

2019-12-05T14:09:46Z

SAT Solvers

← Older revision		Revision as of 07:09, 5 December 2019
Line 5:		Line 5:
	* 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.		* 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.		* glucose - like picosat, but fast. Does not have the ability to produce all possible solutions.
	* Z3 - Can process DIMACS files.		* Z3 - Can process DIMACS files.

			I was not able to get these to work:
			* minisat - just couldn't get it to compile.

			I haven't used these:
			* veriT-SAT - Can read DIMACS formatted SAT files.

	=SMT Solvers=		=SMT Solvers=

Simson: /* SMT Solvers */

2019-12-05T04:26:30Z

SMT Solvers

← Older revision		Revision as of 21:26, 4 December 2019
Line 20:		Line 20:
	SMT-LIB standard (read this):		SMT-LIB standard (read this):
	* http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf		* http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf

			Yices is another solver worth looking at. I’ll be doing that shortly:
			* http://smt2015.csl.sri.com/wp-content/uploads/2015/06/2015-Dutertre-Solving-Exists-Forall-Problems-With-Yices.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:

Simson: /* SMT Solvers */

2019-12-05T04:17:38Z

SMT Solvers

← Older revision		Revision as of 21:17, 4 December 2019
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/z3		* 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]

Simson: /* SMT Solvers */

2019-12-05T04:04:05Z

SMT Solvers

← Older revision		Revision as of 21:04, 4 December 2019
Line 11:		Line 11:

	Most SMT solvers will take an input file in the SMT-LIB file format.		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 [https://pypi.org/project/z3-solver/ z3-solver with pip].
			* https://github.com/Z3Prover/z3/wiki
			* [https://rise4fun.com/z3/tutorial z3Tutorial with online solver]
			* https://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models

			I have put together a git repo of some of my very simple z3 scripts:
			* https://github.com/simsong/z3

	=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]

Simson: Created page with "=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..."

2019-12-04T22:36:47Z

Created page with "=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..."

New page

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

=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]