Arrow Research search

Author name cluster

Albert Oliveras

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

21 papers
2 author rows

Possible papers

21

AIJ Journal 2026 Journal Article

Using execution logs for improving Pseudo-Boolean propagation

  • Robert Nieuwenhuis
  • Albert Oliveras
  • Enric Rodríguez-Carbonell
  • Rui Zhao

Among all procedures that CDCL-based SAT solvers implement, unit propagation dominates the total running time. Hence, it is not a surprise that large research efforts have been invested on improving it. As a result, the two-watched-literal scheme, enhanced with implementation details boosting its performance, emerged as the dominant method. The importance of unit propagation in pseudo-Boolean solvers is similar. However, no dominant method exists: counter and watch-based propagation are well-suited for different types of constraints, opening the door to hybrid methods. The higher complexity of implementing pseudo-Boolean solvers has shifted the research focus to higher-level aspects of other procedures, considering implementation details of unit propagation not a priority. In this paper, we first present execution logs: a novel methodology that allows us to precisely evaluate the performance of different propagation procedures. Secondly, we show how both counter and watch-based propagation routines in the RoundingSat solver can be largely improved thanks to a careful analysis of various implementation issues. Thirdly, a detailed analysis shows that hybrid methods outperform the ones based on a single technique. Finally, our experiments reveal that improvements in propagation lead to a clearly better overall performance of the solver.

Details DOI

JAIR Journal 2025 Journal Article

Improving and Understanding the Power of Satisfaction-Driven Clause Learning

  • Albert Oliveras
  • Chunxiao Li
  • Darryl Wu
  • Jonathan Chung
  • Vijay Ganesh

In this paper, we explain how to improve Satisfaction-Driven Clause Learning (SDCL) SAT solvers by using a MaxSAT-based technique that enables them to learn shorter, and hence better, redundant clauses. A thorough empirical evaluation of an implementation on the MapleSAT solver shows that the resulting system solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver. Additionally we improve the understanding of the power of these solvers by proving that, given a refutation of a formula that consists of resolution and redundant-clause addition steps, an SDCL solver is able to produce a proof whose size is polynomial with respect to the size of the original refutation.

PDF Details DOI

SAT Conference 2025 Conference Paper

Symbolic Conflict Analysis in Pseudo-Boolean Optimization

  • Robert Nieuwenhuis
  • Albert Oliveras
  • Enric Rodríguez-Carbonell
  • Rui Zhao

In the the last two decades, a lot of effort has been devoted to the development of satisfiability-checking tools for a variety of SAT-related problems. However, most of these tools lack optimization capabilities. That is, instead of finding any solution, one is sometimes interested in a solution that is best according to some criterion. Pseudo-Boolean solvers can be used to deal with optimization by successively solving a series of problems that contain an additional pseudo-Boolean constraint expressing that a better solution is required. A key point for the success of this simple approach is that lemmas that are learned for one problem can be reused for subsequent ones. In this paper we go one step further and show how, by using a simple symbolic conflict analysis procedure, not only can lemmas be reused between problems but also strengthened, thus further pruning the search space traversal. In addition, we show how this technique automatically allows one to infer upper bounds in maximization problems, thus giving an estimation of how far the solver is from finding an optimal solution. Experimental results with our PB solver reveal that (i) this technique is indeed effective in practice, providing important speedups in problems where several solutions are found and (ii) on problems with very few solutions, where the impact of our technique is limited, its overhead is negligible.

Details

SAT Conference 2024 Conference Paper

Speeding up Pseudo-Boolean Propagation

  • Robert Nieuwenhuis
  • Albert Oliveras
  • Enric Rodríguez-Carbonell
  • Rui Zhao

Unit propagation is known to be one of the most time-consuming procedures inside CDCL-based SAT solvers. Not surprisingly, it has been studied in depth and the two-watched-literal scheme, enhanced with implementation details boosting its performance, has emerged as the dominant method. In pseudo-Boolean solvers, the importance of unit propagation is similar, but no dominant method exists: counter propagation and watched-based extensions are efficient for different types of constraints, which has opened the door to hybrid methods. However, probably due to the higher complexity of implementing pseudo-Boolean solvers, research efforts have not focused much on concrete implementation details for unit propagation but rather on higher-level aspects of other procedures, such as conflict analysis. In this paper, we present (i) a novel methodology to precisely assess the performance of propagation mechanisms, (ii) an evaluation of implementation variants of the propagation methods present in {RoundingSat} and (iii) a detailed analysis showing that hybrid methods outperform the ones based on a single technique. Our final contribution is to show that a carefully implemented hybrid propagation method is considerably faster than the preferred propagation mechanism in {RoundingSat}, and that this improvement leads to a better overall performance of the solver.

