Albert Oliveras

56 papers A* 5A 13B 10Journal 21Unranked 6

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