Formalization of aspects of the Maximum Weighted Irredundant Set (MWIS) problem

This repository contains some code concerning the formalization in Coq/Ssreflect of some results on the MWIS problem and a heuristic implemented in C++ that computes a solution and a dual bound for this problem.

Our goal is to explore two ideas related to formalizing results of graph theory: our first proposal is that some long proofs, involving a large number of cases that can be checked mechanically, can be channeled through a proof assistant; the other is to analyze the possibility of generating a Coq file that certifies a numerical value for a given graph parameter.

An additional feature of the algorithm that finds a solution of the MWIS problem is that it generates a Coq file with the instance and the proposed solution.

Files and folders 🔧

• mwis: The formalized theory.

  • mwis/check_ir.v: Some tools to check irredundancy, cardinality and weights of given graphs and sets.
  • mwis/prelim.v: Some preliminary results.
  • mwis/mwis.v: Main components of the theory.
  • mwis/mwis_prop.v: The huge proofs involving claw-free and copaw-free graphs.

• solver: A heuristic for solving the MWIS problem. This code is able to generate a Coq certificate of a lower bound of IR_w(G). Use "make" inside this folder to compile it and generate all instances.

• instances: A testbed of 26 (unweighted) instances with up to 100 vertices from the DIMACS challenge, and an instance of 48 vertices with weights corresponding to a service allocation problem of the city of Buenos Aires.

• certs: Coq certificates of the instances. Use "make easy" or "make hard" to check the easy or hard instances resp., or "make weighted" to check the weighted instance.

The remaining files correspond to a version of Coq graph-theory (0.8) with Domination Theory. You can find the README of this package below.

Requirements 📋

MWIS formalization requires the dependencies of package graph-theory 0.8: Coq 8.11+, MathComp 1.10+, finmap, hierarchy builder 0.10. Certificate verification requires previously compiling the MWIS formalization.

In our case, the following versions downloaded with OPAM tool works:

• coq 8.13.1
• coq-mathcomp-ssreflect 1.12.0
• coq-hierarchy-builder 1.0.0
• coq-mathcomp-finmap 1.5.1

For compiling the solver, we used GCC 9.4.0 (but any reasonable version should work as well).

You can follow these steps:

• Compile graph-theory and MWIS Coq files: just "make" in the root folder
• (Optional) Compile solver and generate certificates: "make" in the solver folder
• Check certificates: "make" in the certs folder

Authors and contact information ✒️

• Ricardo Katz (@rdkatz), mail: [email protected]
• Daniel Severín (@aureus123), mail: [email protected]

Original README of graph-theory package

A library of formalized graph theory results, including various standard results from the literature (e.g., Menger’s Theorem, Hall’s Marriage Theorem, and the excluded minor characterization of treewidth-two graphs) as well as some more recent results arising from the study of relation algebra within the ERC CoVeCe project (e.g., soundness and completeness of an axiomatization of graph isomorphism).

Meta

• Author(s):
  • Christian Doczkal (initial)
  • Damien Pous (initial)
  • Daniel Severín (external contributor)
• Coq-community maintainer(s):
  • Christian Doczkal (@chdoc)
  • Damien Pous (@damien-pous)
• License: CeCILL-B
• Compatible Coq versions: 8.11 or later
• Additional dependencies:
  • MathComp's SSReflect library, version 1.10 or later
  • MathComp's finmap library
  • Hierarchy Builder
• Coq namespace: GraphTheory
• Related publication(s):
  • Graph Theory in Coq - Minors, Treewidth, and Isomorphisms doi:10.1007/s10817-020-09543-2
  • Completeness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq doi:10.1145/3372885.3373831
  • A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs doi:10.1007/978-3-319-94821-8_11
  • Formalization of the Domination Chain with Weighted Parameters (Short Paper) doi:10.4230/LIPIcs.ITP.2019.36

Building and installation instructions

The easiest way to install the latest released version of Graph Theory is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-graph-theory

To instead build and install manually, do:

git clone https://github.com/coq-community/graph-theory.git
cd graph-theory
make   # or make -j <number-of-cores-on-your-machine> 
make install

Additional Documentation

Documentation describing the contents of the individual files is available on the project website