| 2026 | SAT | WhyUnsat: A Practical Explanation Tool (Tool Paper). | Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell |
| 2025 | SAT | Symbolic Conflict Analysis in Pseudo-Boolean Optimization. | Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell, Rui Zhao |
| 2024 | SAT | Speeding up Pseudo-Boolean Propagation. | Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell, Rui Zhao |
| 2020 | LPAR | Decision levels are stable: towards better SAT heuristics. | Robert Nieuwenhuis, Adri Lozano, Albert Oliveras, Enric Rodrguez-Carbonell |
| 2014 | CP | The IntSat Method for Integer Linear Programming. | Robert Nieuwenhuis |
| 2013 | CP | A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. | Ignasi Abo, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell |
| 2013 | CP | To Encode or to Propagate? The Best Choice for Each Constraint in SAT. | Ignasi Abo, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell, Peter J. Stuckey |
| 2012 | CADE | SAT and SMT Are Still Resolution: Questions and Challenges. | Robert Nieuwenhuis |
| 2011 | SAT | Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One. | Ignasi Abo, Morgan Deters, Robert Nieuwenhuis, Peter J. Stuckey |
| 2011 | SAT | BDDs for Pseudo-Boolean Constraints - Revisited. | Ignasi Abo, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell |
| 2010 | CP | SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering. | Robert Nieuwenhuis |
| 2009 | SAT | Cardinality Networks and Their Applications. | Roberto Asn, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell |
| 2009 | SAT | Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. | Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell |
| 2009 | SAT | SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms. | Robert Nieuwenhuis |
| 2008 | CAV | The Barcelogic SMT Solver. | Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2008 | FMCAD | A Write-Based Solver for SAT Modulo the Theory of Arrays. | Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell, Albert Rubio |
| 2008 | LPAR | Efficient Generation of Unsatisfiability Proofs and Cores in SAT. | Roberto Asn, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell |
| 2008 | LPAR | The Max-Atom Problem and Its Relevance. | Marc Bezem, Robert Nieuwenhuis, Enric Rodrguez-Carbonell |
| 2008 | SAT | SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. | Germain Faure, Robert Nieuwenhuis, Albert Oliveras, Enric Rodrguez-Carbonell |
| 2006 | CAV | SMT Techniques for Fast Predicate Abstraction. | Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras |
| 2006 | LPAR | Splitting on Demand in SAT Modulo Theories. | Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2006 | SAT | On SAT Modulo Theories and Optimization Problems. | Robert Nieuwenhuis, Albert Oliveras |
| 2005 | CAV | DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. | Robert Nieuwenhuis, Albert Oliveras |
| 2005 | LPAR | Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. | Robert Nieuwenhuis, Albert Oliveras |
| 2004 | CAV | DPLL( T): Fast Decision Procedures. | Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2004 | LPAR | Abstract DPLL and Abstract DPLL Modulo Theories. | Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli |
| 2003 | LPAR | Congruence Closure with Integer Offsets. | Robert Nieuwenhuis, Albert Oliveras |
| 2001 | CADE | Context Trees. | Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela |
| 2001 | CADE | On the Evaluation of Indexing Techniques for Theorem Proving. | Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov |
| 2001 | FOCS | The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time. | Hubert Comon, Guillem Godoy, Robert Nieuwenhuis |
| 2001 | LICS | On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. | Guillem Godoy, Robert Nieuwenhuis |
| 2000 | LICS | Paramodulation with Built-in Abelian Groups. | Guillem Godoy, Robert Nieuwenhuis |
| 1999 | CADE | Invited Talk: Rewrite-based Deduction and Symbolic Constraints. | Robert Nieuwenhuis |
| 1999 | LICS | Paramodulation with Non-Monotonic Orderings. | Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio |
| 1998 | LICS | Decision Problems in Ordered Rewriting. | Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michal Rusinowitch |
| 1997 | CADE | Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. | Robert Nieuwenhuis, Jos Miguel Rivero, Miguel ngel Vallejo |
| 1996 | LICS | Basic Paramodulation and Decidable Theories (Extended Abstract). | Robert Nieuwenhuis |
| 1995 | LICS | Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) | Hubert Comon, Robert Nieuwenhuis, Albert Rubio |
| 1994 | CADE | AC-Superposition with Constraints: No AC-Unifiers Needed. | Robert Nieuwenhuis, Albert Rubio |
| 1992 | CADE | Theorem Proving with Ordering Constrained Clauses. | Robert Nieuwenhuis, Albert Rubio |
| 1992 | ESOP | Basic Superposition is Complete. | Robert Nieuwenhuis, Albert Rubio |
| 1990 | CADE | TRIP: An Implementation of Clausal Rewriting. | Robert Nieuwenhuis, Fernando Orejas, Albert Rubio |