Albert Oliveras

Publication Activity (10 Years)

Years Active: 1991-2024
Publications (10 Years): 13

Top Topics

Integer Linear Programming

Clause Learning

Top Venues

Publications

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
IntSat: integer linear programming by conflict-driven constraint learning. Optim. Methods Softw. 39 (1) (2024)
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning. CoRR (2024)
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao
Speeding up Pseudo-Boolean Propagation. SAT (2024)
Sam Buss, Jonathan Chung, Vijay Ganesh, Albert Oliveras
Extended Resolution Clause Learning via Dual Implication Points. CoRR (2024)
Albert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao
Analyzing Multiple Conflicts in SAT: An Experimental Evaluation. LPAR (2023)
Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, Vijay Ganesh
Learning Shorter Redundant Clauses in SDCL Using MaxSAT. SAT (2023)
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
A Heuristic Approach to the Design of Optimal Cross-Docking Boxes. IEEE Access 9 (2021)
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Emma Rollon
Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving. IEEE Access 9 (2021)
Robert Nieuwenhuis, Adrià Lozano, Albert Oliveras, Enric Rodríguez-Carbonell
Decision levels are stable: towards better SAT heuristics. LPAR (2020)
Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. CoRR (2020)
Cristina Borralleras, Daniel Larraz, Enric Rodríguez-Carbonell, Albert Oliveras, Albert Rubio
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers. ACM Trans. Comput. Log. 20 (4) (2019)
Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Proving Termination Through Conditional Termination. TACAS (1) (2017)
Lorenzo Candeago, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Speeding up the Constraint-Based Method in Difference Logic. SAT (2016)
Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Compositional Safety Verification with Max-SMT. FMCAD (2015)
Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Compositional Safety Verification with Max-SMT. CoRR (2015)
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Valentin Mayer-Eichberger
A New Look at BDDs for Pseudo-Boolean Constraints. CoRR (2014)
Daniel Larraz, Kaustubh Nimkar, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Proving Non-termination Using Max-SMT. CAV (2014)
Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions. SAT (2014)
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Peter J. Stuckey
To Encode or to Propagate? The Best Choice for Each Constraint in SAT. CP (2013)
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. CP (2013)
Clark W. Barrett, Morgan Deters, Leonardo Mendonça de Moura, Albert Oliveras, Aaron Stump
6 Years of SMT-COMP. J. Autom. Reason. 50 (3) (2013)
Daniel Larraz, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Proving termination of imperative programs using Max-SMT. FMCAD (2013)
Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. J. Autom. Reason. 48 (1) (2012)
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Valentin Mayer-Eichberger
A New Look at BDDs for Pseudo-Boolean Constraints. J. Artif. Intell. Res. 45 (2012)
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
BDDs for Pseudo-Boolean Constraints - Revisited. SAT (2011)
Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
A Framework for Certified Boolean Branch-and-Bound Optimization. J. Autom. Reason. 46 (1) (2011)
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Cardinality Networks: a theoretical and empirical study. Constraints An Int. J. 16 (2) (2011)
Javier Larrosa, Albert Oliveras, Enric Rodríguez-Carbonell
Semiring-Induced Propositional Logic: Definition and Basic Algorithms. LPAR (Dakar) (2010)
Roberto Javier Asín Achá, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Commun. 23 (2-3) (2010)
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Cardinality Networks and Their Applications. SAT (2009)
Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. SAT (2009)
Clark W. Barrett, Morgan Deters, Albert Oliveras, Aaron Stump
Design and Results of the 3rd Annual Satisfiability Modulo Theories Competition (SMT-Comp 2007). Int. J. Artif. Intell. Tools 17 (4) (2008)
Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Efficient Generation of Unsatisfiability Proofs and Cores in SAT. LPAR (2008)
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
The Barcelogic SMT Solver. CAV (2008)
Federico Heras, Javier Larrosa, Albert Oliveras
MiniMaxSAT: An Efficient Weighted Max-SAT solver. J. Artif. Intell. Res. 31 (2008)
Sava Krstic, Albert Oliveras
Preface. Electron. Notes Theor. Comput. Sci. 198 (2) (2008)
Germain Faure, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. SAT (2008)
Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
A Write-Based Solver for SAT Modulo the Theory of Arrays. FMCAD (2008)
Federico Heras, Javier Larrosa, Albert Oliveras
MiniMaxSat: A New Weighted Max-SAT Solver. SAT (2007)
Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
Challenges in Satisfiability Modulo Theories. RTA (2007)
Robert Nieuwenhuis, Albert Oliveras
Fast congruence closure and extensions. Inf. Comput. 205 (4) (2007)
Robert Nieuwenhuis, Albert Oliveras
On SAT Modulo Theories and Optimization Problems. SAT (2006)
Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
Splitting on Demand in SAT Modulo Theories. LPAR (2006)
Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras
SMT Techniques for Fast Predicate Abstraction. CAV (2006)
Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
). J. ACM 53 (6) (2006)
Robert Nieuwenhuis, Albert Oliveras
Proof-Producing Congruence Closure. RTA (2005)
Robert Nieuwenhuis, Albert Oliveras
Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. LPAR (2005)
Robert Nieuwenhuis, Albert Oliveras
DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. CAV (2005)
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
DPLL( T): Fast Decision Procedures. CAV (2004)
Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
Abstract DPLL and Abstract DPLL Modulo Theories. LPAR (2004)
Robert Nieuwenhuis, Albert Oliveras
Congruence Closure with Integer Offsets. LPAR (2003)
Eduardo Lleida, José B. Mariño, Climent Nadeu, Albert Oliveras
Two level continuous speech recognition using demisyllable-based HMM word spotting. EUROSPEECH (1991)