ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals
http://hdl.handle.net/2117/3092
2015-07-29T06:58:20ZThe ordering principle in a fragment of approximate counting
http://hdl.handle.net/2117/28288
The ordering principle in a fragment of approximate counting
Atserias Peri, Albert; Thapen, Neil
The ordering principle states that every finite linear order has a least element. We show that, in the relativized setting, the surjective weak pigeonhole principle for polynomial time functions does not prove a Herbrandized version of the ordering principle over T-2(1). This answers an open question raised in Buss et al. [2012] and completes their program to compare the strength of Jerabek's bounded arithmetic theory for approximate counting with weakened versions of it.
2014-01-01T00:00:00ZProcess discovery algorithms using numerical abstract domains
http://hdl.handle.net/2117/28272
Process discovery algorithms using numerical abstract domains
Carmona Vargas, Josep; Cortadella Fortuny, Jordi
The discovery of process models from event logs has emerged as one of the crucial problems for enabling the continuous support in the life-cycle of an information system. However, in a decade of process discovery research, the algorithms and tools that have appeared are known to have strong limitations in several dimensions. The size of the logs and the formal properties of the model discovered are the two main challenges nowadays. In this paper we propose the use of numerical abstract domains for tackling these two problems, for the particular case of the discovery of Petri nets. First, numerical abstract domains enable the discovery of general process models, requiring no knowledge (e.g., the bound of the Petri net to derive) for the discovery algorithm. Second, by using divide and conquer techniques we are able to control the size of the process discovery problems. The methods proposed in this paper have been implemented in a prototype tool and experiments are reported illustrating the significance of this fresh view of the process discovery problem.
2014-12-01T00:00:00ZBetter feedback for educational online judges
http://hdl.handle.net/2117/28174
Better feedback for educational online judges
Mani, Anaga; Venkataramani, Divya; Petit Silvestre, Jordi; Roura Ferret, Salvador
The verdicts of most online programming judges are, essentially, binary: the submitted codes are either “good enough” or not. Whilst this policy is appropriate for competitive or recruitment platforms, it can hinder the adoption of online judges on educative settings, where it could be adequate to provide better feedback to a student (or instructor) that has submitted a wrong code. An obvious option would be to just show him or her an instance where the code fails. However, that particular instance could be not very significant, and so could induce unreflectively patching the code. The approach considered in this paper is to data mine all the past incorrect submissions by all the users of the judge, so to extract a small subset of private test cases that may be relevant to most future users. Our solution is based on parsing the test files, building a bipartite graph, and solving a Set Cover problem by means of Integer Linear Programming. We have tested our solution with a hundred problems in Jutge.org. Those experiments suggest that our approach is general, efficient, and provides high quality results.
2014-01-01T00:00:00ZFirefighting as a game
http://hdl.handle.net/2117/28172
Firefighting as a game
Álvarez Faura, M. del Carme; Blesa Aguilera, Maria Josep; Molter, Hendrik
The Firefighter Problem was proposed in 1995 [16] as a deterministic discrete-time model for the spread (and containment) of a fire. Its applications reach from real fires to the spreading of diseases and the containment of floods. Furthermore, it can be used to model the spread of computer viruses or viral marketing in communication networks.
In this work, we study the problem from a game-theoretical perspective. Such a context seems very appropriate when applied to large networks, where entities may act and make decisions based on their own interests, without global coordination.
We model the Firefighter Problem as a strategic game where there is one player for each time step who decides where to place the firefighters. We show that the Price of Anarchy is linear in the general case, but at most 2 for trees. We prove that the quality of the equilibria improves when allowing coalitional cooperation among players. In general, we have that the Price of Anarchy is in T(n/k) where k is the coalition size. Furthermore, we show that there are topologies which have a constant Price of Anarchy even when constant sized coalitions are considered.
2014-12-10T00:00:00ZLower bounds for DNF-refutations of a relativized weak pigeonhole principle
http://hdl.handle.net/2117/28085
Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
Atserias Peri, Albert; Müller, Moritz; Oliva Valls, Sergi
The relativized weak pigeonhole principle states that if at least 2n out of n(2) pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNF-refutation of the CNF encoding of this principle requires size 2((log n)3/2-is an element of) for every is an element of > 0 and every sufficiently large n. By reducing it to the standard weak pigeonhole principle with 2n pigeons and n holes, we also show that this lower bound is essentially tight in that there exist DNF-refutations of size 2((log n)O(1)) even in R(log). For the lower bound proof we need to discuss the existence of unbalanced low-degree bipartite expanders satisfying a certain robustness condition.
2015-06-01T00:00:00ZTableau-based reasoning for graph properties
http://hdl.handle.net/2117/28034
Tableau-based reasoning for graph properties
Lambers, Leen; Orejas Valdés, Fernando
Graphs are ubiquitous in Computer Science. For this reason, in many areas, it is very important to have the means to express and reason about graph properties. A simple way is based on defining an appropriate encoding of graphs in terms of classical logic. This approach has been followed by Courcelle. The alternative is the definition of a specialized logic, as done by Habel and Pennemann, who defined a logic of nested graph conditions, where graph properties are formulated explicitly making use of graphs and graph morphisms, and which has the expressive power of Courcelle's first order logic of graphs. In particular, in his thesis, Pennemann defined and implemented a sound proof system for reasoning in this logic. Moreover, he showed that his tools outperform some standard provers when working over encoded graph conditions. Unfortunately, Pennemann did not prove the completeness of his proof system. In this sense, one of the main contributions of this paper is the solution to this open problem. In particular, we prove the (refutational) completeness of a tableau method based on Pennemann's rules that provides a specific theorem-proving procedure for this logic. This procedure can be considered our second contribution. Finally, our tableaux are not standard, but we had to define a new notion of nested tableaux that could be useful for other formalisms where formulas have a hierarchical structure like nested graph conditions.
2014-01-01T00:00:00ZAdaptive clock with useful jitter
http://hdl.handle.net/2117/27967
Adaptive clock with useful jitter
Cortadella Fortuny, Jordi; Lavagno, Luciano; López Muñoz, Pedro; Lupon Navazo, Marc; Moreno Vega, Alberto; Roca Pérez, Antoni; Sapatnekar, Sachin S.
The growing variability in nanoelectronic devices due to uncertainties from the manufacturing process and environmental conditions (power supply, temperature, aging) requires increasing design guardbands, forcing circuits to work with conservative clock frequencies. Various schemes for clock generation based on ring oscillators have been proposed with the goal to mitigate the power and performance losses
attributable to variability. However, there has been no systematic analysis to quantify the benefits of such schemes.This paper presents and analyzes an Adaptive Clocking scheme with
Useful Jitter (ACUJ) that uses variability as an opportunity to reduce power by adapting the clock frequency to the varying environmental conditions and, thus, reducing guardband margins significantly. Power can be reduced between 20% and 40% at iso-performance and performance can be boosted by similar amounts at iso-power. Additionally, energy savings can be translated to substantial advantages in terms of reliability and thermal management. More importantly, the technology can be adopted with minimal modifications to conventional EDA flows.
Report - Departament Ciències de la Computació
2015-05-19T00:00:00ZOn the complexity of exchanging
http://hdl.handle.net/2117/27400
On the complexity of exchanging
Molinero Albareda, Xavier; Olsen, Martin; Serna Iglesias, María José
We analyze the computational complexity of the problem of deciding
whether, for a given simple game, there exists the possibility of rearranging the participants in a set of j given losing coalitions into a set of j winning coalitions. We also look at the problem of turning winning coalitions into losing coalitions. We analyze the problem when the simple game is represented by a list of wining, losing, minimal winning or maximal loosing coalitions.
2015-03-24T00:00:00ZBounded-width QBF is PSPACE-complete
http://hdl.handle.net/2117/27300
Bounded-width QBF is PSPACE-complete
Atserias Peri, Albert; Oliva Valls, Sergi
Tree-width and path-width are two well-studied parameters of structures that measure their similarity to a tree and a path, respectively. We show that QBF on instances with constant path-width, and hence constant tree-width, remains PSPACE-complete. This answers a question by Vardi. We also show that on instances with constant path-width and a very slow-growing number of quantifier alternations (roughly inverse-Ackermann many in the number of variables), the problem remains NP-hard. Additionally, we introduce a family of formulas with bounded tree-width that do have short refutations in Q-resolution, the natural generalization of resolution for quantified Boolean formulas.
2014-11-01T00:00:00ZA boolean rule-based approach for manufacturability-aware cell routing
http://hdl.handle.net/2117/27267
A boolean rule-based approach for manufacturability-aware cell routing
Cortadella Fortuny, Jordi; Petit Silvestre, Jordi; Gómez Fernández, Sergio; Moll Echeto, Francisco de Borja
An approach for cell routing using gridded design rules is proposed. It is technology-independent and parameterizable for different fabrics and design rules, including support for multiple-patterning lithography. The core contribution is a detailed-routing algorithm based on a Boolean formulation of the problem. The algorithm uses a novel encoding scheme, graph theory to support floating terminals, efficient heuristics to reduce the computational cost, and minimization of the number of unconnected pins in case the cell is unroutable. The versatility of the algorithm is demonstrated by routing single-and double-height cells. The efficiency is ascertained by synthesizing a library with 127 cells in about one hour and a half of CPU time. The layouts derived by the implemented tool have also been compared with the ones from a commercial library; thus, showing the competitiveness of the approach for gridded geometries.
2014-03-01T00:00:00Z