A linear pseudo-Boolean constraint (LPB) [1,4,5] is an expression of the form a_1ℓ_1 +...+ a_mℓ_m ≥ d. Here each ℓ_i is a literal of the form x_i or 1 - x_i. An LPB can be used to represent a Boolean function; e.g. 2x_1 + x_2 + x_3 ≥ 2 represents the same function as the propositional formula x_1 ∨ (x_1 ∧ x_3). Functions that can be represented by a single LPB are called threshold functions. The problem of finding the LPB for a threshold function given as disjunctive normal form (DNF) is called threshold synthesis problem. The reference on Boolean functions [4] formulates the research challenge of recognising threshold functions through an entirely combinatorial procedure. In fact, such a procedure had been proposed in [3,2] and was later reinvented by us [7]. In this paper, we report on an implementation of this procedure for which we have run experiments for up to m = 22. It can solve the biggest problems in a couple of seconds.
展开▼
