Now showing items 1-12 of 12

    • 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 ...
    • BDDs for Pseudo-Boolean Constraints 

      Abío Roig, Ignasi; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer Verlag, 2011)
      Conference report
      Restricted access - publisher's policy
      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 ...
    • Cardinality networks and their applications 

      Asín Acha, Roberto Javier; Nieuwenhuis, Robert Lukas Mario; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (Springer, 2009)
      Conference report
      Restricted access - publisher's policy
      We introduce Cardinality Networks, a new CNF encoding of cardinality constraints. It improves upon the previously existing encodings such as the sorting networks of [ES06] in that it requires much less clauses and auxiliary ...
    • Compositional safety verification with Max-SMT 

      Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2015)
      Conference report
      Open Access
      We present an automated compositional program verification technique for safety properties based on conditional inductive invariants. For a given program part (e.g., a single loop) and a postcondition, we show how to, using ...
    • Decision levels are stable: towards better SAT heuristics 

      Nieuwenhuis, Robert Lukas Mario; Lozano Navarro, Adrián; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric (EasyChair Publications, 2020)
      Conference report
      Restricted access - publisher's policy
      We shed new light on the Literal Block Distance (LBD) and glue-based heuristics used in current SAT solvers. For this, we first introduce the concept of stickiness: given a run of a CDCL SAT solver, for each pair of literals ...
    • Incomplete SMT techniques for solving non-linear formulas over the integers 

      Borralleras Andreu, Cristina; Larraz Hurtado, Daniel; Rodríguez Carbonell, Enric; Oliveras Llunell, Albert; Rubio Gimeno, Alberto (2019-08-01)
      Article
      Open Access
      We present new methods for solving the Satisfiability Modulo Theories problem over the theory of QuantifierFree Non-linear Integer Arithmetic, SMT(QF-NIA), which consists of deciding the satisfiability of ground formulas ...
    • 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 ...
    • 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 ...
    • Proving termination of imperative programs using Max-SMT 

      Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2013)
      Conference report
      Open Access
      We show how Max-SMT can be exploited in constraint-based program termination proving. Thanks to expressing the generation of a ranking function as a Max-SMT optimization problem where constraints are assigned different ...
    • Proving termination through conditional termination 

      Borralleras Andreu, Cristina; Brockschmidt, Marc; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (Springer, 2017)
      Conference report
      Open Access
      We present a constraint-based method for proving conditional termination of integer programs. Building on this, we construct a framework to prove (unconditional) program termination using a powerful mechanism to combine ...
    • Speeding up the constraint-based method in difference logic 

      Candeago, L.; Larraz Hurtado, Daniel; Oliveras Llunell, Albert; Rodríguez Carbonell, Enric; Rubio Gimeno, Alberto (2016)
      Conference report
      Open Access
      Over the years the constraint-based method has been successfully applied to a wide range of problems in program analysis, from invariant generation to termination and non-termination proving. Quite often the semantics of ...
    • 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 ...