Sciweavers

CPAIOR
2007
Springer

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

14 years 14 days ago
On Boolean Functions Encodable as a Single Linear Pseudo-Boolean Constraint
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
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CPAIOR
Authors Jan-Georg Smaus
Comments (0)