What are the real world uses for SAT solvers?

Question

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?

Answer 1

One actual example of SAT solvers is finding the set of compatible package versions in python conda package manager.

(see, for example, https://www.anaconda.com/blog/understanding-and-improving-condas-performance)

The practical applications of SAT solvers involve as well (see http://www.carstensinz.de/talks/RISC-2005.pdf):

• Product Configuration
• Hardware Verification
• Bounded Model Checking
• (Hardware) Equivalence Checking
• Asynchronous circuit synthesis (IBM)
• Software-Verification
• Expert system verification
• Planning (air-traffic control, telegraph routing)
• Scheduling (sport tournaments)
• Finite mathematics (quasigroups)
• Cryptanalysis

Answer 2

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.