7 ms·

I’ve had a supply demand problem that I couldn’t figure out how to use a SAT solver for - thousands of demands ( movies have to reach thousands of theatres) wit

I’ve had a supply demand problem that I couldn’t figure out how to use a SAT solver for - thousands of demands ( movies have to reach thousands of theatres) with tens of possible paths (fedex, satellite, download) - each at different costs, some impossible and costs will change with volume and consideration of other similar deliveries. Have a solution that models each choice of supply demand tuples as nodes in a tree and doing depth first search on it. Any ideas on how to switch to an SAT solver? How would I even write such a large SAT Boolean expression, and how would I tell the SAT solver that the costs will change for each choice depending on business rules and other choices made? It seemed impossible with a SAT system but I assume I’m not familiar enough with the concepts.

ahmedalsudani 7y ago
What are you trying to do? Show that deliveries can be made or minimize the cost? If you’re minimizing the cost, shouldn’t this be formulated as an optimization problem?
- jvanderbot 7y ago
  Yes. That's a MILP. And if we think SAT solvers are useful and underused, wait till you start working with MILP solvers.
  - nickpsecurity 7y ago
    I think it was this year I learned they exist. They told me a few to check out. I still don't have a list of applications. What areas were you thinking about when you said underused?
  - shaklee3 7y ago
    Yes, yes, yes. I've made this comment a few times on here but tools like MIP solvers are vastly unknown since they didn't take on a sexy name when they started out. However, they can outperform most heuristic based algorithms, and even solve some of the largest problems. It's how the NFL makes their schedules oh, and you can imagine how complicated that is.
    - new4thaccount 7y ago
      Fun fact. Most power grids in the developed world are run off of some of the largest MILP and LP problems. We're talking about millions of constraints to commit units and hundreds of thousands to dispatch them. These run around the clock 24/7. I've only recently learned about SAT type solvers as MILP/LP problems are very fast and globally optimal, unlike things like A* or Genetic Algorithms. I think GA's are cool because you can write one in less than 1/2 page of Python, where MIP solvers are usually large black-box C codesets (Ex: GLPK, CPLEX, GUROBI, XPRESS, Open-Solver).
      - jvanderbot 7y ago
        GA does not belong anywhere near real problems. They are toy solutions with zero guarantees. Fun to code though!
        new4thaccount 7y ago
        Sadly, I've mostly come to the same conclusion in that I at least need a MIP Gap to tell me how far I am from the optimal solution. My only issue with LP and MILP solvers is scalibility. You have none! Multicore doesn't really seem to help any.
  - svd4anything 7y ago
    Ssshhh ... Stop telling everyone. I have rewritten various problems as MILP it finds a solution and people think I’m smart! My favorite MILP is commercial and perhaps somewhat obscure for general population - Mosek. Any recommendations in regards to other good options? perhaps open source that might be in same or better league.
    - throwawaymath 7y ago
      Gurobi, CPLEX and XPRESS are the obvious commercial ones. GLPK and Cbc will also do MILP. For more information, see this page: http://plato.asu.edu/guide.html http://plato.asu.edu/guide.html
      - svd4anything 7y ago
        Thank you so much. Very nice collection of information.
- sudhirj 7y ago
  Cost minimisation, so yes, it is an optimisation problem, and I haven’t heard of MILPs, will check them out. Is that a Prolog style constraint solver? And would it support dynamic constraints, where some choices will render others impossible (inventory / bandwidth exhaustion)?
wongarsu 7y ago
It sounds like you should be able to transform the tree into a graph that encodes every possible intermediate state and use a path finding algorithm to find the shortest path from "nothing delivered" to "everything delivered". A* might work well since it sounds like you can fairly easily calculate a minimum bound for the cost to get from anywhere to the "fully delivered" state.
- whatshisface 7y ago
  How would A* perform on a graph with 2^n nodes?
  - user5994461 7y ago
    It can perform very well if you happen to have a good heuristic function for that problem and that data. However large graphs might not fit in memory.
    - sudhirj 7y ago
      Yeah, the highlight of my current solution is that the graph is computed lazily / on demand (supplies are passed in the current path and provide estimates) - very CPU heavy but light on memory. There no way I can precompute every possibility, but is there anything specific to A* that rules out lazy node creation? In this problem the nature of every node is a function of the path you took to get there.
      - wongarsu 7y ago
        You need memory proportional to the number of nodes you visit (score of the node, previous node on the shortes path to this node, list of next candidates). There is nothing preventing you from creating everything else lazily, and in practise most nodes will never get visited. A* also allows you to find a solution faster by overestimating your heuristic: For example if you multiply your heurisitic with 1.1 you are guaranteed to find a path whose length is within 10% of the shortest path, requiring less CPU time and memory for the search.
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 ago
  Thanks 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 ago
  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).

