
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.

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

The browsable version of DomTheory is in the directory "html". Open the file "toc.html".

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).

For any questions about these files, please contact me at daniel@fceia.unr.edu.ar

Enjoy them! :)
Daniel.-

