4 ms·
You probably want to use SMT (which uses SAT underneath), not SAT directly. SMT solvers usually let you write constraints over numbers which is a more natural f
by darzu 7y ago
You probably want to use SMT (which uses SAT underneath), not SAT directly. SMT solvers usually let you write constraints over numbers which is a more natural fit for your problem.
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 https://rise4fun.com/Z3/tutorial/optimization
- sudhirj 7y agoThanks a lot, will check this out.
- sigstoat 7y ago> 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.
- pfdietz 7y agoAt 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).