Boolean Satisfiability Problem - Self-reducibility

Self-reducibility

An algorithm which correctly answers if an instance of SAT is solvable can be used to find a satisfying assignment. First, the question is asked on formula . If the answer is "no", the formula is unsatisfiable. Otherwise, the question is asked on, i.e. the first variable is assumed to be 0. If the answer is "no", it is assumed that, otherwise . Values of other variables are found subsequently.

This property is used in several theorems in complexity theory:

(Karp-Lipton theorem)