Robert Nieuwenhuis. Main publications

Robert Nieuwenhuis' main publications

2024

R. Nieuwenhuis, A. Oliveras, and E. Rodríguez-Carbonell
IntSat: integer linear programming by conflict-driven constraint learning. .
Journal: Optim. Methods Softw. 39(1): 169-196 (2024)
Paper

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao:
Speeding up Pseudo-Boolean Propagation. .
Int. Conf. on Theory and Applications of Satisfiability Testing (SAT),
Paper

2021

R. Nieuwenhuis, A. Oliveras, E. Rodríguez-Carbonell, and E. Rollón
Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving .
Journal: IEEE Access Vol 9, pp 142095-142104, Print ISSN: 2169-3536
doi: 10.1109/ACCESS.2021.3120597.
Paper

R. Nieuwenhuis, A. Oliveras, and E. Rodríguez-Carbonell
A Heuristic Approach to the Design of Optimal Cross-Docking Boxes .
Journal: IEEE Access Vol 9, pp 122578 - 122588, Print ISSN: 2169-3536
doi: 10.1109/ACCESS.2021.3109976.
Paper

2020

R. Nieuwenhuis, A. Lozano, A. Oliveras, and E. Rodríguez-Carbonell
Decision levels are stable: towards better SAT heuristics.
23rd Int. Conf. Logic for Programming, Artif. Intell. and Reasoning (LPAR)
EPiC Series in Computing, E. Albert and L. Kovacs, Eds., vol. 73. EasyChair, 2020, pp. 1-11.
Paper

2016

Marc Bezem and Robert Nieuwenhuis
Completeness of Cutting Planes Revisited.
In: J. van Eijck, R. Iemhoff and J. Joosten (editors)
Liber Amicorum Alberti
College Publications, ISBN 9781848902046, pp. 37-46, 2016.
paper

Roberto Asín, Marc Bezem and Robert Nieuwenhuis
Improving IntSat by expressing disjunctions of bounds as linear constraints. .
Journal: AI Communications, vol. 29, no. 1, pp. 205-209, 2016
Paper © IOS Press.

2015

Robert Nieuwenhuis
SAT-Based Techniques for Integer Linear Constraints.
EasyChair Proceedings in Computing Vol 36, Pages 1-13, 2015.
Paper .

2014

Roberto Asín, Robert Nieuwenhuis
Curriculum-based course timetabling with SAT and Max-SAT .
Annals of Operations Research 218(1): 71-91 (2014)
Paper © Springer

Robert Nieuwenhuis
The IntSat Method for Integer LInear Programming. .
Int. Conf. Principles and Practice of Constraint Programming CP 2014: 574-589.
Paper © Springer Verlag.

2013

Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm
Harald Ganzinger's Legacy: Contributions to Logics and Programming.
Programming Logics - Essays in Memory of Harald Ganzinger 1-18, Springer LNCS 7797, 2013.
Paper © Springer Verlag.

Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. .
Int. Conf. Principles and Practice of Constraint Programming CP 2013: 80-96.
Paper © Springer Verlag.

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. .
Int. Conf. Principles and Practice of Constraint Programming CP 2013: 97-106.
Paper © Springer Verlag.

2012

Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Valentin Mayer-Eichberger
A New Look at BDDs for Pseudo-Boolean Constraints.
Journal of Artificial Intelligence Research (JAIR; ISSN 1076 - 9757) Volume 45, pages 443-480, November 2012.
Paper © AAAI Press.

Robert Nieuwenhuis
SAT and SMT Are Still Resolution: Questions and Challenges (invited paper).
Int. Joint Conf. On Automated Reasoning (IJCAR), 2012: pages 10-13
Paper © Springer

2011

Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Cardinality Networks: a Theoretical and Empirical Study .
Constraints Journal, 16(2): 195-221.
Paper © Springer

Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
A framework for Certified Boolean Branch-and-Bound Optimization .
Journal of Automated Reasoning 46(1):81-102.
www.springerlink.com/content/y431p584k0p66w44
Paper © Springer

