Mind the Gap: Bit-vector Interpolation recast over Linear Integer Arithmetic
87
Observe from Figure 2(c) that
0 ≤ x + 2y − 4 ≤ 1
LIA
=
0 ≤ x + 2y − 4 ≤ 1
BV
∩
box BV (1, 2; 5)
BV
and moreover 0 mod 8 = 0 ≤ (x + 2y − 4) mod 8 for all (x, y) ∈ M
2 thus
0 ≤ x + 2y − 4 ≤ 1
LIA
=
x + 2y − 4 ≤ 1 ∧ box BV (1, 2; 5)
BV
therefore cumulatively
x + 2y ≤ 5
LIA
=
ϕ 1 ∨ ϕ 2
BV
where
ϕ 1 = [x + 2y ≤ 3
∧ (x ≤ 3 ∧ y ≤ 1)]
ϕ 2 = [x + 2y − 4 ≤ 1 ∧ ((x ≤ 3 ∧ y ≤ 3) ∨ (x ≤ 7 ∧ y ≤ 1))]
The general rule of the separation of the given inequality and the boxing is
shown in this theorem:
Theorem 2 (boxing with gapping). Let c ∈ N
d and b ∈ N.
d
i=1 c i x i ≤ b
LIA
=
φ 0 ∨ φ 1 ∨ φ 2
BV
where S = b/(m/2) and
φ 0 ≡
d
i=1 c i x i − (S − 2)(m/2) ≤ m/2 − 1
∧ box BV (c; (S − 1)(m/2) − 1)
φ 1 ≡
d
i=1 c i x i − (S − 1)(m/2) ≤ m/2 − 1
∧ box BV (c; S(m/2) − 1)
φ 2 ≡
d
i=1 c i x i − S(m/2) ≤ b mod (m/2)
∧ box BV (c; b)
Corollary 2 (boxing and gapping with simplification). If b/(m/2) = 1
or b mod m = m/2 − 1 then
d
i=1 c i x i ≤ b
LIA
=
φ 1 ∨ φ 2
BV
.
Example 5. Let m = 8 and consider again x + 2y ≤ 5 so that c = 1, 2. Then
S = 5/4 = 1 and, applying corollary 2,
x + 2y ≤ 5
LIA
=
φ 1 ∨ φ 2
BV
where
φ 1 ≡ (x + 2y − 0 · 4 ≤ 4 − 1)
∧ box BV (c; 1 · 4 − 1) = ϕ 1
φ 2 ≡ (x + 2y − 1 · 4 ≤ 5 mod 4) ∧ box BV (c; 5)
= ϕ 2
aligning with the intuition given in example 4.
Example 6. Figure 3 illustrates Theorem 2 for 7x + 3y ≤ 17 and m = 8. Then
S = 17/(8/2) = 4 and
7x + 3y ≤ 17
LIA
=
φ 0 ∨ φ 1 ∨ φ 2
BV
where
φ 0 = 7x + 3y − 8 ≤ 3 ∧ box BV (c; 11)
φ 1 = 7x + 3y − 12 ≤ 3 ∧ box BV (c; 15)
φ 2 = 7x + 3y − 16 ≤ 1 ∧ box BV (c; 17)
The box BV (c; 11), box BV (c, 15), box BV (c; 17) formulae are again depicted in grey.
For example,
box BV (c; 11) = (x ≤ 0 ∧ y ≤ 3) ∨ (x ≤ 1 ∧ y ≤ 2) ∨ (x ≤ 1 ∧ y ≤ 1)
because d = 2, L = 3 and I 2 ((d−1)(L+1)) = {{1, 3, 2, 2, 3, 1}. From Figure 3
observe
7x + 3y ≤ 17
LIA
=
φ 0
BV
∪
φ 1
BV
∪
φ 2
BV
.
Example 7. Consider again example 5 where S = 1. Then φ 0 = false because
box BV (c; (S − 1)(m/2) − 1) = box BV (c; −1) = false. This is because L = 0
and I d ((d − 1)(L + 1)) = I 2 (1) = ∅. Theorem 2 then gives
x + 2y ≤ 5
LIA
=
φ 1 ∨ φ 2
BV
which squares with Corollary 2.
87
Observe from Figure 2(c) that
0 ≤ x + 2y − 4 ≤ 1
LIA
=
0 ≤ x + 2y − 4 ≤ 1
BV
∩
box BV (1, 2; 5)
BV
and moreover 0 mod 8 = 0 ≤ (x + 2y − 4) mod 8 for all (x, y) ∈ M
2 thus
0 ≤ x + 2y − 4 ≤ 1
LIA
=
x + 2y − 4 ≤ 1 ∧ box BV (1, 2; 5)
BV
therefore cumulatively
x + 2y ≤ 5
LIA
=
ϕ 1 ∨ ϕ 2
BV
where
ϕ 1 = [x + 2y ≤ 3
∧ (x ≤ 3 ∧ y ≤ 1)]
ϕ 2 = [x + 2y − 4 ≤ 1 ∧ ((x ≤ 3 ∧ y ≤ 3) ∨ (x ≤ 7 ∧ y ≤ 1))]
The general rule of the separation of the given inequality and the boxing is
shown in this theorem:
Theorem 2 (boxing with gapping). Let c ∈ N
d and b ∈ N.
d
i=1 c i x i ≤ b
LIA
=
φ 0 ∨ φ 1 ∨ φ 2
BV
where S = b/(m/2) and
φ 0 ≡
d
i=1 c i x i − (S − 2)(m/2) ≤ m/2 − 1
∧ box BV (c; (S − 1)(m/2) − 1)
φ 1 ≡
d
i=1 c i x i − (S − 1)(m/2) ≤ m/2 − 1
∧ box BV (c; S(m/2) − 1)
φ 2 ≡
d
i=1 c i x i − S(m/2) ≤ b mod (m/2)
∧ box BV (c; b)
Corollary 2 (boxing and gapping with simplification). If b/(m/2) = 1
or b mod m = m/2 − 1 then
d
i=1 c i x i ≤ b
LIA
=
φ 1 ∨ φ 2
BV
.
Example 5. Let m = 8 and consider again x + 2y ≤ 5 so that c = 1, 2. Then
S = 5/4 = 1 and, applying corollary 2,
x + 2y ≤ 5
LIA
=
φ 1 ∨ φ 2
BV
where
φ 1 ≡ (x + 2y − 0 · 4 ≤ 4 − 1)
∧ box BV (c; 1 · 4 − 1) = ϕ 1
φ 2 ≡ (x + 2y − 1 · 4 ≤ 5 mod 4) ∧ box BV (c; 5)
= ϕ 2
aligning with the intuition given in example 4.
Example 6. Figure 3 illustrates Theorem 2 for 7x + 3y ≤ 17 and m = 8. Then
S = 17/(8/2) = 4 and
7x + 3y ≤ 17
LIA
=
φ 0 ∨ φ 1 ∨ φ 2
BV
where
φ 0 = 7x + 3y − 8 ≤ 3 ∧ box BV (c; 11)
φ 1 = 7x + 3y − 12 ≤ 3 ∧ box BV (c; 15)
φ 2 = 7x + 3y − 16 ≤ 1 ∧ box BV (c; 17)
The box BV (c; 11), box BV (c, 15), box BV (c; 17) formulae are again depicted in grey.
For example,
box BV (c; 11) = (x ≤ 0 ∧ y ≤ 3) ∨ (x ≤ 1 ∧ y ≤ 2) ∨ (x ≤ 1 ∧ y ≤ 1)
because d = 2, L = 3 and I 2 ((d−1)(L+1)) = {{1, 3, 2, 2, 3, 1}. From Figure 3
observe
7x + 3y ≤ 17
LIA
=
φ 0
BV
∪
φ 1
BV
∪
φ 2
BV
.
Example 7. Consider again example 5 where S = 1. Then φ 0 = false because
box BV (c; (S − 1)(m/2) − 1) = box BV (c; −1) = false. This is because L = 0
and I d ((d − 1)(L + 1)) = I 2 (1) = ∅. Theorem 2 then gives
x + 2y ≤ 5
LIA
=
φ 1 ∨ φ 2
BV
which squares with Corollary 2.