Re:Modern SAT solvers: fast, neat and underused
by sigstoat on Sunday May 19, 2019 @05:26PM
(#19955608)
> Also if you have thousands of variables, you probably shouldn't be writing SMT statements directly. Usually you have some sort of script for your problem domain that emits SMT then invokes the solver. E.g. the popular SMT solver Z3 has a very simple lisp-like syntax that's easy to emit from a script.
the follow on is that the same program should also process the model (answer) that Z3 produces and render it in a domain-appropriate fashion.
this is easiest if you use something like the python interface to Z3, instead of actually generating SMT-LIB sexps and feeding them to Z3.
Re:Modern SAT solvers: fast, neat and underused
by pfdietz on Monday May 20, 2019 @07:10AM
(#19959188)
At one point I wrote a Common Lisp interface to Z3. The syntax was nice, except that empty lists have to be printed as () rather than NIL. So close to working with no tweaks.
The hardest part is getting the model back at the end (well, and making problems that don't scale too badly with N).
Also if you have thousands of variables, you probably shouldn't be writing SMT statements directly. Usually you have some sort of script for your problem domain that emits SMT then invokes the solver. E.g. the popular SMT solver Z3 has a very simple lisp-like syntax that's easy to emit from a script.
As for changing costs, you might be able to use simple expressions like: costOfShippingXusingZ = 100 - numOfXusingZ * 2
Or you might use "soft constraints" that let you add weights to optional constraints.
It's important to note that with SMT/SAT solvers you generally want to keep your formulas linear or "first-order" which means don't multiply variables together if you can help it.
This might be useful: https://rise4fun.com/Z3/tutorial/optimization