Algebraic simplification techniques for propositional satisfiability

Abstract

The ability to reduce either the number of variables or clauses in instances of the Satisfiability problem (SAT) impacts the expected computational effort of solving a given instance. This ability can actually be essential for specific andha rdc lasses of instances. The objective of this paper is to propose new simplification techniques for Conjunctive Normal Form (CNF) formulas. Experimental results, obtainedon representative problem instances, indicate that large simplifications can be observed.