The Interaction Between Simplification and Search in Propositional Satisfiability
Inês Lynce, João P. Marques-Silva · ePrints Soton (University of Southampton) · 2001
Simplification techniques have been extensively applied to formulas in Conjunctive Normal Form (CNF). Consequently, different models of the same problem can be obtained by using different techniques, namely by reducing either the number of variables or clauses, and by inferring new clauses.