82
T. Okudono and A. King
(a) x + y ≤ 3
(b) x + y ≤ 3 with box
(c) x + y ≤ 7
(d) x + y − 4 ≤ 3 (e) x + y − 4 ≤ 3 with box 1 (f) x + y − 4 ≤ 3 with box 2
Fig. 1. Gapping and boxing for x + y ≤ 3 and x + y ≤ 7
techniques, boxing and gapping, and demonstrate how they are used together to
construct such an f ; the sequel provides a more formal development.
To illustrate boxing and gapping, first consider the set of solutions to the
inequality x + y ≤ 3, when interpreted with both the LIA semantics and BV
semantics. Figure 1(a) gives the LIA solutions in blue and the BV solutions
in red over the non-negative integer grid {(x, y) | 0 ≤ x < 8 ∧ 0 ≤ y < 8}
using a modulo of 8 for bit-vectors. The solution sets differ on, for instance,
(5, 6) since (5 + 6) (mod 8) = 3 ≤ 3 but 5 + 6 = 11 ≤ 3. It does not generally
follow that
f
LIA
⊆
f
BV
as Figure 1(d) illustrates for f = x + y − 4 ≤ 3. Then
(1, 2) ∈
x + y − 4 ≤ 3
LIA
since 1+2−4 = −1 ≤ 3 but (1, 2) ∈
x + y − 4 ≤ 3
BV
since (1 + 2 − 4) (mod 8) = 7 ≤ 3.
Enumeration A naive approach to finding a formula f such that
f
BV
=
LIA
is to enumerate all solutions of
LIA
to then summarise them in a single BV
formula. Figure 1(a) illustrates the 4 + 3 + 2 + 1 = 10 LIA solutions for =
(x + y ≤ 3) which are summarised in the following BV formula:
f 1 = (x = 0 ∧ y = 0) ∨ . . . ∨ (x = 0 ∧ y = 3) ∨ . . . ∨ (x = 3 ∧ y = 0)
This formula has 9 binary disjuncts and 10 binary conjuncts, hence 19 logical
connectives in total. A more compact formulation is to cover the blue triangular
region of Figure 1(a) with columns as realised with the following BV formula:
f 2 = (x = 0 ∧ y ≤ 3) ∨ . . . ∨ (x = 3 ∧ y ≤ 0)
Only non-negative solutions on the grid are considered so there is no need to
additionally assert 0 ≤ y. This formula has 3 binary disjuncts and 4 binary
conjuncts giving and 7 connectives in total.