zbMATH — the first resource for mathematics

Algebraic simplification techniques for propositional satisfiability. (English) Zbl 1044.68781
Dechter, Rina (ed.), Principles and practice of constraint programming - CP 2000. 6th international conference, Singapore, September 18–21, 2000. Proceedings. Berlin: Springer (ISBN 3-540-41053-8). Lect. Notes Comput. Sci. 1894, 537-542 (2000).
Summary: 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.
For the entire collection see [Zbl 0947.00041].

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX Cite
Full Text: Link