Candeago, L.; Larraz, D.; Oliveras, A.; Rodriguez, E.; Rubio, A. International Conference on Theory and Applications of Satisfiability Testing p. 284-301 DOI: 10.1007/978-3-319-40970-2_18 Data de presentació: 2016-07 Presentació treball a congrés
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 the program under study as well as the properties to be generated belong to difference logic, i.e., the fragment of linear arithmetic where atoms are inequalities of the form u v = k. However, so far constraint-based techniques have not exploited this fact: in general, Farkas’ Lemma is used to produce the constraints over template unknowns, which leads to non-linear SMT problems. Based on classical results of graph theory, in this paper we propose new encodings for generating these constraints when program semantics and templates belong to difference logic. Thanks to this approach, instead of a heavyweight non-linear arithmetic solver, a much cheaper SMT solver for difference logic or linear integer arithmetic can be employed for solving the resulting constraints. We present encouraging experimental results that show the high impact of the proposed techniques on the performance of the VeryMax verification system
Brockschmidt, M.; Larraz, D.; Oliveras, A.; Rodriguez, E.; Rubio, A. International Conference on Formal Methods in Computer-Aided Design p. 33-40 Data de presentació: 2015-09-28 Presentació treball a congrés
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 a Max-SMT solver, an inductive invariant together with a precondition can be synthesized so that the precondition ensures the validity of the invariant and that the invariant implies the postcondition. From this, we build a bottom-up program verification framework that propagates preconditions of small program parts as postconditions for preceding program parts. The method recovers from failures to prove the validity of a precondition, using the obtained intermediate results to restrict the search space for further proof attempts. As only small program parts need to be handled at a time, our method is scalable and distributable. The derived conditions can be viewed as implicit contracts between different parts of the program, and thus enable an incremental program analysis.
Larraz, D.; Oliveras, A.; Rodriguez, E.; Rubio, A. International Conference on Theory and Applications of Satisfiability Testing p. 333-350 DOI: 10.1007/978-3-319-09284-3-25 Data de presentació: 2014-07 Presentació treball a congrés
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 monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. When variables do not have finite domains, artificial ones can be introduced by imposing a lower and an upper bound, and made iteratively larger until a solution is found (or the procedure times out). For the approach to be practical, unsatisfiable cores are used to guide which domains have to be relaxed (i.e., enlarged) from one iteration to the following one. However, it is not clear then how large they have to be made, which is critical. Here we propose to guide the domain relaxation step by analyzing minimal models produced by the SMT(LIA) solver. Namely, we consider two different cost functions: the number of violated artificial domain bounds, and the distance with respect to the artificial domains. We compare these approaches with other techniques on benchmarks coming from constraint-based program analysis and show the potential of the method. Finally, we describe how one of these minimal-model-guided techniques can be smoothly adapted to deal with the extension Max-SMT of SMT(NIA) and then applied to program termination proving.
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 that if they hold at a location during execution once, then they will continue to hold at that location from then onwards. The check that quasi-invariants can indeed be reached is then performed separately. Our technique considers strongly connected subgraphs of a program's control flow graph for analysis and thus produces more generic witnesses of non-termination than existing methods. Moreover, it can handle programs with unbounded non-determinism and is more likely to converge than previous approaches.
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 weights, quasi-ranking functions --functions that almost satisfy all conditions for ensuring well-foundedness-- are produced in a lack of ranking functions. By means of trace partitioning, this allows our method to progress in the termination analysis where other approaches would get stuck. Moreover, Max-SMT makes it easy to combine the process of building the termination argument with the usually necessary task of generating supporting invariants. The method has been implemented in a prototype that has successfully been tested on a wide set of programs.
Abio, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E. International Conference on Principles and Practice of Constraint Programming p. 80-96 DOI: 10.1007/978-3-642-40627-0_9 Data de presentació: 2013-09-16 Presentació treball a congrés
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 can be true. They are crucial in many applications. Although sophisticated encodings for cardinality constraints exist, it is well known that for small n and k straightforward encodings without auxiliary variables sometimes behave better, and that the choice of the right trade-off between minimizing either the number of variables or the number of clauses is highly application-dependent. Here we build upon previous work on Cardinality Networks to get the best of several worlds: we develop an arc-consistent encoding that, by recursively decomposing the constraint into smaller ones, allows one to decide which encoding to apply to each sub-constraint. This process minimizes a function λ·num- vars + num-clauses, where λ is a parameter that can be tuned by the user. Our careful experimental evaluation shows that (e.g., for λ = 5) this new technique produces much smaller encodings in variables and clauses, and indeed strongly improves SAT solvers' performance.
Abio, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.; Stuckey, P. International Conference on Principles and Practice of Constraint Programming p. 97-106 DOI: 10.1007/978-3-642-40627-0_10 Data de presentació: 2013-09-16 Presentació treball a congrés
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 approach, SMT). For example, given a cardinality constraint x 1 + … + x n ≤ k, as soon as k variables become true, such a propagator can set the remaining variables to false, generating a so-called explanation clause of the form x1∧…∧xk→xi¯ . But certain “bottle-neck” constraints end up generating an exponential number of explanations, equivalent to a naive SAT encoding, much worse than using a compact encoding with auxiliary variables from the beginning. Therefore, Abío and Stuckey proposed starting off with a full SMT approach and partially encoding, on the fly, only certain “active” parts of constraints. Here we build upon their work. Equipping our solvers with some additional bookkeeping to monitor constraint activity has allowed us to shed light on the effectiveness of SMT: many constraints generate very few, or few different, explanations. We also give strong experimental evidence showing that it is typically unnecessary to consider partial encodings: it is competitive to encode the few really active constraints entirely. This makes the approach amenable to any kind of constraint, not just the ones for which partial encodings are known.
El tema d'aquesta tesi és el desenvolupament de tècniques i eines basades en SAT per solucionar problemes combinatoris industrials. Primer, descrivim l'arquitectura dels SAT i SMT Solvers actuals, basats en l'algorisme DPLL. Aquests sistemes es poden usar com a caixes negres per resoldre problemes combinatoris. Malgrat això, sovint podem incrementar la seva eficiència amb petites modificacions de l'algorisme bàsic. Per això, el primer objectiu de la tesi és l'estudi i desenvolupament de tècniques per ajustar els SAT Solvers a problemes combinatoris concrets. Els SAT Solvers només poden tractar lògica proposicional. Per resoldre problemes combinatoris generals, es poden considerar els següents mètodes:¿Reduir els constraints complexos a clàusules proposicionals.¿Enriquir el llenguatge del SAT Solver. El primer mètode correspon a codificar un constraint a SAT. El segon, a usar propagadors, la peça bàsica dels SMT Solvers. Respecte el primer mètode, en aquest document millorem la codificació de dos dels constraints combinatoris més importants: els cardinality i els pseudo-Boolean constraints. Després, presentem un mètode mixt, anomenat "lazy decomposition", que combina els avantatges de propagadors i codificacions.L'altre part de la tesi usa aquestes millores teòriques en problemes combinatoris industrials. Donem un mètode per construir eficientment amb SAT calendaris per algunes lligues esportives professionals. Els resultats són prometedors i mostren que SAT és una eina vàlida per aquests problemes.Malgrat això, el comportament caòtic dels SAT Solvers basats en CDCL, degut a les heurístiques VSIDS, fan difícil que s'obtinguin resultats similars en dos problemes semblants. Això pot ser un inconvenient en problemes del món real, ja que els usuaris esperen obtenir solucions semblants quan es modifica lleugerament l'especificació del problema. Per resoldre aquesta limitació, hem estudiat i resolt el problema de close solution, és a dir, el problema de trobar ràpidament solucions properes quan es consideren problemes similars.
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 DPLL procedure. These systems can be used as black boxes for solving combinatorial problems. However, sometimes we can increase their efficiency with slight modifications of the basic algorithm. Therefore, the study and development of techniques for adjusting SAT Solvers to specific combinatorial problems is the first goal of this thesis.
Namely, SAT Solvers can only deal with propositional logic. For solving general combinatorial problems, two different approaches are possible:
- Reducing the complex constraints into propositional clauses.
- Enriching the SAT Solver language.
The first approach corresponds to encoding the constraint into SAT. The second one corresponds to using propagators, the basis for SMT Solvers. Regarding the first approach, in this document we improve the encoding of two of the most important combinatorial constraints: cardinality constraints and pseudo-Boolean constraints. After that, we present a new mixed approach, called lazy decomposition, which combines the advantages of encodings and propagators.
The other part of the thesis uses these theoretical improvements in industrial combinatorial problems. We give a method for efficiently scheduling some professional sport leagues with SAT. The results are promising and show that a SAT approach is valid for these problems.
However, the chaotical behavior of CDCL-based SAT Solvers due to VSIDS heuristics makes it difficult to obtain a similar solution for two similar problems. This may be inconvenient in real-world problems, since a user expects similar solutions when it makes slight modifications to the problem specification. In order to overcome this limitation, we have studied and solved the close solution problem, i.e., the problem of quickly finding a close solution when a similar problem is considered.
Duch, A.; Petit, J.; Rodriguez, E.; Roura, S. International Conference on Computer Supported Education p. 437-442 DOI: 10.5220/0004389604370442 Data de presentació: 2013-05-07 Presentació treball a congrés
We report our experience of including the implementation of a player of a computer game as a programming project in a CS2 course focusing in data structures and algorithms. Every semester, an instructor designs the rules of a game, prepares its visualization, and implements an elementary player with a very simple strategy. The game is then delivered to students who, as a first step in order to pass the project, must program a player that wins the elementary player. Then, a tournament begins among all the students with accepted players. At
every round of this tournament a player is eliminated until just one player, the champion, survives. Grades for this assignment are computed automatically and increasingly with respect to the round where students have been eliminated. The result is a fun and very motivating programming experience for our students.
In most termination tools two ingredients, namely recursive path orderings (RPOs) and polynomial interpretation orderings (POLOs), are used in a consecutive disjoint way to solve the final constraints generated from the termination problem. In this article we present a simple ordering that combines both RPO and POLO and defines a family of orderings that includes both, and extend them with the possibility of having, at the same time, an RPO-like treatment for some symbols and a POLO-like treatment for the others. The ordering is extended to higher-order terms, providing a new fully automatable use of polynomial interpretations in combination with beta-reduction.
Abio, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.; Mayer, V. Journal of artificial intelligence research Vol. 45, num. 1, p. 443-480 DOI: 10.1613/jair.3653 Data de publicació: 2012 Article en revista
Pseudo-Boolean constraints are omnipresent in practical applications, and thus a significant effort has been devoted to the development of good SAT encoding techniques for them. Some of these encodings first construct a Binary Decision Diagram (BDD) for the constraint, and then encode the BDD into a propositional formula. These BDD-based approaches have some important advantages, such as not being dependent on the size of the coefficients, or being able to share the same BDD for representing many constraints. We first focus on the size of the resulting BDDs, which was considered to be an open problem in our research community. We report on previous work where it was proved that there are Pseudo-Boolean constraints for which no polynomial BDD exists. We also give an alternative and simpler proof assuming that NP is different from Co-NP. More interestingly, here we also show how to overcome the possible exponential blowup of BDDs by coefficient decomposition. This allows us to give the first polynomial generalized arc-consistent ROBDD-based encoding for Pseudo-Boolean constraints. Finally, we focus on practical issues: we show how to efficiently construct such ROBDDs, how to encode them into SAT with only 2 clauses per node, and present experimental results that confirm that our approach is competitive with other encodings and state-of-the-art Pseudo-Boolean solvers.
Abío, I.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E. International Conference on Theory and Applications of Satisfiability Testing p. 61-75 DOI: 10.1007/978-3-642-21581-0_7 Data de presentació: 2011-06-21 Presentació treball a congrés
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 are based on building Binary Decision Diagrams
(BDDs) and translating these into CNF. Indeed, BDD-based encodings
have important advantages, such as sharing the same BDD for representing
Here we first prove that, unless NP = Co-NP, there are Pseudo-
Boolean constraints that admit no variable ordering giving a polynomial
(Reduced, Ordered) BDD. As far as we know, this result is new (in
spite of some misleading information in the literature). It gives several
interesting insights, also relating proof complexity and BDDs.
But, more interestingly for practice, here we also show how to overcome
this theoretical limitation by coefficient decomposition. This allows
us to give the first polynomial arc-consistent BDD-based encoding for
Borralleras, C.; Lucas, S.; Oliveras, A.; Rodriguez, E.; Rubio, A. Journal of automated reasoning Vol. 48, num. 1, p. 107-131 DOI: 10.1007/s10817-010-9196-8 Data de publicació: 2010-09-04 Article en revista
Larrosa, J.; Oliveras, A.; Rodriguez, E. International Conference on Logic for Programming, Artificial Intelligence and Reasoning p. 332-347 DOI: 10.1007/978-3-642-17511-4_19 Data de presentació: 2010-04 Presentació treball a congrés
Asín, R.J.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E. AI communications: the european journal of artificial intelligence Vol. 23, num. 2-3, p. 145-157 DOI: 10.3233/AIC-2010-0462 Data de publicació: 2010 Article en revista
Asín, R.J.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E. International Conference on Theory and Applications of Satisfiability Testing p. 167-180 DOI: 10.1007/978-3-642-02777-2_18 Data de presentació: 2009-06-30 Presentació treball a congrés
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 variables, while arc consistency is still preserved: e.g., for a constraint x 1 + ... + x n ≤ k, as soon as k variables among the x i ’s become true, unit propagation sets all other x i ’s to false. Our encoding also still admits incremental strengthening: this constraint for any smaller k is obtained without adding any new clauses, by setting a single variable to false.
Here we give precise recursive definitions of the clause sets that are needed and give detailed proofs of the required properties. We demonstrate the practical impact of this new encoding by careful experiments comparing it with previous encodings on real-world instances.
Larrosa, J.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E. International Conference on Theory and Applications of Satisfiability Testing p. 453-466 DOI: 10.1007/978-3-642-02777-2_42 Data de presentació: 2009 Presentació treball a congrés
Borralleras, C.; Lucas, S.; Navarro, R.; Rodriguez, E.; Rubio, A. International Conference on Automated Deduction p. 294-305 DOI: 10.1007/978-3-642-02959-2_23 Data de presentació: 2009 Presentació treball a congrés
Bofill, M.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.; Rubio, A. Formal Methods in Computer-Aided Design 2008 (FMCAD) p. 1-8 DOI: 10.1109/FMCAD.2008.ECP.18 Data de presentació: 2008 Presentació treball a congrés
Faure, G.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E. International Conference on Theory and Applications of Satisfiability Testing p. 77-90 DOI: 10.1007/978-3-540-79719-7_8 Presentació treball a congrés
Bofill, M.; Nieuwenhuis, R.; Oliveras, A.; Rodriguez, E.; Rubio, A. International Conference on Computer Aided Verification p. 294-298 DOI: 10.1007/978-3-540-70545-1_27 Data de presentació: 2008 Presentació treball a congrés
A technique for generating invariant polynomial inequalities
of bounded degree is presented using the abstract interpretation
framework. It is based on overapproximating basic semi-algebraic
sets, i.e., sets defined by conjunctions of polynomial inequalities,
by means of convex polyhedra. While improving on the existing methods
for generating invariant polynomial equalities, since
polynomial inequalities are allowed in the guards of the transition
system, the approach does not suffer from the prohibitive complexity
of methods based on quantifier-elimination. The application of our
implementation to benchmark programs shows that the method produces
non-trivial invariants in reasonable time. In some cases the
generated invariants are essential to verify safety properties that
cannot be proved with just classical linear invariants.