Tseytin pointed out that there’s a simple way to get around the lower bounds he had proved for his graph-oriented problems, by allowing new kinds of proof steps: Given any set of axioms F, we can introduce a new variable z that doesn’t appear anywhere in F, and add three new clauses 
; here x and y are arbitrary literals of F. It’s clear that F is satisfiable if and only if F ∪ G is satisfiable, because G essentially says that z = NAND(x, y). Adding new variables in this way is somewhat analogous to using lemmas when proving a theorem, or to introducing a memo cache in a computer program.
His method, which is called extended resolution, can be much ...
Get The Art of Computer Programming: Satisfiability, Volume 4, Fascicle 6 now with the O’Reilly learning platform.
O’Reilly members experience books, live events, courses curated by job role, and more from O’Reilly and nearly 200 top publishers.
