• A parametric approach for smaller and better encodings of cardinality constraints 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer, 2013)
      Text en actes de congrés
      Accés obert
      Adequate encodings for high-level constraints are a key ingredient for the application of SAT technology. In particular, cardinality constraints state that at most (at least, or exactly) k out of n propositional variables ...
    • BDDs for Pseudo-Boolean Constraints 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer Verlag, 2011)
      Text en actes de congrés
      Accés restringit per política de l'editorial
      Pseudo-Boolean constraints are omnipresent in practical applications, and therefore a significant effort has been devoted to the development of good SAT encoding techniques for these constraints. Several of these encodings ...
    • Classification of plane germs: metric and valorative properties 

      Abío Roig, Ignasi (Universitat Politècnica de Catalunya, 2008-06)
      Projecte/Treball Final de Carrera
      Accés obert
      In this memory we follow the geometric approach of Casas’ boof [1] for studying of the singularities of plane germs of curves, which updates Enriques’ works to modern standards and reviews the modern development of the ...
    • Reducing chaos in SAT-like search: finding solutions close to a given one 

      Abío Roig, Ignasi; Deters, Morgan; Nieuwenhuis, Robert Lukas Mario; Stuckey, Peter (Springer Verlag, 2011)
      Text en actes de congrés
      Accés restringit per política de l'editorial
      Motivated by our own industrial users, we attack the following challenge that is crucial in many practical planning, scheduling or timetabling applications. Assume that a solver has found a solution for a given hard ...
    • Solving hard industrial combinatorial problems with SAT 

      Abío Roig, Ignasi (Universitat Politècnica de Catalunya, 2013-05-15)
      Tesi
      Accés obert
      The topic of this thesis is the development of SAT-based techniques and tools for solving industrial combinatorial problems. First, it describes the architecture of state-of-the-art SAT and SMT Solvers based on the classical ...
    • The ultrametric space of plane branches 

      Abío Roig, Ignasi; Alberich Carramiñana, Maria; González Alonso, Víctor (2011)
      Article
      Accés restringit per política de l'editorial
      We study properties of the space of irreducible germs of plane curves (branches), seen as an ultrametric space. We provide various geometrical methods to measure the distance between two branches and to compare distances ...
    • The ultrametric space of plane branches 

      Abío Roig, Ignasi; Alberich Carramiñana, Maria; González Alonso, Víctor (2010-08)
      Report de recerca
      Accés obert
      We study properties of the space of irreducible germs of plane curves (branches), seen as an ultrametric space. We provide various geometrical methods to measure the distance between two branches and to compare distances ...
    • To encode or to propagate? The best choice for each constraint in SAT 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Stuckey, Peter (Springer, 2013)
      Text en actes de congrés
      Accés obert
      Sophisticated compact SAT encodings exist for many types of constraints. Alternatively, for instances with many (or large) constraints, the SAT solver can also be extended with built-in propagators (the SAT Modulo Theories ...