Two level continuous speech recognition using demisyllable-based HMM word spotting. - Eduardo Lleida; José B. Mariño; Climent Nadeu; Albert Oliveras (EUROSPEECH, 1991)

Congruence Closure with Integer Offsets. - Robert Nieuwenhuis; Albert Oliveras (LPAR, 2003)

DPLL( T): Fast Decision Procedures. - Harald Ganzinger; George Hagen; Robert Nieuwenhuis; Albert Oliveras; Cesare Tinelli (CAV, 2004)

Abstract DPLL and Abstract DPLL Modulo Theories. - Robert Nieuwenhuis; Albert Oliveras; Cesare Tinelli (LPAR, 2004)

DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. - Robert Nieuwenhuis; Albert Oliveras (CAV, 2005)

Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. - Robert Nieuwenhuis; Albert Oliveras (LPAR, 2005)

Proof-Producing Congruence Closure. - Robert Nieuwenhuis; Albert Oliveras (RTA, 2005)

SMT Techniques for Fast Predicate Abstraction. - Shuvendu K. Lahiri; Robert Nieuwenhuis; Albert Oliveras (CAV, 2006)

Splitting on Demand in SAT Modulo Theories. - Clark W. Barrett; Robert Nieuwenhuis; Albert Oliveras; Cesare Tinelli (LPAR, 2006)

On SAT Modulo Theories and Optimization Problems. - Robert Nieuwenhuis; Albert Oliveras (SAT, 2006)

Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). - Robert Nieuwenhuis; Albert Oliveras; Cesare Tinelli (J. ACM, 2006)

Challenges in Satisfiability Modulo Theories. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (RTA, 2007)

MiniMaxSat: A New Weighted Max-SAT Solver. - Federico Heras; Javier Larrosa; Albert Oliveras (SAT, 2007)

Preface. - Sava Krstic; Albert Oliveras (SMT@CAV, 2007)

Fast congruence closure and extensions. - Robert Nieuwenhuis; Albert Oliveras (Inf. Comput., 2007)

The Barcelogic SMT Solver. - Miquel Bofill; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (CAV, 2008)

A Write-Based Solver for SAT Modulo the Theory of Arrays. - Miquel Bofill; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (FMCAD, 2008)

Efficient Generation of Unsatisfiability Proofs and Cores in SAT. - Roberto Asín; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (LPAR, 2008)

SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. - Germain Faure; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (SAT, 2008)

Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). - Clark W. Barrett; Morgan Deters; Albert Oliveras; Aaron Stump (Int. J. Artif. Intell. Tools, 2008)

MiniMaxSAT: An Efficient Weighted Max-SAT solver. - Federico Heras; Javier Larrosa; Albert Oliveras (J. Artif. Intell. Res., 2008)

Cardinality Networks and Their Applications. - Roberto Asín; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (SAT, 2009)

Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. - Javier Larrosa; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (SAT, 2009)

Semiring-Induced Propositional Logic: Definition and Basic Algorithms. - Javier Larrosa; Albert Oliveras; Enric Rodríguez-Carbonell (LPAR (Dakar), 2010)

Practical algorithms for unsatisfiability proof and core generation in SAT solvers. - Roberto Javier Asín Achá; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (AI Commun., 2010)

BDDs for Pseudo-Boolean Constraints - Revisited. - Ignasi Abío; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (SAT, 2011)

Cardinality Networks: a theoretical and empirical study. - Roberto Asín; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (Constraints An Int. J., 2011)

A Framework for Certified Boolean Branch-and-Bound Optimization. - Javier Larrosa; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (J. Autom. Reason., 2011)

A New Look at BDDs for Pseudo-Boolean Constraints. - Ignasi Abío; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Valentin Mayer-Eichberger (J. Artif. Intell. Res., 2012)

SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. - Cristina Borralleras; Salvador Lucas; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (J. Autom. Reason., 2012)

A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. - Ignasi Abío; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (CP, 2013)

To Encode or to Propagate? The Best Choice for Each Constraint in SAT. - Ignasi Abío; Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Peter J. Stuckey (CP, 2013)

Proving termination of imperative programs using Max-SMT. - Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (FMCAD, 2013)

6 Years of SMT-COMP. - Clark W. Barrett; Morgan Deters; Leonardo Mendonça de Moura; Albert Oliveras; Aaron Stump (J. Autom. Reason., 2013)

Proving Non-termination Using Max-SMT. - Daniel Larraz; Kaustubh Nimkar; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (CAV, 2014)

Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions. - Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (SAT, 2014)

Compositional Safety Verification with Max-SMT. - Marc Brockschmidt; Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (FMCAD, 2015)

Speeding up the Constraint-Based Method in Difference Logic. - Lorenzo Candeago; Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (SAT, 2016)

Proving Termination Through Conditional Termination. - Cristina Borralleras; Marc Brockschmidt; Daniel Larraz; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (TACAS (1), 2017)

Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. - Cristina Borralleras; Daniel Larraz; Enric Rodríguez-Carbonell; Albert Oliveras; Albert Rubio (ACM Trans. Comput. Log., 2019)

Decision levels are stable: towards better SAT heuristics. - Robert Nieuwenhuis; Adrià Lozano; Albert Oliveras; Enric Rodríguez-Carbonell (LPAR, 2020)

A Heuristic Approach to the Design of Optimal Cross-Docking Boxes. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (IEEE Access, 2021)

Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Emma Rollon (IEEE Access, 2021)

Analyzing Multiple Conflicts in SAT: An Experimental Evaluation. - Albert Oliveras; Enric Rodríguez-Carbonell; Rui Zhao (LPAR, 2023)

Learning Shorter Redundant Clauses in SDCL Using MaxSAT. - Albert Oliveras; Chunxiao Li 002; Darryl Wu; Jonathan Chung 003; Vijay Ganesh 001 (SAT, 2023)

Speeding up Pseudo-Boolean Propagation. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Rui Zhao (SAT, 2024)

Extended Resolution Clause Learning via Dual Implication Points. - Sam Buss; Jonathan Chung 003; Vijay Ganesh 001; Albert Oliveras (CoRR, 2024)

IntSat: integer linear programming by conflict-driven constraint learning. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell (Optim. Methods Softw., 2024)

Symbolic Conflict Analysis in Pseudo-Boolean Optimization. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Rui Zhao (SAT, 2025)