Articles de revista
http://hdl.handle.net/2117/3517
2018-04-23T08:04:14ZAre crossing dependencies really scarce?
http://hdl.handle.net/2117/112359
Are crossing dependencies really scarce?
Ferrer Cancho, Ramon; Gómez Rodríguez, Carlos; Esteban Ángeles, Juan Luis
The syntactic structure of a sentence can be modelled as a tree, where vertices correspond to words and edges indicate syntactic dependencies. It has been claimed recurrently that the number of edge crossings in real sentences is small. However, a baseline or null hypothesis has been lacking. Here we quantify the amount of crossings of real sentences and compare it to the predictions of a series of baselines. We conclude that crossings are really scarce in real sentences. Their scarcity is unexpected by the hubiness of the trees. Indeed, real sentences are close to linear trees, where the potential number of crossings is maximized.
2017-12-21T13:26:22ZFerrer Cancho, RamonGómez Rodríguez, CarlosEsteban Ángeles, Juan LuisThe syntactic structure of a sentence can be modelled as a tree, where vertices correspond to words and edges indicate syntactic dependencies. It has been claimed recurrently that the number of edge crossings in real sentences is small. However, a baseline or null hypothesis has been lacking. Here we quantify the amount of crossings of real sentences and compare it to the predictions of a series of baselines. We conclude that crossings are really scarce in real sentences. Their scarcity is unexpected by the hubiness of the trees. Indeed, real sentences are close to linear trees, where the potential number of crossings is maximized.Subproblem ordering heuristics for AND/OR best-first search
http://hdl.handle.net/2117/111987
Subproblem ordering heuristics for AND/OR best-first search
Lam, William; Kask, Kalev; Larrosa Bondia, Francisco Javier; Dechter, Rina
Best-first search can be regarded as anytime scheme for producing lower bounds on the optimal solution, a characteristic that is mostly overlooked. We explore this topic in the context of AND/OR best-first search, guided by the MBE heuristic, when solving graphical models. In that context, the impact of the secondary heuristic for subproblem ordering may be significant, especially in the anytime context. Indeed, our paper illustrates this, showing that a new concept of bucket errors can advise in providing effective subproblem orderings in AND/OR search for both exact and anytime solutions.
2017-12-14T07:34:26ZLam, WilliamKask, KalevLarrosa Bondia, Francisco JavierDechter, RinaBest-first search can be regarded as anytime scheme for producing lower bounds on the optimal solution, a characteristic that is mostly overlooked. We explore this topic in the context of AND/OR best-first search, guided by the MBE heuristic, when solving graphical models. In that context, the impact of the secondary heuristic for subproblem ordering may be significant, especially in the anytime context. Indeed, our paper illustrates this, showing that a new concept of bucket errors can advise in providing effective subproblem orderings in AND/OR search for both exact and anytime solutions.Residual-guided look-ahead in AND/OR search for graphical models
http://hdl.handle.net/2117/111099
Residual-guided look-ahead in AND/OR search for graphical models
Lam, William; Kask, Kalev; Larrosa Bondia, Francisco Javier; Dechter, Rina
We introduce the concept of local bucket error for the mini-bucket heuristics and show how it can be used to improve the power of AND/OR search for combinatorial optimization tasks in graphical models (e.g. MAP/MPE or weighted CSPs). The local bucket error illuminates how the heuristic errors are distributed in the search space, guided by the mini-bucket heuristic. We present and analyze methods for compiling the local bucket-errors (exactly and approximately) and show that they can be used to yield an effective tool for balancing look-ahead overhead during search. This can be especially instrumental when memory is restricted, accommodating the generation of only weak compiled heuristics. We illustrate the impact of the proposed schemes in an extensive empirical evaluation for both finding exact solutions and anytime suboptimal solutions.
2017-11-23T07:31:29ZLam, WilliamKask, KalevLarrosa Bondia, Francisco JavierDechter, RinaWe introduce the concept of local bucket error for the mini-bucket heuristics and show how it can be used to improve the power of AND/OR search for combinatorial optimization tasks in graphical models (e.g. MAP/MPE or weighted CSPs). The local bucket error illuminates how the heuristic errors are distributed in the search space, guided by the mini-bucket heuristic. We present and analyze methods for compiling the local bucket-errors (exactly and approximately) and show that they can be used to yield an effective tool for balancing look-ahead overhead during search. This can be especially instrumental when memory is restricted, accommodating the generation of only weak compiled heuristics. We illustrate the impact of the proposed schemes in an extensive empirical evaluation for both finding exact solutions and anytime suboptimal solutions.Jutge.org: characteristics and experiences
http://hdl.handle.net/2117/110183
Jutge.org: characteristics and experiences
Petit Silvestre, Jordi; Roura Ferret, Salvador; Carmona Vargas, Josep; Cortadella Fortuny, Jordi; Duch Brown, Amalia; Giménez, Omer; Mani, Anaga; Mas Rovira, Jan; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto; San Pedro Martín, Javier de; Venkataramani, Divya
Jutge.org is an open educational online programming judge designed for students and instructors, featuring a repository of problems that is well organized by courses, topics and difficulty. Internally, Jutge.org uses a secure and efficient architecture and integrates modern verification techniques, formal methods, static code analysis and data mining. Jutge.org has exhaustively been used during the last decade at the Universitat Politecnica de Catalunya to strengthen the learn-by-doing approach in several courses. This paper presents the main characteristics of Jutge.org and shows its use and impact in a wide range of courses covering basic programming, data structures, algorithms, artificial intelligence, functional programming and circuit design.
2017-11-09T13:53:28ZPetit Silvestre, JordiRoura Ferret, SalvadorCarmona Vargas, JosepCortadella Fortuny, JordiDuch Brown, AmaliaGiménez, OmerMani, AnagaMas Rovira, JanRodríguez Carbonell, EnricRubio Gimeno, AlbertoSan Pedro Martín, Javier deVenkataramani, DivyaJutge.org is an open educational online programming judge designed for students and instructors, featuring a repository of problems that is well organized by courses, topics and difficulty. Internally, Jutge.org uses a secure and efficient architecture and integrates modern verification techniques, formal methods, static code analysis and data mining. Jutge.org has exhaustively been used during the last decade at the Universitat Politecnica de Catalunya to strengthen the learn-by-doing approach in several courses. This paper presents the main characteristics of Jutge.org and shows its use and impact in a wide range of courses covering basic programming, data structures, algorithms, artificial intelligence, functional programming and circuit design.A correction on Shiloach's algorithm for minimum linear arrangement of trees
http://hdl.handle.net/2117/106035
A correction on Shiloach's algorithm for minimum linear arrangement of trees
Esteban Ángeles, Juan Luis; Ferrer Cancho, Ramon
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 subsequent literature. We also improve some aspects of the notation.
2017-06-30T11:25:05ZEsteban Ángeles, Juan LuisFerrer Cancho, RamonMore 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 subsequent literature. We also improve some aspects of the notation.Improving IntSat by expressing disjunctions of bounds as linear constraints
http://hdl.handle.net/2117/103144
Improving IntSat by expressing disjunctions of bounds as linear constraints
Asín Acha, Roberto Javier; Aloysius Bezem, Marcus; Nieuwenhuis, Robert Lukas Mario
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 no strong enough ILP constraint, and the backjump has to be done based on the conflicting set of bounds. The techniques given in this article precisely analyze how and when that set can be translated into the required new ILP constraint. Moreover, this can be done efficiently. This obviously strengthens learning and significantly improves the performance of IntSat (as confirmed by our experiments). We also briefly discuss extensions and other applications.
2017-03-31T10:33:34ZAsín Acha, Roberto JavierAloysius Bezem, MarcusNieuwenhuis, Robert Lukas MarioConflict-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 no strong enough ILP constraint, and the backjump has to be done based on the conflicting set of bounds. The techniques given in this article precisely analyze how and when that set can be translated into the required new ILP constraint. Moreover, this can be done efficiently. This obviously strengthens learning and significantly improves the performance of IntSat (as confirmed by our experiments). We also briefly discuss extensions and other applications.Quasipolynomial size frege proofs of Frankl's Theorem on the trace of sets
http://hdl.handle.net/2117/100899
Quasipolynomial size frege proofs of Frankl's Theorem on the trace of sets
Aisenberg, James; Bonet Carbonell, M. Luisa; Buss, Sam
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 values of the parameter t, we prove that Frankl's Theorem has polynomial size AC(0)-Frege proofs from instances of the pigeonhole principle.
2017-02-13T11:15:11ZAisenberg, JamesBonet Carbonell, M. LuisaBuss, SamWe 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 values of the parameter t, we prove that Frankl's Theorem has polynomial size AC(0)-Frege proofs from instances of the pigeonhole principle.The scaling of the minimum sum of edge lengths in uniformly random trees
http://hdl.handle.net/2117/88535
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
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 trees in polynomial time, they have remained theoretical and have not been implemented in practical contexts to our knowledge. Here we use one of those algorithms to investigate the growth of this sum as a function of the size of the tree in uniformly random trees. We show that this sum is bounded above by its value in a star tree. We also show that the mean edge length grows logarithmically in optimal linear arrangements, in stark contrast to the linear growth that is expected on optimal arrangements of star trees or on random linear arrangements.
2016-07-06T09:32:34ZEsteban Ángeles, Juan LuisFerrer Cancho, RamonGómez Rodríguez, CarlosThe 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 trees in polynomial time, they have remained theoretical and have not been implemented in practical contexts to our knowledge. Here we use one of those algorithms to investigate the growth of this sum as a function of the size of the tree in uniformly random trees. We show that this sum is bounded above by its value in a star tree. We also show that the mean edge length grows logarithmically in optimal linear arrangements, in stark contrast to the linear growth that is expected on optimal arrangements of star trees or on random linear arrangements.The computability path ordering
http://hdl.handle.net/2117/85100
The computability path ordering
Blanqui, Frédéric; Jouannaud, Jean Pierre; Rubio Gimeno, Alberto
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 on terms obtained by lifting a precedence on function symbols. A first version, core CPO, is essentially obtained from the higher-order recursive path ordering (HORPO) by eliminating type checks from some recursive calls and by incorporating the treatment of bound variables as in the com-putability closure. The well-foundedness proof shows that core CPO captures the essence of computability arguments ^#224, la Tait and Girard, therefore explaining its name. We further show that no further type check can be eliminated from its recursive calls without loosing well-foundedness, but for one for which we found no counterexample yet. Two extensions of core CPO are then introduced which allow one to consider: the first, higher-order inductive types; the second, a precedence in which some function symbols are smaller than application and abstraction.
2016-04-04T09:50:47ZBlanqui, FrédéricJouannaud, Jean PierreRubio Gimeno, AlbertoThis 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 on terms obtained by lifting a precedence on function symbols. A first version, core CPO, is essentially obtained from the higher-order recursive path ordering (HORPO) by eliminating type checks from some recursive calls and by incorporating the treatment of bound variables as in the com-putability closure. The well-foundedness proof shows that core CPO captures the essence of computability arguments ^#224, la Tait and Girard, therefore explaining its name. We further show that no further type check can be eliminated from its recursive calls without loosing well-foundedness, but for one for which we found no counterexample yet. Two extensions of core CPO are then introduced which allow one to consider: the first, higher-order inductive types; the second, a precedence in which some function symbols are smaller than application and abstraction.Normal higher-order termination
http://hdl.handle.net/2117/79284
Normal higher-order termination
Jouannaud, Jean Pierre; Rubio Gimeno, Alberto
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 Church's simply typed λ-calculus and, on the other hand, any use of eta, as a reduction, as an expansion, or as an equation. The user's rules may be of any type in this type system, either a base, functional, or weakly polymorphic type.
2015-11-16T09:58:07ZJouannaud, Jean PierreRubio Gimeno, AlbertoWe 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 Church's simply typed λ-calculus and, on the other hand, any use of eta, as a reduction, as an expansion, or as an equation. The user's rules may be of any type in this type system, either a base, functional, or weakly polymorphic type.