1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
Satisfiability of inequality constraints and detection of cycles with
negative weight in graphs
Author: Jean Goubault
Institution: G.I.E. Dyade, Inria Rocquencourt
Description:
It has been well-known since Bellman [1957] that deciding the
satisfiability over the set Z of integers of collections K of
inequalities of the form x<=y+c, where x, y are variables and c is a
constant of Z, can be done in polynomial time.
This holds even if we relax the form of our inequalities to be
x<=c or x>=c. The idea is to build a directed graph whose vertices
are the variables (and a special vertex for 0), and whose edges are
inequalities: the inequality x<=y+c is coded as an edge from x to y,
with weight c. Now the set K of inequality constraints is satisfiable
if and only if the constructed graph has no cycle of negative weight,
where the weight of a path is defined as the sum of the weights of its
edges.
The aim of this contribution is, first, to reprove these
results in Coq, and second, to build the decision procedure itself as
a Coq term. This allows us (in principle) to construct a reflection
tactic deciding these kinds of sets K. The reflection tactic itself
has not been written, but all contributions are welcome.
These results are established in the general case where, instead of Z,
we consider any totally ordered group. A tableau procedure, coded as a Coq
term, is provided to decide any positive combination of inequalities of
the form above (positive meaning: using only conjunction and disjunction).
When the totally ordered group has a 1, i.e., when it has a minimal strictly
positive element, then we extend this tableau procedure to the case of
general quantifier-free formulae built on inequations of the form above.
This is specialized in zgraph.v to the case of Z.
Keywords: graphs, cycles, paths, constraints, inequalities, reflection
|
