|
|
Ein linearer pseudo-Boolescher Constraint (LPB) ist ein Ausdruck der Form a_1 l_1+...+a_m l_m ≥ d. Hierbei ist jedes l_i ein Literal der Form x_i or ¯x_i=1-x_i, d.h., x_i wird 0 wenn x_i falsch ist und 1 wenn x_i wahr ist, und umgekehrt für ¯x_i. Des weiteren sind a_1,...,a_m,d natürliche Zahlen. LPBs sind eine Verallgemeinerung von aussagenlogischen Klauseln. Boolesche Funktionen können mittels LPBs oft kompakter dargestellt werden als mittels konjunktiver oder disjunktiver Normalformen. Z.B. entspricht die LPB 2x_1+¯x_2+x_3+x_4≥2 der DNF x_1\/(¬ x_2/\ x_3)\/(¬ x_2/\ x_4)\/(x_3/\ x_4). Daher gibt es in der Literatur mehrere Ansätze, die Techniken aus dem SAT Solving (aussagenlogische Erfüllbarkeit) auf LPBs zu verallgemeinern. In diesen Arbeiten wird immer davon ausgegangen, dass sich die LPBs aus der Kodierung innerhalb der Problemdomäne natürlich ergeben.
|
