Boolean satisfiability problem

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