Ignasi Abío, Morgan Deters, Robert Nieuwenhuis, Peter J. Stuckey
Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One .
14th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), Ann Arbor, USA, june 2011, pages 273-286
paper (.pdf) © Springer-Verlag

Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
BDDs for Pseudo-Boolean Constraints - Revisited.
14th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), Ann Arbor, USA, june 2011, pages 61-75
paper (.pdf) © Springer-Verlag

2010

Robert Nieuwenhuis:
SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering.
(Invited talk) Int. Conf. Principles and Practice of Constraint Programming CP 2010
paper (.pdf) © Springer-Verlag

Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
Hard problems in max-algebra, control theory, hypergraphs and other areas.
Information Processing Letters 110 (2010) 133-138
paper (.pdf) © Elsevier Science

Roberto Asin, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Practical Algorithms for Unsatisfiability Proof and Core Generation in SAT solvers .
AI Communications 2010;23:145-157.
paper (.pdf) © IOS Press

2009

Robert Asin, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Cardinality Networks and their Applications.
12th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), Swansea, UK, July 2009.
paper (.pdf) © Springer-Verlag

Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates.
12th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), Swansea, UK, July 2009.
paper (.pdf) © Springer-Verlag

2008

Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
The Max-Atom Problem and its Relevance .
15th Int. Conf. Logic for Programming, Artif. Intell. and Reasoning (LPAR), November 2008, Qatar.
paper (.pdf) © Springer-Verlag

Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio
The Barcelogic SMT Solver .
20th International Conference on Computer Aided Verification (CAV)), July 2008, Princeton (USA).
paper (.pdf) © Springer-Verlag

Roberto Asin, Albert Oliveras, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
Efficient Generation of Unsatisfiability Proofs and Cores in SAT .
15th Int. Conf. Logic for Programming, Artif. Intell. and Reasoning (LPAR), November 2008, Qatar.
paper (.pdf) © Springer-Verlag

Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio
A Write-Based Solver for SAT Modulo the Theory of Arrays .
Formal Methods in Computer-Aided Design 2008 (FMCAD), November 2008, Portland (USA).
paper (.pdf)

Germain Faure, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers.
11th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), Guangzhou, China, May 2008.
paper (.pdf) © Springer-Verlag

Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra.
Discrete Applied Mathematics 156 (18) 3506--3509, November 2008.
paper (.pdf) © Elsevier Science

2007

Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell and Albert Rubio
Challenges in Satisfiability Modulo Theories (invited paper).
18th International Conference on Rewriting Techniques and Applications (RTA)
June 2007, Paris, France. Springer LNCS 4533, pp 2-18.
paper (.pdf) © Springer-Verlag

Robert Nieuwenhuis and Albert Oliveras
Fast Congruence Closure and Extensions .
Information and Computation, 205(4):557-580, April 2007.
paper (.pdf) © Elsevier Science

2006

Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli
Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T).
Journal of the ACM, 53(6), 937-977, November 2006.
paper (.pdf) © ACM Press

Robert Nieuwenhuis and Albert Oliveras
On SAT Modulo Theories and Optimization Problems..
9th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT), August 2006, Seattle.
paper (.pdf) © Springer-Verlag

Shuvendu Lahiri, Robert Nieuwenhuis and Albert Oliveras
SMT Techniques for Predicate Abstraction.
18th International Conference on Computer Aided Verification (CAV), August 2006, Seattle.
paper (.pdf) © Springer-Verlag

Clark Barrett, Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli
Splitting on Demand in Satisfiability Modulo Theories.
13th Int. Conf. Logic for Programming, Artif. Intell. and Reasoning (LPAR), November 2006, Phnom Penh.
paper (.pdf) © Springer-Verlag

2005

Robert Nieuwenhuis and Albert Oliveras
Decision procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. (Invited Paper).
12th Int. Conf. Logic for Programming, Artif. Intell. and Reasoning (LPAR), December 2005, Jamaica.
paper (.ps.gz) © Springer-Verlag

Robert Nieuwenhuis (Ed.)
Automated Deduction- CADE-20
Proceedings of the 20th International Conference (CADE 2005).
Volume 3632 of Lecture Notes in Computer Science. © Springer-Verlag.

