- We start with
(N, +). - However, see that in the first order theory, we can talk about e.g.
x > y as ∃z, x + z + 1 = y. - so, we need to add this
> symbol into the theory when we try to do QE. - Furthermore, we also add in
0, 1. - Finally, we add in the divisibility predicate, where
Dn(x) is true iff n divides x.
§ Do we really need to add the divisiblity predicate? Can't we get it from the other ones?
- Answer: yes we do!
- Key idea: the other predicates, of equality and disequality, give, for any variable
x, either a finite set of solutions or a cofinite set of solutions (complement is fiinite). - However, divisibility by
2 is neither finite nor cofinite! Thus, it is an extra predicate we need to add into the theory to make it work :)
§ Keeping Only Positive Predicates
- In this theory, we can always convert negations of predicates into a disjunct of purely positive predicates:
-
x != y becomes x < y \/ x > y. -
!D3(x) becomes D3(x + 1) \/ D3(x + 2), which is pretty interesting: we are writing x != 0 (mod 3) as (x = 1 (mod 3)) \/ (x = 2 (mod 3)). - Finally, we can write
!(x < y) as x = y \/ x > y.
§ General Enough Specific Example
∃ x: 2x + 3y < 4z /\ x + z < 2y + 3 /\ 2z + 4 < 5x + y /\ D2 (3x + 2y + 1) /\ D3 (5x + z)
- From this, we want to extract out a finite list of candidates for
x. - So, we create a disjunction where we convert the
∃ x into (x = v1 /\ P) \/ (x = v2 /\ P) ... \/ (x = vN /\ P). - First, we normalize the inequalities to make the coefficient of
x to be 30. - For
f < g, we can simply rescale as kf < kg. - For divisibility, we can write
n | x as kn | kx, or in our notation, Dn(x) becomes Dkn(kx).
∃ x,30x + 45y < 60z30x + 30z < 60y + 90z12z + 24 < 30x + 6yD20 (30x + 20y + 10)D18 (30x + 6z)
- Next, we want to say that there exists an
x that is divisible by 30, instead of having 30x. - This now becomes:
∃ x,x + 45y < 60zx + 30z < 60y + 90z12z + 24 < x + 6yD20 (x + 20y + 10)D18 (x + 6z)D30(x) # NEW
- We now get lower and upper bounds on
x, and we get divisbility constraints. - The inequality
12z + 24 < x + 6y gives a lower bound: 12z + 24 - 6y < x. - the other two inequalities give an upper bound:
x < 60z - 45y and x < 60y + 90z - 30z. - We can't directly enumerate this list, since the list's length is symbolic (depends on values of
y and z). - Finally, for the divisibility, we want numbers with these particular remainders.
- The chinese remainder theorem will tell us that such a number will occur in a consecutive set of
lcm(20, 18, 30) numbers! - Finally, what do we do with the minus sign?
- We can always change the minus to a plus, in an inequality:
-y < 0 if y > 0. - For divisibility, to check
D18(12x + 24 -6y + 7 + 6z), we write it as (18 - 6) y, i.e. 12y.
§ Other Considerations
- If we have multiple lower bounds, then we make the search from all lower bounds.
- If we no lower bounds, we start from zero.
- If we have no divisibility constraint, then we can do fourier motzkin? [Question: Why can't I think of it as modulo by zero? Aha, I can, but the LCM will be infinity ]
§ References