Journal of Applied Mathematics and Decision Sciences 
Volume 2005 (2005), Issue 2, Pages 61-74
doi:10.1155/JAMDS.2005.61

On the orthogonalization of arbitrary Boolean formulae

Renato Bruni

 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

Abstract

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.