ahmedalsudani 7y ago

What are you trying to do? Show that deliveries can be made or minimize the cost? If you’re minimizing the cost, shouldn’t this be formulated as an optimization problem?

jvanderbot 7y ago
Yes. That's a MILP. And if we think SAT solvers are useful and underused, wait till you start working with MILP solvers.
- nickpsecurity 7y ago
  I think it was this year I learned they exist. They told me a few to check out. I still don't have a list of applications. What areas were you thinking about when you said underused?
- shaklee3 7y ago
  Yes, yes, yes. I've made this comment a few times on here but tools like MIP solvers are vastly unknown since they didn't take on a sexy name when they started out. However, they can outperform most heuristic based algorithms, and even solve some of the largest problems. It's how the NFL makes their schedules oh, and you can imagine how complicated that is.
  - new4thaccount 7y ago
    Fun fact. Most power grids in the developed world are run off of some of the largest MILP and LP problems. We're talking about millions of constraints to commit units and hundreds of thousands to dispatch them. These run around the clock 24/7. I've only recently learned about SAT type solvers as MILP/LP problems are very fast and globally optimal, unlike things like A* or Genetic Algorithms. I think GA's are cool because you can write one in less than 1/2 page of Python, where MIP solvers are usually large black-box C codesets (Ex: GLPK, CPLEX, GUROBI, XPRESS, Open-Solver).
    - jvanderbot 7y ago
      GA does not belong anywhere near real problems. They are toy solutions with zero guarantees. Fun to code though!
      - new4thaccount 7y ago
        Sadly, I've mostly come to the same conclusion in that I at least need a MIP Gap to tell me how far I am from the optimal solution. My only issue with LP and MILP solvers is scalibility. You have none! Multicore doesn't really seem to help any.
- svd4anything 7y ago
  Ssshhh ... Stop telling everyone. I have rewritten various problems as MILP it finds a solution and people think I’m smart! My favorite MILP is commercial and perhaps somewhat obscure for general population - Mosek. Any recommendations in regards to other good options? perhaps open source that might be in same or better league.
  - throwawaymath 7y ago
    Gurobi, CPLEX and XPRESS are the obvious commercial ones. GLPK and Cbc will also do MILP. For more information, see this page: http://plato.asu.edu/guide.html http://plato.asu.edu/guide.html
    - svd4anything 7y ago
      Thank you so much. Very nice collection of information.
sudhirj 7y ago
Cost minimisation, so yes, it is an optimisation problem, and I haven’t heard of MILPs, will check them out. Is that a Prolog style constraint solver? And would it support dynamic constraints, where some choices will render others impossible (inventory / bandwidth exhaustion)?

wongarsu 7y ago

It sounds like you should be able to transform the tree into a graph that encodes every possible intermediate state and use a path finding algorithm to find the shortest path from "nothing delivered" to "everything delivered". A* might work well since it sounds like you can fairly easily calculate a minimum bound for the cost to get from anywhere to the "fully delivered" state.

whatshisface 7y ago
How would A* perform on a graph with 2^n nodes?
- user5994461 7y ago
  It can perform very well if you happen to have a good heuristic function for that problem and that data. However large graphs might not fit in memory.
  - sudhirj 7y ago
    Yeah, the highlight of my current solution is that the graph is computed lazily / on demand (supplies are passed in the current path and provide estimates) - very CPU heavy but light on memory. There no way I can precompute every possibility, but is there anything specific to A* that rules out lazy node creation? In this problem the nature of every node is a function of the path you took to get there.
    - wongarsu 7y ago
      You need memory proportional to the number of nodes you visit (score of the node, previous node on the shortes path to this node, list of next candidates). There is nothing preventing you from creating everything else lazily, and in practise most nodes will never get visited. A* also allows you to find a solution faster by overestimating your heuristic: For example if you multiply your heurisitic with 1.1 you are guaranteed to find a path whose length is within 10% of the shortest path, requiring less CPU time and memory for the search.

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 ago
Thanks 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 ago
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).