Technical Report No. 230 - Abstract

Jan-Georg Smaus
On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint

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 a_1,...,a_m,d are natural numbers. An LPB is a generalisation of a propositional clause, on the other hand it is a restriction of integer linear programming. 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 give an algorithm for computing an LPB representation of a given formula if this is possible.