Clausal Rewriting: Applications and Implementation. - Robert Nieuwenhuis; Fernando Orejas (ADT, 1990)

TRIP: An Implementation of Clausal Rewriting. - Robert Nieuwenhuis; Fernando Orejas; Albert Rubio (CADE, 1990)

Clausal Rewriting. - Robert Nieuwenhuis; Fernando Orejas (CTRS, 1990)

Efficient Deduction in Equality Horn Logic by Horn-Completion. - Robert Nieuwenhuis; Pilar Nivela (Inf. Process. Lett., 1991)

Theorem Proving with Ordering Constrained Clauses. - Robert Nieuwenhuis; Albert Rubio (CADE, 1992)

Basic Superposition is Complete. - Robert Nieuwenhuis; Albert Rubio (ESOP, 1992)

Program Development: Completion Subsystem. - Hubert Bertling; Harald Ganzinger; Renate Schäfers; Robert Nieuwenhuis; Fernando Orejas (PROSPECTRA Book, 1993)

Saturation of First-Order (Constrained) Clauses with the Saturate System. - Pilar Nivela; Robert Nieuwenhuis (RTA, 1993)

A Precedence-Based Total AC-Compatible Ordering. - Albert Rubio; Robert Nieuwenhuis (RTA, 1993)

Simple LPO Constraint Solving Methods. - Robert Nieuwenhuis (Inf. Process. Lett., 1993)

AC-Superposition with Constraints: No AC-Unifiers Needed. - Robert Nieuwenhuis; Albert Rubio (CADE, 1994)

Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) - Hubert Comon; Robert Nieuwenhuis; Albert Rubio (LICS, 1995)

On Narrowing, Refutation Proofs and Constraints. - Robert Nieuwenhuis (RTA, 1995)

Theorem Proving with Ordering and Equality Constrained Clauses. - Robert Nieuwenhuis; Albert Rubio (J. Symb. Comput., 1995)

A Total AC-Compatible Ordering Based on RPO. - Albert Rubio; Robert Nieuwenhuis (Theor. Comput. Sci., 1995)

An Implementation Kernel for Theorem Proving with Equality Clauses. - Robert Nieuwenhuis; José Miguel Rivero; Miguel Ángel Vallejo (APPIA-GULP-PRODE, 1996)

Basic Paramodulation and Decidable Theories (Extended Abstract). - Robert Nieuwenhuis (LICS, 1996)

Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. - Robert Nieuwenhuis; José Miguel Rivero; Miguel Ángel Vallejo (CADE, 1997)

Barcelona. - Robert Nieuwenhuis; José Miguel Rivero; Miguel Ángel Vallejo (J. Autom. Reason., 1997)

Paramodulation with Built-in AC-Theories and Symbolic Constraints. - Robert Nieuwenhuis; Albert Rubio (J. Symb. Comput., 1997)

Decision Problems in Ordered Rewriting. - Hubert Comon; Paliath Narendran; Robert Nieuwenhuis; Michaël Rusinowitch (LICS, 1998)

Decidability and Complexity Analysis by Basic Paramodulation. - Robert Nieuwenhuis (Inf. Comput., 1998)

Invited Talk: Rewrite-based Deduction and Symbolic Constraints. - Robert Nieuwenhuis (CADE, 1999)

Constraints and Theorem Proving. - Harald Ganzinger; Robert Nieuwenhuis (CCL, 1999)

Paramodulation with Non-Monotonic Orderings. - Miquel Bofill; Guillem Godoy; Robert Nieuwenhuis; Albert Rubio (LICS, 1999)

Solved Forms for Path Ordering Constraints. - Robert Nieuwenhuis; José Miguel Rivero (RTA, 1999)

Modular Redundancy for Theorem Proving. - Miquel Bofill; Guillem Godoy; Robert Nieuwenhuis; Albert Rubio (FroCoS, 2000)

Paramodulation with Built-in Abelian Groups. - Guillem Godoy; Robert Nieuwenhuis (LICS, 2000)

Induction=I-Axiomatization+First-Order Consistency. - Hubert Comon; Robert Nieuwenhuis (Inf. Comput., 2000)

Paramodulation-Based Theorem Proving. - Robert Nieuwenhuis; Albert Rubio (Handbook of Automated Reasoning, 2001)

Context Trees. - Harald Ganzinger; Robert Nieuwenhuis; Pilar Nivela (IJCAR, 2001)

On the Evaluation of Indexing Techniques for Theorem Proving. - Robert Nieuwenhuis; Thomas Hillenbrand; Alexandre Riazanov; Andrei Voronkov (IJCAR, 2001)

The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time. - Hubert Comon; Guillem Godoy; Robert Nieuwenhuis (FOCS, 2001)

