SAT solver
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.
This article is issued from Conwaylife. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.