Robert Nieuwenhuis and Albert Oliveras
DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic.
17th International Conference on Computer Aided Verification (CAV), July 2005, Edinburgh.
paper (.pdf) © Springer-Verlag

Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli
Abstract DPLL and Abstract DPLL Modulo Theories.
11th Int. Conf. on Logics for Programming, AI and Reasoning (LPAR)
Montevideo, March 2005. Springer LNAI 3452, pp 36-50.
paper (.pdf) © Springer-Verlag

Robert Nieuwenhuis and Albert Oliveras.
Proof-Producing Congruence closure.
16th International Conference on Rewriting Techniques and Applications (RTA)
April 19 - 21, 2005 Nara, Japan. Springer LNCS 3467, pp 453-468.
paper (.pdf) © Springer-Verlag

2004

Harald Ganzinger, Robert Nieuwenhuis and Pilar Nivela
Fast Term Indexing with Coded Context Trees
Journal of Automated Reasoning, 32 (2): 103-120, February 2004.
Paper © Kluwer

Guillem Godoy and Robert Nieuwenhuis
Constraint Solving for Orderings Compatible with Abelian Semigroups, Monoids and Groups
Constraints 9(3), 167-192, July 2004.
Paper © Kluwer

Guillem Godoy and Robert Nieuwenhuis
Superposition with Completely Built-in Abelian Groups
Journal of Symbolic Computation. 37(1), January 2004, 1-33.
Paper © Elsevier Science

Guillem Godoy, Robert Nieuwenhuis and Ashish Tiwari
Classes of Term Rewrite Systems with Polynomial Confluence Problems
ACM Transactions on Computational Logic (TOCL). 5(2), April 2004
Paper © ACM

Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli
DPLL(T): Fast Decision Procedures
16th International Conference on Computer Aided Verification (CAV), July 2004, Boston (USA).
[ Paper © Springer-Verlag | Detailed experimental results ]

2003

Anatoli Degtyarev, Robert Nieuwenhuis and Andrei Voronkov
Stratified Resolution
Journal of Symbolic Computation (JSC) 36(1-2):77-99, July-August 2003.
Paper © Elsevier Science

Robert Nieuwenhuis and Albert Oliveras.
Congruence closure with integer offsets.
10th Int. Conf. on Logics for Programming, AI and Reasoning (LPAR), Sept. 2003
paper (.ps) © Springer-Verlag

Hubert Comon, Paliath Narendran, Robert Nieuwenhuis and Michael Rusinowitch.
Deciding the Confluence of Ordered Rewriting.
ACM Transactions on Computational Logic (TOCL) 4(1), January 2003.
Paper © ACM

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings.
Journal of Automated Reasoning 30(1), 99-120, Jan 2003.
Paper © Kluwer.

Robert Nieuwenhuis (Ed.)
Rewriting Techniques and Applications
Proceedings of the 14th International Conference (RTA 2003).
Volume 2706 of Lecture Notes in Computer Science, ISBN 3-540-40254-3. © Springer-Verlag.

2002

Robert Nieuwenhuis and Jose Miguel Rivero
Practical Algorithms for Deciding Path Ordering Constraint Satisfaction.
Information and Computation. 178(2):422-440,2002.
Paper © Academic Press

Robert Nieuwenhuis
The impact of CASC in the development of automated deduction systems .
(Guest editoral) AI Communications 15(2-3), 2002.
Paper at IOS Press © IOS Press

Robert Nieuwenhuis (Ed.)
Procs. 2002 Workshop on the Implementation of Logics.
October 2002, Tbilisi, Georgia.
Electronic version of the proceedings.

2001

Guillem Godoy and Robert Nieuwenhuis
On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups
Procs. 16th Annual IEEE Symposium on Logic in Computer Science (LICS)
Boston, USA, 2001.
Long paper © IEEE and Slides

Harald Ganzinger, Robert Nieuwenhuis and Pilar Nivela
Context Trees
Int. Joint Conf. On Automated Reasoning (IJCAR), Siena, Italy, 2001.
Paper © Springer-Verlag

Robert Nieuwenhuis, Thomas Hillenbrand, Alexander Riazanov and Andrei Voronkov
On the Evaluation of Indexing Techniques for Theorem Proving
Int. Joint Conf. On Automated Reasoning (IJCAR), Siena, Italy, 2001.
Paper © Springer-Verlag

