Robert Nieuwenhuis

Publication Activity (10 Years)

Years Active: 1990-2024
Publications (10 Years): 8

Top Topics

Integer Linear Programming

Propositional Satisfiability

Stochastic Local Search Algorithms

Top Venues

Ann. Oper. Res.

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)
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)
Roberto Asín, Marc Bezem, Robert Nieuwenhuis
Improving IntSat by expressing disjunctions of bounds as linear constraints. AI Commun. 29 (1) (2016)
Robert Nieuwenhuis
SAT-Based Techniques for Integer Linear Constraints. GCAI (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)
Roberto Javier Asín Achá, Robert Nieuwenhuis
Curriculum-based course timetabling with SAT and MaxSAT. Ann. Oper. Res. 218 (1) (2014)
Robert Nieuwenhuis
The IntSat Method for Integer Linear Programming. CP (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)
Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm
Harald Ganzinger's Legacy: Contributions to Logics and Programming. Programming Logics (2013)
Robert Nieuwenhuis
SAT and SMT Are Still Resolution: Questions and Challenges. IJCAR (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)
Nikolaj Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports 1 (7) (2011)
Ignasi Abío, Morgan Deters, Robert Nieuwenhuis, Peter J. Stuckey
Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One. 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)
Nikolaj Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware (2010)
Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
Hard problems in max-algebra, control theory, hypergraphs and other areas. Inf. Process. Lett. 110 (4) (2010)
Robert Nieuwenhuis
SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering. CP (2010)
Nikolaj Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware (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)
Robert Nieuwenhuis
SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms. SAT (2009)
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)
Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra. Discret. Appl. Math. 156 (18) (2008)
Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
The Max-Atom Problem and Its Relevance. LPAR (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)
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)
Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
07401 Executive Summary -- Deduction and Decision Procedures. Deduction and Decision Procedures (2007)
Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
07401 Abstracts Collection -- Deduction and Decision Procedures. Deduction and Decision Procedures (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)
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
05431 Executive Summary - Deduction and Applications. Deduction and Applications (2005)
Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
05431 Abstracts Collection - Deduction and Applications. Deduction and Applications (2005)
Guillem Godoy, Robert Nieuwenhuis, Ashish Tiwari
Classes of term rewrite systems with polynomial confluence problems. ACM Trans. Comput. Log. 5 (2) (2004)
Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
Fast Term Indexing with Coded Context Trees. J. Autom. Reason. 32 (2) (2004)
Guillem Godoy, Robert Nieuwenhuis
Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups. Constraints An Int. J. 9 (3) (2004)
Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
DPLL( T): Fast Decision Procedures. CAV (2004)
Guillem Godoy, Robert Nieuwenhuis
Superposition with completely built-in Abelian groups. J. Symb. Comput. 37 (1) (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)
Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch
Deciding the confluence of ordered term rewrite systems. ACM Trans. Comput. Log. 4 (1) (2003)
Anatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov
Stratified resolution. J. Symb. Comput. 36 (1-2) (2003)
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. J. Autom. Reason. 30 (1) (2003)
Robert Nieuwenhuis
The impact of CASC in the development of automated deduction systems. AI Commun. 15 (2-3) (2002)
Robert Nieuwenhuis, José Miguel Rivero
Practical Algorithms for Deciding Path Ordering Constraint Satisfaction. Inf. Comput. 178 (2) (2002)
Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov
On the Evaluation of Indexing Techniques for Theorem Proving. IJCAR (2001)
Guillem Godoy, Robert Nieuwenhuis
On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. LICS (2001)
Hubert Comon, Guillem Godoy, Robert Nieuwenhuis
The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time. FOCS (2001)
Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
Context Trees. IJCAR (2001)
Guillem Godoy, Robert Nieuwenhuis
Paramodulation with Built-in Abelian Groups. LICS (2000)
Hubert Comon, Robert Nieuwenhuis
Induction=I-Axiomatization+First-Order Consistency. Inf. Comput. 159 (1-2) (2000)
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
Modular Redundancy for Theorem Proving. FroCoS (2000)
Robert Nieuwenhuis
Invited Talk: Rewrite-based Deduction and Symbolic Constraints. CADE (1999)
Harald Ganzinger, Robert Nieuwenhuis
Constraints and Theorem Proving. CCL (1999)
Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
Paramodulation with Non-Monotonic Orderings. LICS (1999)
Robert Nieuwenhuis, José Miguel Rivero
Solved Forms for Path Ordering Constraints. RTA (1999)
Robert Nieuwenhuis
Decidability and Complexity Analysis by Basic Paramodulation. Inf. Comput. 147 (1) (1998)
Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch
Decision Problems in Ordered Rewriting. LICS (1998)
Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo
Barcelona. J. Autom. Reason. 18 (2) (1997)
Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo
Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. CADE (1997)
Robert Nieuwenhuis, Albert Rubio
Paramodulation with Built-in AC-Theories and Symbolic Constraints. J. Symb. Comput. 23 (1) (1997)
Robert Nieuwenhuis
Basic Paramodulation and Decidable Theories (Extended Abstract). LICS (1996)
Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo
An Implementation Kernel for Theorem Proving with Equality Clauses. APPIA-GULP-PRODE (1996)
Albert Rubio, Robert Nieuwenhuis
A Total AC-Compatible Ordering Based on RPO. Theor. Comput. Sci. 142 (2) (1995)
Robert Nieuwenhuis, Albert Rubio
Theorem Proving with Ordering and Equality Constrained Clauses. J. Symb. Comput. 19 (4) (1995)
Hubert Comon, Robert Nieuwenhuis, Albert Rubio
Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) LICS (1995)
Robert Nieuwenhuis
On Narrowing, Refutation Proofs and Constraints. RTA (1995)
Robert Nieuwenhuis, Albert Rubio
AC-Superposition with Constraints: No AC-Unifiers Needed. CADE (1994)
Robert Nieuwenhuis
Simple LPO Constraint Solving Methods. Inf. Process. Lett. 47 (2) (1993)
Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas
Program Development: Completion Subsystem. PROSPECTRA Book (1993)
Albert Rubio, Robert Nieuwenhuis
A Precedence-Based Total AC-Compatible Ordering. RTA (1993)
Pilar Nivela, Robert Nieuwenhuis
System. RTA (1993)
Robert Nieuwenhuis, Albert Rubio
Basic Superposition is Complete. ESOP (1992)
Robert Nieuwenhuis, Albert Rubio
Theorem Proving with Ordering Constrained Clauses. CADE (1992)
Robert Nieuwenhuis, Pilar Nivela
Efficient Deduction in Equality Horn Logic by Horn-Completion. Inf. Process. Lett. 39 (1) (1991)
Robert Nieuwenhuis, Fernando Orejas
Clausal Rewriting: Applications and Implementation. ADT (1990)
Robert Nieuwenhuis, Fernando Orejas, Albert Rubio
TRIP: An Implementation of Clausal Rewriting. CADE (1990)
Robert Nieuwenhuis, Fernando Orejas
Clausal Rewriting. CTRS (1990)