Technical Report No. 227 - Abstract

Jan-Georg Smaus
Representing Boolean Functions as Linear Pseudo-Boolean Constraints

A linear pseudo-Boolean constraint (LPB) is an expression of the form a_1*l_1+...+a_m*l_m>= d, where each l_i is a literal (it assumes the value 1 or 0 depending on whether a propositional variable x_i is true or false) and the a_1,...,a_m,d are natural numbers. The formalism can be viewed as a generalisation of a propositional clause. It has been said that LPBs can be used to represent Boolean functions more compactly than the well-known conjunctive or disjunctive normal forms. In this paper, we address the question: how much more compactly? We compare the expressiveness of a single LPB to that of related formalisms, and we give a statement that outlines how the problem of computing an LPB representation of a given CNF or DNF might be solved recursively. However, there is currently still a missing link for this to be a full algorithm.