Details

LPAR Conference 2023 Conference Paper

Analyzing Multiple Conflicts in SAT: An Experimental Evaluation

  • Albert Oliveras
  • Enric Rodríguez-Carbonell
  • Rui Zhao

Unit propagation and conflict analysis are two essential ingredients of CDCL SAT Solving. The order in which unit propagation is computed does not matter when no conflict is found, because it is well known that there exists a unique unit-propagation fixpoint. However, when a conflict is found, current CDCL implementations stop and analyze that concrete conflict, even though other conflicts may exist in the unit-propagation closure. In this experimental evaluation, we report on our experience in modifying this concrete aspect in the CaDiCaL SAT Solver and try to answer the question of whether we can improve the performance of SAT Solvers by the analysis of multiple conflicts.

Details

SAT Conference 2023 Conference Paper

Learning Shorter Redundant Clauses in SDCL Using MaxSAT

  • Albert Oliveras
  • Chunxiao Li 0002
  • Darryl Wu
  • Jonathan Chung 0003
  • Vijay Ganesh 0001

In this paper we present the design and implementation of a Satisfaction-Driven Clause Learning (SDCL) SAT solver, MapleSDCL, which uses a MaxSAT-based technique that enables it to learn shorter, and hence better, redundant clauses. We also perform a thorough empirical evaluation of our method and show that our SDCL solver solves Mutilated Chess Board (MCB) problems significantly faster than CDCL solvers, without requiring any alteration to the branching heuristic used by the underlying CDCL SAT solver.

Details

LPAR Conference 2020 Conference Paper

Decision levels are stable: towards better SAT heuristics

  • Robert Nieuwenhuis
  • Adrià Lozano
  • Albert Oliveras
  • Enric Rodríguez-Carbonell

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 we define, by a real value between 0 and 1, how sticky they are, basically, how frequently they are set at the same decision level. By means of a careful and detailed experimental setup and analysis, we confirm the following quite surprising fact: given a SAT instance, when running different CDCL SAT solvers on it, no matter their settings or random seeds, the stickiness relation between literals is always very similar, in a precisely defined sense. We analyze how quickly stickiness stabilizes in a run (quite quickly), and show that it is stable even under different encodings of cardinality constraints. We then describe how and why these solid new insights lead to heuristics refinements for SAT (and extensions, such as SMT) and improved information sharing in parallel solvers.

Details

SAT Conference 2016 Conference Paper

Speeding up the Constraint-Based Method in Difference Logic

  • Lorenzo Candeago
  • Daniel Larraz
  • Albert Oliveras
  • Enric Rodríguez-Carbonell
  • Albert Rubio

Abstract 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 \le 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.

Details

SAT Conference 2014 Conference Paper

Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions

  • Daniel Larraz
  • Albert Oliveras
  • Enric Rodríguez-Carbonell
  • Albert Rubio

Abstract 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.

Details

SAT Conference 2011 Conference Paper

BDDs for Pseudo-Boolean Constraints - Revisited

  • Ignasi Abío
  • Robert Nieuwenhuis
  • Albert Oliveras
  • Enric Rodríguez-Carbonell

Abstract 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 many constraints. 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 Pseudo-Boolean constraints.

Details

SAT Conference 2009 Conference Paper

Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates

  • Javier Larrosa
  • Robert Nieuwenhuis
  • Albert Oliveras
  • Enric Rodríguez-Carbonell

Abstract We consider optimization problems of the form ( S, cost ), where S is a clause set over Boolean variables x 1. .. x n, with an arbitrary cost function cost: \({\mathbb{B}}^n {\rightarrow} {\mathbb{R}}\), and the aim is to find a model A of S such that cost ( A ) is minimized. Here we study the generation of proofs of optimality in the context of branch-and-bound procedures for such problems. For this purpose we introduce, an abstract DPLL-based branch and bound algorithm that can model optimization concepts such as cost-based propagation and cost-based backjumping. Most, if not all, SAT-related optimization problems are in the scope of. Since many of the existing approaches for solving these problems can be seen as instances, allows one to formally reason about them in a simple way and exploit the enhancements of given here, in particular its uniform method for generating independently verifiable optimality proofs.

