Cardinality Constraints X37043

Statement

optilog

html

Write a program in Python that, using the optilog library, finds all solutions of a set of cardinality constraints.

A set of cardinality constraints is a set of inequalities like:

x₁ + x₂ ≥ 1

x₂ + x₃ + x₄ ≥ 2

x₁ + x₂ + x₃ + x₄ ≤ 2

They can be translated into SAT using sequential counters:

S₁¹ ↔ x₁
S_iⁱ ↔ S_i−1ⁱ⁻¹ ∧ x_i	i=2,…,k
S_i¹ ↔ S_i−1¹ ∨ x_i	i=2,…,n
S_i^j ↔ S_i−1^j ∨ (x_i ∧ S_i−1^j−1)	i=3,…,n, j=2,…,min{i−1,k}

The clause S_n^k plus the clauses defining the right implications of the previous equivalences enforce x₁+⋯+x_n≥ k. In the last equivalence, for instance, the clauses are:

S_i^j → S_i−1^j ∨ (x_i ∧ S_i−1^j−1) ≡

⎧
⎪
⎪
⎨
⎪
⎪
⎩

S_i^j

∨ S_i−1^j∨ S_i−1^j−1 ≡

S_i^j

∨ S_i−1^j−1

S_i^j

∨ S_i−1^j∨ x_i

The constraint x₁ + ⋯ + x_n ≥ k is interpreted as: the number of variables assigned to true is at least k. The minus sign is interpreted as negation. Therefore, x₁ − x₂ ≥ 2 is interpreted as: both x₁ and x₂ are both true. Therefore, as inequality, it is in fact x₁ + (1− x₂) ≥ 2 that has a unique solution x₁=1, x₂= 0.

Input

The input is a text (in the stdin) with pairs of connected nodes. For instance, the following text in the case of our example:

x1 + x2 > 1
x2 + x3 + x4 > 2
x1 + x2 + x3 + x4 < 2

Output

The output is also a text (in the stdout) where in every line there is a variable assignment (variables assigned to 1 (true) as possitive, and those assigned to 0 (false) as negative. In this example:

{ -x1 x2 x3 -x4 }
{ -x1 x2 -x3 x4 }

Scoring

Public test cases

Input

x1 + x2 + x3 > 2
x1 + x2 + x3 < 2

Output

{ -x1 x2 x3 }
{ x1 -x2 x3 }
{ x1 x2 -x3 }

Input

x1 + x2 > 1
x2 + x3 + x4 > 2
x1 + x2 + x3 + x4 < 2

Output

{ -x1 x2 x3 -x4 }
{ -x1 x2 -x3 x4 }

Input

x1 - x2 > 2

Output

{ x1 -x2 }

Information

Author: Jordi Levy
Language: English
Official solutions: Python
User solutions: Python