3
$\begingroup$

Why somebody would use SAT solvers (Boolean satisfiability problem) to solve their real world problems?

Are there any examples of the real uses of this model?

$\endgroup$
  • $\begingroup$ This question is vague. Are you asking only about SAT solvers or not? There are different types of solvers. $\endgroup$ – nbro Sep 14 '17 at 16:11
1
$\begingroup$

Instead of talking about just SAT solvers, let me talk about optimization in general. Many economic problems can be cast as optimization problems: for example, FedEx may have a list of packages and the destinations for those packages, and must decide which packages to put on which trucks, and what order to deliver those packages in.

If you write out a mathematical description of this problem, there are a truly stunning number of possible solutions, and a well-defined way to evaluate which of two solutions is better. A solver is an algorithm that will evaluate a solution, come up with another solution, and then evaluate that one, and so on.

In small cases and simple problems, the solver can also terminate with a proof that it is actually the best solution possible. But typically instead the solver just reports "this is the best solution that I've seen," and that's used. An improvement in the solver means you can reliably get lower-cost solutions than you were seeing before.

For the SAT problem specifically, the Wikipedia page on SAT gives some examples:

Since the SAT problem is NP-complete, only algorithms with exponential worst-case complexity are known for it. In spite of this, efficient and scalable algorithms for SAT were developed over the last decade[when?] and have contributed to dramatic advances in our ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints (i.e. clauses).[1] Examples of such problems in electronic design automation (EDA) include formal equivalence checking, model checking, formal verification of pipelined microprocessors,[12] automatic test pattern generation, routing of FPGAs,[14] planning, and scheduling problems, and so on. A SAT-solving engine is now considered to be an essential component in the EDA toolbox.

$\endgroup$
  • $\begingroup$ We are focused on pure mathematics, that means everything which has to do with optimization theory. Or to be more specific, with state-spaces in general. In contrast, simulation games in a logic planning system is outside of our scope. Dedicated PDDL to SAT Compiler may be described in the literature but they were only used by amateurs for solving role-playing games, transport domans and natural language questions. $\endgroup$ – Manuel Rodriguez Aug 26 '18 at 8:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.