FCEIA - Escuela de Ciencias Exactas y Naturales
http://hdl.handle.net/2133/1815
Sun, 16 Jan 2022 20:34:03 GMT2022-01-16T20:34:03ZFormalization of the Domination Chain with Weighted Parameters
http://hdl.handle.net/2133/18978
Formalization of the Domination Chain with Weighted Parameters
The Cockayne-Hedetniemi Domination Chain is a chain of inequalities between classic parameters
of graph theory: for a given graph G, ir(G) ≤ γ(G) ≤ ι(G) ≤ α(G) ≤ Γ(G) ≤ IR(G). These
parameters return the maximum/minimum cardinality of a set satisfying some property. However,
they can be generalized for graphs with weighted vertices where the objective is to maximize/minimize
the sum of weights of a set satisfying the same property, and the domination chain still holds for them.
In this work, the definition of these parameters as well as the chain is formalized in Coq/Ssreflect.
Tue, 01 Jan 2019 00:00:00 GMThttp://hdl.handle.net/2133/189782019-01-01T00:00:00ZDomination Chain with Weighted Parameters (Coq files)
http://hdl.handle.net/2133/18977
Domination Chain with Weighted Parameters (Coq files)
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.; 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).
Thu, 14 Mar 2019 00:00:00 GMThttp://hdl.handle.net/2133/189772019-03-14T00:00:00ZAppendix and source code of ACP solver for the paper On the additive chromatic number of several families of graphs
http://hdl.handle.net/2133/18976
Appendix and source code of ACP solver for the paper On the additive chromatic number of several families of graphs
This folder contains a source code for solving the ADDITIVE COLORING PROBLEM as well as testing the ADDITIVE COLORING CONJECTURE. In addition, it contains the appendix of the paper "On the additive chromatic number of several families of graphs" with proofs of some propositions, the integer programming model and some computational experiments.; Steps to reproduce
The programs ACOPT, TEST and DSATUR should be compiled with Visual Studio 2013. The programs also require IBM ILOG CPLEX 12.6. Below, some examples are given. Testing the additive coloring conjecture on all graphs of 4 vertices: test.exe graphs4.all Recall that acopt.exe and dsatur.exe must be present in the same folder. Also, acopt must be compiled without "VERBOSE" definition (just comment that line in source code). Since "test" generates several files on-the-fly and makes heavy use of the hard disk, it is advisable to execute it on a RamDisk. Obtaining the additive chromatic number of a graph, e.g. the cycle sun with m = 10, and assuming an upper bound UB = 8: acopt.exe CS10.graph 8 If none upper bound is provided, it uses UB = Delta(G)^2-Delta(G)+1 by default (which is really bad!). A lower bound LB can also be provided together with UB. For example: acopt.exe KS10.graph 10 4 In particular, for obtaining an additive k-coloring for a specific k, use UB = LB = k. It is recommended to compile acopt with "VERBOSE" definition for viewing log and optimal solution.
Wed, 12 Feb 2020 00:00:00 GMThttp://hdl.handle.net/2133/189762020-02-12T00:00:00ZCross-identification of stellar catalogs with multiple stars: Complexity and Resolution
http://hdl.handle.net/2133/18963
Cross-identification of stellar catalogs with multiple stars: Complexity and Resolution
In this work, I present an optimization problem which consists of assigning entries
of a stellar catalog to multiple entries of another stellar catalog such that the probability
of such assignment is maximum. I show a way of modeling it as a Maximum
Weighted Stable Set Problem which is further used to solve a real astronomical
instance and I partially characterize the forbidden subgraphs of the resulting family
of graphs given by that reduction. Finally, I prove that the problem is NP-Hard.
Wed, 01 Aug 2018 00:00:00 GMThttp://hdl.handle.net/2133/189632018-08-01T00:00:00Z