On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint

13 years 10 months ago

Download www.informatik.uni-freiburg.de

A linear pseudo-Boolean constraint (LPB) is an expression of the form a1 · 1 + . . . + am · m ≥ d, where each i is a literal (it assumes the value 1 or 0 depending on whether a propositional variable xi is true or false) and a1, . . . , am, 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. Note: This report is the long version of [18] and contains the proofs omitted there for space reasons.

Jan-Georg Smaus

Real-time Traffic