Boolean satisfiability problem
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.