Boolean satisfiability problem: Difference between revisions
m →External links: category |
m Confocal moved page SAT solver to Boolean satisfiability problem: name the page after the problem to be solved |
||
| (One intermediate revision by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Glossary}} | {{Glossary}} | ||
''' | The '''Boolean satisfiability problem''' is the problem of determining whether the variables of a given Boolean formula can be consistently replaced by the values "true" or "false" in such a way that the formula evaluates to "true". | ||
A '''SAT solver''' is a software tool used to algorithmically solve Boolean satisfiability problems, or alternately prove that that no solution exists (i.e. that the problem is unsatisfiable). | |||
On input a formula over Boolean variables, such as {{nowrap|"(''x'' or ''y'') and (''x'' or not ''y'')"}}, a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of ''x'' and ''y'' which make the formula true, or unsatisfiable, meaning that there are no such values of ''x'' and ''y''. | |||
SAT solvers gained prominence in the [[Conway's Game of Life|Conway Life]] community in the late 2010s with the advent of [[search program]]s such as [[Oscar Cunningham]]'s [[Logic Life Search|LLS]] and [[Adam P. Goucher]]'s [[ikpx]]. [[Sir Robin]], the first known [[elementary]] [[knightship]] in Conway Life, is an example of a pattern found with the help of SAT solvers. | SAT solvers gained prominence in the [[Conway's Game of Life|Conway Life]] community in the late 2010s with the advent of [[search program]]s such as [[Oscar Cunningham]]'s [[Logic Life Search|LLS]] and [[Adam P. Goucher]]'s [[ikpx]]. [[Sir Robin]], the first known [[elementary]] [[knightship]] in Conway Life, is an example of a pattern found with the help of SAT solvers. | ||
| Line 6: | Line 9: | ||
==External links== | ==External links== | ||
* {{LinkWikipedia|Boolean_satisfiability_problem#Algorithms_for_solving_SAT|name=Boolean satisfiability problem § Algorithms for solving SAT}} | * {{LinkWikipedia|Boolean_satisfiability_problem#Algorithms_for_solving_SAT|name=Boolean satisfiability problem § Algorithms for solving SAT}} | ||
* {{LinkWikipedia|SAT_solver|name=SAT solver}} | |||
[[Category:Software| ]] | [[Category:Software| ]] | ||
[[Category:Search software| ]] | [[Category:Search software| ]] | ||
[[Category:Mathematical miscellany]] | [[Category:Mathematical miscellany]] | ||
Latest revision as of 19:09, 30 March 2023
The Boolean satisfiability problem is the problem of determining whether the variables of a given Boolean formula can be consistently replaced by the values "true" or "false" in such a way that the formula evaluates to "true".
A SAT solver is a software tool used to algorithmically solve Boolean satisfiability problems, or alternately prove that that no solution exists (i.e. that the problem is unsatisfiable). On input a formula over Boolean variables, such as "(x or y) and (x or not y)", a SAT solver outputs whether the formula is satisfiable, meaning that there are possible values of x and y which make the formula true, or unsatisfiable, meaning that there are no such values of x and y.
SAT solvers gained prominence in the Conway Life community in the late 2010s with the advent of search programs such as Oscar Cunningham's LLS and Adam P. Goucher's ikpx. Sir Robin, the first known elementary knightship in Conway Life, is an example of a pattern found with the help of SAT solvers.
External links
- Boolean satisfiability problem § Algorithms for solving SAT at Wikipedia
- SAT solver at Wikipedia