Domination Chain with Weighted Parameters (Coq files)
Description
This code contains a formal description of basic facts about Graph Theory and Domination Theory in the language Coq/Ssreflect. It is called DomTheory and consists of: *) The proof that the sum of degrees equals the cardinal of the edge set. *) Definitions and results about open and closed neighborhoods, stable sets, dominating sets, irredundant sets, hereditary and superhereditary properties, maximal/minimal sets and sets of maximum/minimum weight. *) The (weighted version of the) Cockayne-Hedetniemi domination chain. *) Examples of proofs with domination parameters on complete graphs. This code also contains: *) A browsable version made with the tool CoqDocJS, with some ''pretty-print'' symbols (like empty set, summation and set comprehension) added later. *) A solver that computes the (unweighted and weighted versions of) parameters gamma, ii, alpha, Gamma and IR. *) (experimental) The solver also generates a Coq file with a proof of alpha(G) >= k, where k is the size of the best stable set found during the optimization. *) A set of instances.
Files
Steps to reproduce
Requirements for parsing Coq files: *) Coq 8.6 or higher http://coq.inria.fr/coq-86 *) MathComp library 1.6.1 or higher https://github.com/math-comp/math-comp/releases/tag/mathcomp-1.6.1 Both can be installed in Ubuntu 18.04 with the command "apt-get install coq libssreflect-coq" Requirements for compiling the solver: *) GCC or Visual Studio 2013 *) IBM ILOG CPLEX 12.7 https://developer.ibm.com/docloud/blog/2016/11/24/cos-12-7-ai To compile DomTheory, just execute "make". To compile the solver, go to directory "solver" and execute "make". Additionaly, Coq files can be generated from the instances with the command "make coqinstances". Examples where Gamma(G) differs from IR(G), and Gamma_w(C5) differs from IR_w(C5) with specific weights can be checked with "make examples". Here, the graph C5 is the circuit of 5 vertices and G is the one proposed by Jacobson and Peters (see Figure 8(b) from http://doi.org/10.1016/0012-365X(90)90349-M). To test the Coq files generated by the solver, go to directory "instances" and execute "make" (it requires to compile DomTheory). Command-line arguments for the solver: ./solver option file.graph [file.weights] See solver.cpp for the format of the graph or weight files. If the weight file is not given, weights are set to 1 by default. Options are: 1 - compute gamma(G) 2 - compute ii(G) 3 - compute alpha(G) 4 - compute Gamma(G) 5 - compute IR(G) 6 - compute alpha(G) and generate Coq file For example: ./solve 6 petersen.graph Computes alpha(G) where G is the Petersen graph, and generates a file cert.v with the proof of alpha(G) >= 4. ./solve 4 C5.graph C5.weight Computes Gamma(C5) with the vector of weights (2, 2, 1, 1, 1).