ALBCOM - Algorismia, Bioinformàtica, Complexitat i Mètodes Formals

 

El grup de recerca ALBCOM uneix 19 reconeguts investigadors en mètodes formals; disseny, automatització i verificació de VLSI; algorismes i complexitat; bioinformàtica (vegeu http://albcom.cs.upc.edu/ per a més detalls). La recerca que es realitza a ALBCOM té un important prestigi en la comunitat científica internacional, degut a la qualitat de la seva recerca, tal com mostren les seves publicacions, i a l'activitat en projectes de recerca i de transferència de tecnologia amb empreses i institucions del sector.

El grupo de investigación ALBCOM une 19 reconocidos investigadores en métodos formales; diseño, automatización y verificación de VLSI; algoritmos y complejidad; bioinformática (véase http://albcom.cs.upc.edu/ para más detalles). La investigación que se realiza a ALBCOM tiene un importante prestigio en la comunidad científica internacional, debido a la calidad de su investigación, tal como muestran sus publicaciones, y a la actividad en proyectos de investigación y de transferencia de tecnología con empresas e instituciones del sector.

The primary goal is to produce relevant contributions in the areas of expertise of the group and to disseminate them in renowned international journals and conferences. It is the group's aim that these contributions have a tangible and long-term impact on the scientific community. Technology transfer is considered a byproduct of research excellence and should be sought as a means of increasing the impact of the results, obtaining resources for the group and envisioning new directions for future research.

The primary goal is to produce relevant contributions in the areas of expertise of the group and to disseminate them in renowned international journals and conferences. It is the group's aim that these contributions have a tangible and long-term impact on the scientific community. Technology transfer is considered a byproduct of research excellence and should be sought as a means of increasing the impact of the results, obtaining resources for the group and envisioning new directions for future research.

Recent Submissions

  • Resolution lower bounds for refutation statements 

    Garlik, Michal (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019)
    Conference report
    Open Access
    For any unsatisfiable CNF formula we give an exponential lower bound on the size of resolutionrefutations of a propositional statement that the formula has a resolution refutation. We describethree applications. (1) An ...

  • Definable inapproximability: new challenges for duplicator 

    Atserias, Albert; Dawar, Anuj (2019)
    Article
    Open Access
    We consider the hardness of approximation of optimization problems from the point of view of definability. For many NP-hard optimization problems it is known that, unless P=NP, no polynomial-time algorithm can give an ...

  • Homomorphism problems for first-order definable structures 

    Klin, Bartek; Lasota, Slawomir; Ochremiak, Joanna Regina; Torunczyk, Szymon Abram (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016)
    Conference report
    Open Access
    We investigate several variants of the homomorphism problem: given two relational structures, is there a homomorphism from one to the other? The input structures are possibly infinite, but definable by first-order ...

  • Automating Resolution is NP-hard 

    Atserias, Albert; Muller, Moritz Martin (Institute of Electrical and Electronics Engineers (IEEE), 2019)
    Conference report
    Open Access
    We show that the problem of finding a Resolution refutation that is at most polynomially longer than a shortest one is NP-hard. In the parlance of proof complexity, Resolution is not automatizable unless P = NP. Indeed, ...

  • Bridging the gap between energy consumption and distribution through non-technical loss detection 

    Coma Puig, Bernat; Carmona Vargas, Josep (2019-05-01)
    Article
    Open Access
    The application of Artificial Intelligence techniques in industry equips companies with new essential tools to improve their principal processes. This is especially true for energy companies, as they have the opportunity, ...

  • Distance-uniform graphs with large diameter 

    Lavrov, Mikhail; Loh, Po-Shen; Messegué Buisan, Arnau (2019-06-01)
    Article
    Open Access
    An ϵ-distance-uniform graph is one with a critical distance d such that from every vertex, all but at most an ϵ-fraction of the remaining vertices are at distance exactly d. Motivated by the theory of network creation ...

  • On the power of symmetric linear programs 

    Atserias, Albert; Dawar, Anuj; Ochremiak, Joanna (Institute of Electrical and Electronics Engineers (IEEE), 2019)
    Conference report
    Open Access
    We consider families of symmetric linear programs (LPs) that decide a property of graphs (or other relational structures) in the sense that, for each size of graph, there is an LP defining a polyhedral lift that separates ...

  • Size-degree trade-offs for Sums-of-Squares and Positivstellensatz proofs 

    Atserias, Albert; Hakoniemi, Tuomas Antero (Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019)
    Conference report
    Open Access
    We show that if a system of degree-k polynomial constraints on n Boolean variables has a Sums-of-Squares (SOS) proof of unsatisfiability with at most s many monomials, then it also has one whose degree is of the order of ...

  • The neighborhood role in the linear threshold rank on social networks 

    Riquelme Csori, Fabián; Gonzalez Cantergiani, Pablo; Molinero Albareda, Xavier; Serna Iglesias, María José (2019-08-15)
    Article
    Restricted access - publisher's policy
    Centrality and influence spread are two of the most studied concepts in social network analysis. Several centrality measures, most of them, based on topological criteria, have been proposed and studied. In recent years new ...

  • Circular (yet sound) proofs 

    Atserias, Albert; Lauria, Massimo (Springer, 2019)
    Conference report
    Open Access
    We introduce a new way of composing proofs in rule-based proof systems that generalizes tree-like and dag-like proofs. In the new definition, proofs are directed graphs of derived formulas, in which cycles are allowed as ...

  • RTL-aware dataflow-driven macro placement 

    Vidal Obiols, Alexandre; Cortadella, Jordi; Petit Silvestre, Jordi; Galcerán Oms, Marc; Martorell Cid, Ferran (Institute of Electrical and Electronics Engineers (IEEE), 2019)
    Conference report
    Open Access
    When RTL designers define the hierarchy of a system, they exploit their knowledge about the conceptual abstractions devised during the design and the functional interactions between the logical components. This valuable ...

  • Satellites in the prokaryote world 

    Subirana Torrent, Juan A.; Messeguer Peypoch, Xavier (2019-09-18)
    Article
    Open Access
    Background Satellites or tandem repeats are very abundant in many eukaryotic genomes. Occasionally they have been reported to be present in some prokaryotes, but to our knowledge there is no general comparative study ...

View more