Boolean satisfiability problem: Difference between revisions
Jump to navigation
Jump to search
Apple Bottom (talk | contribs) New stub |
m cat |
||
| Line 5: | Line 5: | ||
==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}} | ||
[[Category:Software]] | [[Category:Software| ]] | ||
[[Category:Search software| ]] | |||
Revision as of 05:55, 8 December 2022
SAT solvers (boolean satisfiability solvers) are a class of software tools used to algorithmically solve boolean satisfiability problems, or alternately prove that that no solution exists (i.e. that the problem is unsatisfiable).
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.