Details

SAT Conference 2009 Conference Paper

Cardinality Networks and Their Applications

  • Roberto Javier Asín Achá
  • Robert Nieuwenhuis
  • Albert Oliveras
  • Enric Rodríguez-Carbonell

Abstract 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.

Details

LPAR Conference 2008 Conference Paper

Efficient Generation of Unsatisfiability Proofs and Cores in SAT

  • Roberto Javier Asín Achá
  • Robert Nieuwenhuis
  • Albert Oliveras
  • Enric Rodríguez-Carbonell

Abstract Some modern DPLL-based propositional SAT solvers now have fast in-memory algorithms for generating unsatisfiability proofs and cores without writing traces to disk. However, in long SAT runs these algorithms still run out of memory. For several of these algorithms, here we discuss advantages and disadvantages, based on carefully designed experiments with our implementation of each one of them, as well as with (our implementation of) Zhang and Malik’s one writing traces on disk. Then we describe a new in-memory algorithm which saves space by doing more bookkeeping to discard unnecessary information, and show that it can handle significantly more instances than the previously existing algorithms, at a negligible expense in time.

Details

SAT Conference 2008 Conference Paper

SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers

  • Germain Faure
  • Robert Nieuwenhuis
  • Albert Oliveras
  • Enric Rodríguez-Carbonell

Abstract Many highly sophisticated tools exist for solving linear arithmetic optimization and feasibility problems. Here we analyze why it is difficult to use these tools inside systems for SAT Modulo Theories (SMT) for linear arithmetic: one needs support for disequalities, strict inequalities and, more importantly, for dealing with incorrect results due to the internal use of imprecise floating-point arithmetic. We explain how these problems can be overcome by means of result checking and error recovery policies. Second, by means of carefully designed experiments with, among other tools, the newest version of ILOG CPLEX and our own new Barcelogic T -solver for arithmetic, we show that, interestingly, the cost of result checking is only a small fraction of the total T -solver time. Third, we report on extensive experiments running exactly the same SMT search using CPLEX and Barcelogic as T -solvers, where CPLEX tends to be slower than Barcelogic. We analyze these at first sight surprising results, explaining why tools such as CPLEX are not very adequate (nor designed) for this kind of relatively small incremental problems. Finally, we show how our result checking techniques can still be very useful in combination with inexact floating-point-based T -solvers designed for incremental SMT problems.

Details

I&C Journal 2007 Journal Article

Fast congruence closure and extensions

  • Robert Nieuwenhuis
  • Albert Oliveras

Congruence closure algorithms for deduction in ground equational theories are ubiquitous in many (semi-)decision procedures used for verification and automated deduction. In many of these applications one needs an incremental algorithm that is moreover capable of recovering, among the thousands of input equations, the small subset that explains the equivalence of a given pair of terms. In this paper we present an algorithm satisfying all these requirements. First, building on ideas from abstract congruence closure algorithms, we present a very simple and clean incremental congruence closure algorithm and show that it runs in the best known time O(n log n). After that, we introduce a proof-producing union-find data structure that is then used for extending our congruence closure algorithm, without increasing the overall O(n log n) time, in order to produce a k-step explanation for a given equation in almost optimal time (quasi-linear in k). Finally, we show that the previous algorithms can be smoothly extended, while still obtaining the same asymptotic time bounds, in order to support the interpreted functions symbols successor and predecessor, which have been shown to be very useful in applications such as microprocessor verification.

Details DOI

SAT Conference 2007 Conference Paper

MiniMaxSat: A New Weighted Max-SAT Solver

  • Federico Heras
  • Javier Larrosa
  • Albert Oliveras

Abstract In this paper we introduce MiniMaxSat, a new Max-SAT solver that incorporates the best SAT and Max-SAT techniques. It can handle hard clauses (clauses of mandatory satisfaction as in SAT), soft clauses (clauses whose falsification is penalized by a cost as in Max-SAT) as well as pseudo-boolean objective functions and constraints. Its main features are: learning and backjumping on hard clauses; resolution-based and subtraction-based lower bounding; and lazy propagation with the two-watched literals scheme. Our empirical evaluation on a wide set of optimization benchmarks indicates that its performance is usually close to the best specialized alternative and, in some cases, even better.

Details

SAT Conference 2006 Conference Paper

On SAT Modulo Theories and Optimization Problems

  • Robert Nieuwenhuis
  • Albert Oliveras

