diff options
Diffstat (limited to 'contrib/graphs')
-rw-r--r-- | contrib/graphs/README | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/contrib/graphs/README b/contrib/graphs/README new file mode 100644 index 000000000..dd342607a --- /dev/null +++ b/contrib/graphs/README @@ -0,0 +1,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 |