On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. - Guillem Godoy; Robert Nieuwenhuis (LICS, 2001)

The impact of CASC in the development of automated deduction systems. - Robert Nieuwenhuis (AI Commun., 2002)

Practical Algorithms for Deciding Path Ordering Constraint Satisfaction. - Robert Nieuwenhuis; José Miguel Rivero (Inf. Comput., 2002)

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

Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. - Miquel Bofill; Guillem Godoy; Robert Nieuwenhuis; Albert Rubio (J. Autom. Reason., 2003)

Stratified resolution. - Anatoli Degtyarev; Robert Nieuwenhuis; Andrei Voronkov (J. Symb. Comput., 2003)

Deciding the confluence of ordered term rewrite systems. - Hubert Comon; Paliath Narendran; Robert Nieuwenhuis; Michaël Rusinowitch (ACM Trans. Comput. Log., 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)

Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups. - Guillem Godoy; Robert Nieuwenhuis (Constraints An Int. J., 2004)

Fast Term Indexing with Coded Context Trees. - Harald Ganzinger; Robert Nieuwenhuis; Pilar Nivela (J. Autom. Reason., 2004)

Superposition with completely built-in Abelian groups. - Guillem Godoy; Robert Nieuwenhuis (J. Symb. Comput., 2004)

Classes of term rewrite systems with polynomial confluence problems. - Guillem Godoy; Robert Nieuwenhuis; Ashish Tiwari 001 (ACM Trans. Comput. Log., 2004)

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

05431 Executive Summary - Deduction and Applications. - Franz Baader; Peter Baumgartner 001; Robert Nieuwenhuis; Andrei Voronkov (Deduction and Applications, 2005)

05431 Abstracts Collection - Deduction and Applications. - Franz Baader; Peter Baumgartner 001; Robert Nieuwenhuis; Andrei Voronkov (Deduction and Applications, 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)

07401 Executive Summary – Deduction and Decision Procedures. - Franz Baader; Byron Cook; Jürgen Giesl; Robert Nieuwenhuis (Deduction and Decision Procedures, 2007)

07401 Abstracts Collection – Deduction and Decision Procedures. - Franz Baader; Byron Cook; Jürgen Giesl; Robert Nieuwenhuis (Deduction and Decision Procedures, 2007)

Challenges in Satisfiability Modulo Theories. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Albert Rubio (RTA, 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)

The Max-Atom Problem and Its Relevance. - Marc Bezem; Robert Nieuwenhuis; 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)

Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra. - Marc Bezem; Robert Nieuwenhuis; Enric Rodríguez-Carbonell (Discret. Appl. Math., 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)

SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms. - Robert Nieuwenhuis (SAT, 2009)

SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering. - Robert Nieuwenhuis (CP, 2010)

10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. - Nikolaj S. Bjørner; Robert Nieuwenhuis; Helmut Veith; Andrei Voronkov (Decision Procedures in Software, Hardware and Bioware, 2010)

10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. - Nikolaj S. Bjørner; Robert Nieuwenhuis; Helmut Veith; Andrei Voronkov (Decision Procedures in Software, Hardware and Bioware, 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)

Hard problems in max-algebra, control theory, hypergraphs and other areas. - Marc Bezem; Robert Nieuwenhuis; Enric Rodríguez-Carbonell (Inf. Process. Lett., 2010)

Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One. - Ignasi Abío; Morgan Deters; Robert Nieuwenhuis; Peter J. Stuckey (SAT, 2011)

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)

Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). - Nikolaj S. Bjørner; Robert Nieuwenhuis; Helmut Veith; Andrei Voronkov (Dagstuhl Reports, 2011)

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

SAT and SMT Are Still Resolution: Questions and Challenges. - Robert Nieuwenhuis (IJCAR, 2012)

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)

Harald Ganzinger's Legacy: Contributions to Logics and Programming. - Deepak Kapur; Robert Nieuwenhuis; Andrei Voronkov; Christoph Weidenbach; Reinhard Wilhelm (Programming Logics, 2013)

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)

The IntSat Method for Integer Linear Programming. - Robert Nieuwenhuis (CP, 2014)

Curriculum-based course timetabling with SAT and MaxSAT. - Roberto Javier Asín Achá; Robert Nieuwenhuis (Ann. Oper. Res., 2014)

SAT-Based Techniques for Integer Linear Constraints. - Robert Nieuwenhuis (GCAI, 2015)

Improving IntSat by expressing disjunctions of bounds as linear constraints. - Roberto Asín; Marc Bezem; Robert Nieuwenhuis (AI Commun., 2016)

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)

Speeding up Pseudo-Boolean Propagation. - Robert Nieuwenhuis; Albert Oliveras; Enric Rodríguez-Carbonell; Rui Zhao (SAT, 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)