88
T. Okudono and A. King
Fig. 3. Gapping and boxing for 7x + 3y ≤ 17 where c = 7, 3, m = 8 and S = 4
3.3 Boxing, Gapping and Flipping
To handle inequalities which have indeterminates with negative coefficients, boxing and gapping are augmented with a third technique, which we have informally
named flipping. Flipping transforms an inequality into a syntactic form which
is amenable to boxing and gapping by reflecting the solutions of the inequality. To detail the transformation, we assume without loss of generality, that an
inequality takes the syntactic form c
+
· x
+ + c
−
· x
−
≤ b where c
+ > 0 and
c
− < 0. Hence x = x
+
◦ x
− where ◦ denotes vector concatenation. The act of
flipping reflects the solutions of the inequality simultaneously around the axes
x
−
1 = 0, . . . , x
−
e = 0 where x
− = x
−
1 , . . . , x
−
e and e is the dimension of x
− .
The development starts with the flipping transformation itself:
Definition 3. Given e ∈ {1, . . . , d}, then the (semantic) flipping function F e :
M
d
→ M
d is defined:
F e (x
+
1 , . . . , x
+
d−e , x
−
1 , . . . , x
−
e ) = x
+
1 , . . . , x
+
d−e , m − 1 − x
−
1 , . . . , m − 1 − x
−
e .
Given an inequality with negative coefficients, we derive a new inequality whose
solutions coincide with the flipped solutions of the given inequality. This transformation is then lifted to formulae as follows:
Definition 4. Given a partition of x into the sub-vectors x
+ = x
+
1 , . . . , x
+
d−e
and x
− = x
−
1 , . . . , x
−
e , then the (syntactic) flipping function F x − is defined:
F x − (c
+
· x
+ + c
−
· x
−
≤ b) = c
+
· x
+
− c
−
· x
− + (m − 1)(c
−
· 1) ≤ b
F x − (f 1 ∨ f 2 ) = F x − (f 1 ) ∨ F x − (f 2 )
F x − (f 1 ∧ f 2 ) = F x − (f 1 ) ∧ F x − (f 2 )
F x − (¬f ) = ¬F x − (f )
(a) 7x + 3y ≤ 17
(b) φ 0 = 7x + 3y − 8 ≤ 3 ∧ box BV (c; 11)
(c) φ 1 = 7x + 3y − 12 ≤ 3 ∧ box BV (c; 15) (d) φ 2 = 7x + 3y − 16 ≤ 1 ∧ box BV (c; 17)