What SAT-solvers Can and Cannot Do
Eugene Goldberg · Kluwer Academic Publishers eBooks · 2006
This chapter consists of two parts. In the first part we show that resolution based SAT-solvers cannot be scalable on real-life formulas unless some extra information about formula structure is known. In the second part we introduce a new way of satisfiability testing that may be used for designing more efficient and “intelligent” SAT-algorithms that will be able to take into account formula structure.