Decision procedures that determine whter or not a given propositional formula is valid play an important role in Computer Science, Mathematical Logic, Artificial Intelligence. Applications of these procedures range from automated theorem proving to hardware circuit validation. The property of validity for propositional calculus is perhaps the most notorious NP-complete problem. In fact, most of these procedures determine satisfiability of propositional formulas as opposed to their validity but due to the duality of these problems, it does not matter which of the two you deal with. The volume of research in this field is just enormous.
The focus of this reasearch has always been on formulas in conjunctive normal form. It actually was the resolution principle that turned researches to looking exclusively at conjuctive normal forms. Reasoning about formulas in conjuctive normal form is very opposite to how humans reason. Conversion of formulas to conjuctive normal form fully destroys formula structure. Besides, this conversion is an expensive procedure in itself and it leads to a significant size increase. Only recently, some researches turned back to more natural representations of propositional formulas. Some of the newest (and in my opinion best) decision procedures work with negational normal forms. So does a decision procedure I developed. Negational normal forms possess some nice properties characteristic to normal forms. At the same time, conversion to neagtional normal form is quick, and the formula structure is preserved in this conversion.
My procedure for testing the validity problem of propositional formulas is based on the Davis-Putnam method (like many others), and it deals with propositional formulas that are initially converted to negational normal form. This procedure splits variables but, in contrast to all other decision procedures based on the Davis-Putnam method, it does not branch. Instead, this procedure iteratively makes validity-preserving transformations of fragments of the formula after selecting a variable for splitting. The transformations involve only a minimal formula part containing occurrences of the selected variable. Selection of the best variable for splitting is crucial in this decision procedure - it shortens the decision process dramatically in many instances. A variable whose splitting leads to a minimal size of the transformed formula is selected. Also, my decision procedure performs plenty of optimizations based on calculation of delta-sets. Some optimizations lead to removing fragments of the formula. Others detect variables for which a single truth value assignment is sufficient.
My paper on this topic is available for download from the Arxiv preprint server:
|Abstract and Full Text|
has not been implemented yet. If anyone are interested in participating in its
implementation and benchmarking, please drop me email.
Need to relax? Try brain teasers. I would recommend those marked 'cool'.