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?
Artificial Intelligence Stack Exchange is a question and answer site for people interested in conceptual questions about life and challenges in a world where "cognitive" functions can be mimicked in purely digital environment. It only takes a minute to sign up.Sign up to join this community
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). Examples of such problems in electronic design automation (EDA) include formal equivalence checking, model checking, formal verification of pipelined microprocessors, automatic test pattern generation, routing of FPGAs, planning, and scheduling problems, and so on. A SAT-solving engine is now considered to be an essential component in the EDA toolbox.