Boolean satisfiability problem: Difference between revisions
Jump to navigation
Jump to search
m cat |
m →External links: category |
||
| Line 9: | Line 9: | ||
[[Category:Software| ]] | [[Category:Software| ]] | ||
[[Category:Search software| ]] | [[Category:Search software| ]] | ||
[[Category:Mathematical miscellany]] | |||
Revision as of 22:57, 24 March 2023
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.