Algebraic Simplification Techniques for Propositional Satisfiability

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 and hard classes of instances. The objective of this paper is to propose new simplification techniques for Conjunctive Normal Form (CNF) formulas. Experimental results, obtained on representative problem instances, indicate that large simplifications can be observed.

• Type: Conference
• Year: 2000
• Where: CP
• Authors: João P. Marques Silva
• Keywords: Artificial Intelligence, Conjunctive Normal Form, CP 2000, Representative Problem Instances, Satisfiability Problem