Enviaments recents

  • A correction on Shiloach's algorithm for minimum linear arrangement of trees 

    Esteban Ángeles, Juan Luis; Ferrer Cancho, Ramon (2017-06-29)
    Article
    Accés obert
    More than 30 years ago, Shiloach published an algorithm to solve the minimum linear arrangement problem for undirected trees. Here we fix a small error in the original version of the algorithm and discuss its effect on ...
  • Improving IntSat by expressing disjunctions of bounds as linear constraints 

    Asín Acha, Roberto Javier; Aloysius Bezem, Marcus; Nieuwenhuis, Robert Lukas Mario (2016)
    Article
    Accés restringit per política de l'editorial
    Conflict-Driven Clause Learning (CDCL) SAT solvers can automatically solve very large real-world problems. IntSat is a new technique extending CDCL to Integer Linear Programming (ILP). For some conflicts, IntSat generates ...
  • Quasipolynomial size frege proofs of Frankl's Theorem on the trace of sets 

    Aisenberg, James; Bonet Carbonell, M. Luisa; Buss, Sam (2016-06-01)
    Article
    Accés obert
    We extend results of Bonet, Buss and Pitassi on Bondy's Theorem and of Nozaki, Arai and Arai on Bollobas' Theorem by proving that Frankl's Theorem on the trace of sets has quasipolynomial size Frege proofs. For constant ...
  • The scaling of the minimum sum of edge lengths in uniformly random trees 

    Esteban Ángeles, Juan Luis; Ferrer Cancho, Ramon; Gómez Rodríguez, Carlos (Institute of Physics (IOP), 2016-06-21)
    Article
    Accés obert
    The minimum linear arrangement problem on a network consists of finding the minimum sum of edge lengths that can be achieved when the vertices are arranged linearly. Although there are algorithms to solve this problem on ...
  • The computability path ordering 

    Blanqui, Frédéric; Jouannaud, Jean Pierre; Rubio Gimeno, Alberto (2015-10-26)
    Article
    Accés obert
    This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability path ordering (CPO), a recursive relation ...
  • Normal higher-order termination 

    Jouannaud, Jean Pierre; Rubio Gimeno, Alberto (2015-03-01)
    Article
    Accés obert
    We extend the termination proof methods based on reduction orderings to higher-order rewriting systems based on higher-order pattern matching. We accommodate, on the one hand, a weakly polymorphic, algebraic extension of ...
  • Efficiently calculating evolutionary tree measures using SAT 

    Bonet Carbonell, M. Luisa; John, Katherine St. (2009)
    Article
    Accés obert
    We develop techniques to calculate important measures in evolutionary biology by encoding to CNF formulas and using powerful SAT solvers. Comparing evolutionary trees is a necessary step in tree reconstruction algorithms, ...
  • Mining frequent closed rooted trees 

    Balcázar Navarro, José Luis; Bifet Figuerol, Albert Carles; Lozano Bojados, Antoni (2010-01)
    Article
    Accés obert
    Many knowledge representation mechanisms are based on tree-like structures, thus symbolizing the fact that certain pieces of information are related in one sense or another. There exists a well-studied process of closure-based ...

Mostra'n més