Recent Submissions

  • The fractal dimension of SAT formulas 

    Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Giráldez Crú, Jesús; Levy Diaz, Jordi (Springer, 2014)
    Conference report
    Restricted access - publisher's policy
    Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is believed that these techniques exploit ...
  • Decomposing utility functions in Bounded Max-Sum for distributed constraint optimization 

    Rollón Rico, Emma; Larrosa Bondia, Francisco Javier (Springer, 2014)
    Conference report
    Restricted access - publisher's policy
    Bounded Max-Sum is a message-passing algorithm for solving distributed Constraint Optimization Problems (DCOP) able to compute solutions with a guaranteed approximation ratio. In this paper we show that the introduction ...
  • The IntSat method for integer linear programming 

    Nieuwenhuis, Robert Lukas Mario (Springer, 2014)
    Conference report
    Restricted access - publisher's policy
    Conflict-Driven Clause-Learning (CDCL) SAT solvers can automatically solve very large real-world problems. To go beyond, and in particular in order to solve and optimize problems involving linear arithmetic constraints, ...
  • Proving non-termination using max-SMT 

    Larraz Hurtado, Daniel; Nimkar, Kaustubh; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (Springer, 2014)
    Conference report
    Open Access
    We show how Max-SMT-based invariant generation can be exploited for proving non-termination of programs. The construction of the proof of non-termination is guided by the generation of quasi-invariants - properties such ...
  • Minimal-model-guided approaches to solving polynomial constraints and extensions 

    Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (Springer, 2014)
    Conference report
    Open Access
    In this paper we present new methods for deciding the satisfiability of formulas involving integer polynomial constraints. In previous work we proposed to solve SMT(NIA) problems by reducing them to SMT(LIA): non-linear ...
  • Nominal completion for rewrite systems with binders 

    Fernández, Maribel; Rubio Gimeno, Alberto (Springer, 2012)
    Conference report
    Restricted access - publisher's policy
    We design a completion procedure for nominal rewriting systems, based on a generalisation of the recursive path ordering to take into account alpha equivalence. Nominal rewriting generalises first-order rewriting by providing ...
  • Semiring-based mini-bucket partitioning schemes 

    Rollón Rico, Emma; Larrosa Bondia, Francisco Javier; Dechter, Rina (AAAI Press. Association for the Advancement of Artificial Intelligence, 2013)
    Conference report
    Restricted access - publisher's policy
    Graphical models are one of the most prominent frameworks to model complex systems and efficiently query them. Their underlying algebraic properties are captured by a valuation structure that, most usually, is a semiring. ...
  • Improving WPM2 for (weighted) partial MaxSAT 

    Ansótegui Gil, Carlos; Bonet Carbonell, M. Luisa; Gabàs, Joel; Levy Díaz, Jordi (Springer, 2013)
    Conference report
    Restricted access - publisher's policy
    Weighted Partial MaxSAT (WPMS) is an optimization variant of the Satisfiability (SAT) problem. Several combinatorial optimization problems can be translated into WPMS. In this paper we extend the state-of-the-art WPM2 ...
  • 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)
    Conference report
    Open Access
    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 ...
  • 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)
    Conference report
    Open Access
    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 ...

View more