Hubert Comon, Guillem Godoy and Robert Nieuwenhuis
The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time
42nd Annual IEEE Symposium on Foundations of Computer Science (FOCS)
Las Vegas, Nevada, USA, 2001.
Paper © IEEE and Slides

Harald Ganzinger and Robert Nieuwenhuis
Constraints and Theorem Proving
Chapter of: Comon, Marche and Treinen, (Eds)
Constraints in Computational Logics: Theory and Applications
Chapter (gzipped postscript, 128KB)
Springer LNCS Vol. 2002, pages 159-201, 2001. © Springer-Verlag

Robert Nieuwenhuis
Recent trends in rewrite-based and paramodulation-based deduction (invited paper)
International Workshop on Rewriting in Proof and Computation (RPC'01)
Sendai, Japan, October 25-27, 2001.
Paper

Robert Nieuwenhuis and Andrei Voronkov (Eds.)
Logics for Programming, AI and Reasoning
Proceedings of the 8th International Conference (LPAR 2001).
Volume 2250 of Lecture Notes in AI, ISBN 3-540-42957-3. © Springer-Verlag.

Robert Nieuwenhuis and Albert Rubio
Paramodulation-Based Theorem Proving.
Chapter of Handbook of Automated Reasoning
Edited by Alan Robinson and Andrei Voronkov.
ISBN 0-444-82949-0. © Elsevier Science and MIT Press, 2001.
Chapter (gzipped postscript, 169KB)

2000

Guillem Godoy and Robert Nieuwenhuis
Paramodulation with Built-In Abelian Groups
Procs. 15th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 413-424,
Santa Barbara, USA, 2000.
Paper © IEEE and Long paper

Hubert Comon and Robert Nieuwenhuis
Induction = I-Axiomatization + First-Order Consistency .
Information and Computation 159(1/2):151-186, May 2000. © Academic Press
Paper

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio
Modular Redundancy for Theorem Proving .
In Procs. FroCoS 2000 © Springer-Verlag
LNCS 1794, pages 186-199, Nancy, France, April, 2000. Springer-Verlag.
Paper

1999

Robert Nieuwenhuis
Rewrite-based Deduction and Symbolic Constraints (Invited Paper) .
In Procs. 16th International Conference on Automated Deduction (CADE) © Springer-Verlag
LNCS/LNAI 1632, pages 302-313, Trento, Italy, July, 1999. Springer-Verlag.
Paper

Robert Nieuwenhuis and Jose Miguel Rivero
Solved Forms for Path Ordering Constraints .
In Procs. 10th International Conference on Rewriting Techniques and Applications (RTA) © Springer-Verlag
LNCS 1631, pages 1-15, Trento, Italy, July, 1999. Springer-Verlag.
Paper. Test software.

Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis and Albert Rubio
Paramodulation with Non-Monotonic Orderings .
In Procs. 14th Annual IEEE Symposium on Logic in Computer Science (LICS)
IEEE Comp. Sc. Press, pages 225-234, Trento, Italy, July, 1999.
Paper

1998

Hubert Comon, Paliath Narendran, Robert Nieuwenhuis and Michael Rusinowitch.
Decision Problems in Ordered Rewriting.
13th Annual IEEE Symposium on Logic in Computer Science (LICS), Indianapolis, USA, 1998.
Paper

Robert Nieuwenhuis.
Decidability and Complexity Analysis by Basic Paramodulation .
Information and Computation, 147:1-21, 1998.
Paper

1997

Robert Nieuwenhuis, Jose Miguel Rivero and Miguel Angel Vallejo.
Dedam: a kernel of data structures and algorithms for automated deduction with equality clauses (System description) .
Springer-Verlag Lecture Notes in Artificial Intelligence 1249. 14th International Conference on Automated Deduction (CADE) © Springer-Verlag Townsville, Australia, July 1997.
Paper

Robert Nieuwenhuis, Jose Miguel Rivero and Miguel Angel Vallejo.
The Barcelona Prover .
Journal of Automated Reasoning , 18:171-176, February 1997.
Paper

Robert Nieuwenhuis and Albert Rubio.
Paramodulation with Built-in AC-Theories and Symblic Constraints .
Journal of Symbolic Computation , 23:1-21, May 1997.
Paper

1996

Robert Nieuwenhuis.
Basic Paramodulation and Decidable Theories .
In 11th Annual IEEE Symposium on Logic in Computer Science (LICS), New Brunswick, NJ, USA, July, 1996.
Paper

1995

Hubert Comon, Robert Nieuwenhuis, and Albert Rubio.
Orderings, AC-Theories and Symbolic Constraint Solving .
In Tenth Annual IEEE Symposium on Logic in Computer Science (LICS) , San Diego, California, USA, June, 1995.
Paper

Albert Rubio and Robert Nieuwenhuis.
A total AC-compatible ordering based on RPO .
Theoretical Computer Science , 142(2):209-227, May 15, 1995.
Paper

Robert Nieuwenhuis.
On Narrowing, Refutation Proofs and Constraints .
In J. Hsiang, editor, 6th International Conference on Rewriting Techniques and Applications (RTA) © Springer-Verlag
LNCS 914, pages 56-70, Kaiserslautern, Germany, April 4-7, 1995. Springer-Verlag.
Paper

Robert Nieuwenhuis and Albert Rubio.
Theorem Proving with Ordering and Equality Constrained Clauses.
Journal of Symbolic Computation , 19(4):321-351, April 1995.
Paper

1994

Robert Nieuwenhuis and Albert Rubio.
AC-Superposition with constraints: No AC-unifiers needed .
In Allan Bundy, editor, 12th International Conference on Automated Deduction © Springer-Verlag , LNAI, Nancy, France, June 1994. Springer-Verlag.
Paper

1993

Robert Nieuwenhuis.
Simple LPO constraint solving methods .
Information Processing Letters , 47:65-69, August 1993.
Paper

Pilar Nivela and Robert Nieuwenhuis.
Practical results on the saturation of full first-order clauses: Experiments with the Saturate system. (System description) .
In C. Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications (RTA) © Springer-Verlag , LNCS 690, Montreal, Canada, June 16-18, 1993. Springer-Verlag.
Paper

Albert Rubio and Robert Nieuwenhuis.
A precedence-based total AC-compatible ordering .
In C. Kirchner, editor, 5th International Conference on Rewriting Techniques and Applications (RTA) © Springer-Verlag , LNCS 690, pages 374-388, Montreal, Canada, June 16-18, 1993.
Paper (longer version)

1992 and before

Robert Nieuwenhuis and Albert Rubio.
Theorem Proving with Ordering Constrained Clauses .
In Deepak Kapur, editor, 11th CADE , LNAI 607, pages 477-491, Saratoga Springs, New York, 1992.

Robert Nieuwenhuis and Albert Rubio.
Basic superposition is complete .
In B. Krieg-Brückner, editor, European Symposium on Programming , LNCS 582, pages 371-390, Rennes, France, February 26-28, 1992. Springer-Verlag.

Robert Nieuwenhuis and Pilar Nivela.
Efficient deduction in equality Horn logic by Horn-completion .
Information Processing Letters , 39(1):1-6, July 1991.

Robert Nieuwenhuis, Fernando Orejas, and Albert Rubio.
TRIP: An Implementation of Clausal Rewriting .
In Mark E. Stickel, editor, 10th International Conference on Automated Deduction , LNAI 449, pages 667-668, Kaiserslautern, FRG, July 24-27, 1990. Springer-Verlag.

Robert Nieuwenhuis and Fernando Orejas.
Clausal Rewriting .
In Stéphane Kaplan and Mitsuhiro Okada, editors, Conditional and Typed Rewriting Systems, 2nd International Workshop , LNCS 516, pages 246-258, Montreal, Canada, June 11-14, 1990. Springer-Verlag.

Robert Nieuwenhuis and Fernando Orejas.
Clausal Rewriting, Applications and Implementation .
In 7th Workshop on Specification of Abstract Data Types , LNCS 534, pages 204-219. Springer-Verlag, 1990.

Robert Nieuwenhuis.
Theorem Proving in first-order logic with equality by clausal rewriting and completion .
PhD thesis, Technical University of Catalonia, Spain, 1990.