Abstract Solvers for SAT Modulo Theories (SMT) can nowadays handle large industrial (e. g. , formal hardware and software verification) problems over theories such as the integers, arrays, or equality. Here we show that SMT approaches can also efficiently solve problems that, at first sight, do not have a typical SMT flavor. In particular, here we deal with SAT and SMT problems where models M are sought such that a given cost function f ( M ) is minimized. For this purpose, we introduce a variant of SMT where the theory T becomes progressively stronger, and prove it correct using the Abstract DPLL Modulo Theories framework. We discuss two different examples of applications of this SMT variant: weighted Max-SAT and weighted Max-SMT. We show how, with relatively little effort, one can obtain a competitive system that, in the case of weighted Max-SMT in the theory of Difference Logic, can even handle well-known hard radio frequency assignment problems without any tailored heuristics. These results seem to indicate that Max-SAT/SMT techniques can already be used for realistic applications.

Details

LPAR Conference 2006 Conference Paper

Splitting on Demand in SAT Modulo Theories

  • Clark W. Barrett
  • Robert Nieuwenhuis
  • Albert Oliveras
  • Cesare Tinelli

Abstract Lazy algorithms for Satisfiability Modulo Theories (SMT) combine a generic DPLL-based SAT engine with a theory solver for the given theory T that can decide the T -consistency of conjunctions of ground literals. For many theories of interest, theory solvers need to reason by performing internal case splits. Here we argue that it is more convenient to delegate these case splits to the DPLL engine instead. The delegation can be done on demand for solvers that can encode their internal case splits into one or more clauses, possibly including new constants and literals. This results in drastically simpler theory solvers. We present this idea in an improved version of DPLL( T ), a general SMT architecture for the lazy approach, and formalize and prove it correct in an extension of Abstract DPLL Modulo Theories, a framework for modeling and reasoning about lazy algorithms for SMT. A remarkable additional feature of the architecture, also discussed in the paper, is that it naturally includes an efficient Nelson-Oppen-like combination of multiple theories and their solvers.

Details

LPAR Conference 2005 Conference Paper

Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools

  • Robert Nieuwenhuis
  • Albert Oliveras

Abstract An overview is given of a number of recent developments in SAT and SAT Modulo Theories (SMT). In particular, based on our framework of Abstract DPLL and Abstract DPLL modulo Theories, we explain our DPLL(T) approach to SMT. Experimental results and future projects are discussed within BarcelogicTools, a set of logic-based tools developed by our research group in Barcelona. At the 2005 SMT competition, BarcelogicTools won all four categories it participated in (out of the seven existing categories).

Details

LPAR Conference 2004 Conference Paper

Abstract DPLL and Abstract DPLL Modulo Theories

  • Robert Nieuwenhuis
  • Albert Oliveras
  • Cesare Tinelli

Abstract We introduce Abstract DPLL, a general and simple abstract rule-based formulation of the Davis-Putnam-Logemann-Loveland (DPLL) procedure. Its properties, such as soundness, completeness or termination, immediately carry over to the modern DPLL implementations with features such as non-chronological backtracking or clause learning. This allows one to formally reason about practical DPLL algorithms in a simple way. In the second part of this paper we extend the framework to Abstract DPLL modulo theories. This allows us to express—and formally reason about—state-of-the-art concrete DPLL-based techniques for satisfiability modulo background theories, such as the different lazy approaches, or our DPLL(T) framework.

Details

LPAR Conference 2003 Conference Paper

Congruence Closure with Integer Offsets

  • Robert Nieuwenhuis
  • Albert Oliveras

Congruence closure algorithms for deduction in ground equational theories are ubiquitous in many (semi-)decision procedures used for verification and automated deduction. They are also frequently used in practical contexts where some interpreted function symbols are present. In particular, for the verification of pipelined microprocessors, in many cases it suffices to be able to deal with integer offsets, that is, instead of only having ground terms t built over free symbols, all (sub)terms can be of the form t + k for arbitrary integer values k. In this paper we first give a different very simple and clean formulation for the standard congruence closure algorithm which we believe is of interest on itself. It builds on ideas from the abstract algorithms of [Kap97, BT00], but it is easily shown to run in the best known time, O ( n log n ), like the classical algorithms [DST80, NO80, Sho84]. After that, we show how this algorithm can be smoothly extended to deal with integer offsets without increasing this asymptotic complexity.

Details
v2026.09.13