Editing Boolean satisfiability problem (section)

==Algorithms for solving SAT==
{{main|SAT solver}}

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 during the 2000s and have contributed to dramatic advances in the ability to automatically solve problem instances involving tens of thousands of variables and millions of constraints (i.e. clauses).<ref name="Codish.Ohrimenko.Stuckey.2007">{{citation |title=Principles and Practice of Constraint Programming – CP 2007|series=Lecture Notes in Computer Science|volume=4741|year=2007|pages=544–558|contribution=Propagation = Lazy Clause Generation|first1=Olga|last1=Ohrimenko |first2=Peter J.|last2=Stuckey|first3=Michael|last3=Codish|doi=10.1007/978-3-540-74970-7_39|isbn=978-3-540-74969-1 |quote=modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables |citeseerx=10.1.1.70.5471}}.</ref> Examples of such problems in [[electronic design automation]] (EDA) include [[formal equivalence checking]], [[model checking]], [[formal verification]] of [[microprocessor|pipelined microprocessors]],<ref name="Bryant.German.Velev.1999"/> [[automatic test pattern generation]], [[routing (electronic design automation)|routing]] of [[FPGA]]s,<ref>{{Cite journal |last1=Gi-Joon Nam |last2=Sakallah |first2=K. A. |last3=Rutenbar |first3=R. A. |title=A new FPGA detailed routing approach via search-based Boolean satisfiability |journal=IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |volume=21 |issue=6 |pages=674 |year=2002 |url=http://cs-rutenbar.web.engr.illinois.edu/wp-content/uploads/2012/10/rutenbar-sattranscad02.pdf |doi=10.1109/TCAD.2002.1004311 |access-date=2015-09-04 |archive-date=2016-03-15 |archive-url=https://web.archive.org/web/20160315003856/http://cs-rutenbar.web.engr.illinois.edu/wp-content/uploads/2012/10/rutenbar-sattranscad02.pdf |url-status=dead }}</ref> [[Automated planning and scheduling|planning]], and [[Scheduling algorithm|scheduling problems]], and so on. A SAT-solving engine is also considered to be an essential component in the [[electronic design automation]] toolbox.

Major techniques used by modern SAT solvers include the [[Davis–Putnam–Logemann–Loveland algorithm]] (or DPLL), [[conflict-driven clause learning]] (CDCL), and [[stochastic]] [[Local search (constraint satisfaction)|local search]] algorithms such as [[WalkSAT]]. Almost all SAT solvers include time-outs, so they will terminate in reasonable time even if they cannot find a solution. Different SAT solvers will find different instances easy or hard, and some excel at proving unsatisfiability, and others at finding solutions. Recent{{When|date=June 2024}} attempts have been made to learn an instance's satisfiability using deep learning techniques.<ref>{{cite arXiv |last1=Selsam |first1=Daniel |last2=Lamm |first2=Matthew |last3=Bünz |first3=Benedikt |last4=Liang |first4=Percy |last5=de Moura |first5=Leonardo |last6=Dill |first6=David L. |title=Learning a SAT Solver from Single-Bit Supervision |eprint=1802.03685 |date=11 March 2019|class=cs.AI }}</ref>

SAT solvers are developed and compared in SAT-solving contests.<ref>{{cite web|url=http://www.satcompetition.org/ |title=The international SAT Competitions web page|access-date=2007-11-15}}</ref> Modern SAT solvers are also having significant impact on the fields of software verification, constraint solving in artificial intelligence, and operations research, among others.