Journal of Applied Mathematics and Decision Sciences
Volume 2005 (2005), Issue 2, Pages 61-74
On the orthogonalization of arbitrary Boolean formulae
Dipartimento di Informatica e Sistemistica, Università di Roma “La Sapienza”, Via Michelangelo Buonarroti 12, Roma 00185, Italy
Received 15 October 2002; Revised 19 March 2004
Copyright © 2005 Renato Bruni. This is an open access article distributed under the Creative Commons Attribution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited.
The orthogonal conjunctive normal form of a Boolean function is a conjunctive normal form in which any two clauses contain at least a pair of complementary literals. Orthogonal disjunctive normal form is defined similarly. Orthogonalization is the process of transforming the normal form of a Boolean function to orthogonal normal form. The problem is of great relevance in several applications, for example, in the reliability theory. Moreover, such problem is strongly connected with the well-known propositional satisfiability problem. Therefore, important complexity issues are involved. A general procedure for transforming an arbitrary CNF or DNF to an orthogonal one is proposed. Such procedure is tested on randomly generated Boolean formulae.