default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDRobert Nieuwenhuis
Person information
- affiliation: Polytechnic University of Catalonia, Barcelona, Spain
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
[j30]Robert Nieuwenhuis
, Albert Oliveras, Enric Rodríguez-Carbonell:
IntSat: integer linear programming by conflict-driven constraint learning. Optim. Methods Softw. 39(1): 169-196 (2024)- [c54]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao:
Speeding up Pseudo-Boolean Propagation. SAT 2024: 22:1-22:18 - [i9]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning. CoRR abs/2402.15522 (2024) - 2021
- [j29]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
A Heuristic Approach to the Design of Optimal Cross-Docking Boxes. IEEE Access 9: 122578-122588 (2021) - [j28]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Emma Rollon:
Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving. IEEE Access 9: 142095-142104 (2021) - 2020
- [c53]Robert Nieuwenhuis, Adrià Lozano, Albert Oliveras, Enric Rodríguez-Carbonell:
Decision levels are stable: towards better SAT heuristics. LPAR 2020: 1-11
2010 – 2019
- 2016
- [j27]Roberto Asín, Marc Bezem, Robert Nieuwenhuis:
Improving IntSat by expressing disjunctions of bounds as linear constraints. AI Commun. 29(1): 205-209 (2016) - 2015
- [c52]Robert Nieuwenhuis:
SAT-Based Techniques for Integer Linear Constraints. GCAI 2015: 1-13 - 2014
- [j26]Roberto Javier Asín Achá, Robert Nieuwenhuis:
Curriculum-based course timetabling with SAT and MaxSAT. Ann. Oper. Res. 218(1): 71-91 (2014) - [c51]Robert Nieuwenhuis:
The IntSat Method for Integer Linear Programming. CP 2014: 574-589 - [i8]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Valentin Mayer-Eichberger:
A New Look at BDDs for Pseudo-Boolean Constraints. CoRR abs/1401.5860 (2014) - 2013
- [c50]Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm:
Harald Ganzinger's Legacy: Contributions to Logics and Programming. Programming Logics 2013: 1-18 - [c49]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. CP 2013: 80-96 - [c48]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: 97-106 - 2012
- [j25]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: 443-480 (2012) - [c47]Robert Nieuwenhuis:
SAT and SMT Are Still Resolution: Questions and Challenges. IJCAR 2012: 10-13 - 2011
- [j24]Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
Cardinality Networks: a theoretical and empirical study. Constraints An Int. J. 16(2): 195-221 (2011) - [j23]Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
A Framework for Certified Boolean Branch-and-Bound Optimization. J. Autom. Reason. 46(1): 81-102 (2011) - [c46]Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
BDDs for Pseudo-Boolean Constraints - Revisited. SAT 2011: 61-75 - [c45]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: 273-286 - [i7]Nikolaj S. 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): 23-35 (2011) - 2010
- [j22]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): 145-157 (2010) - [j21]Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell:
Hard problems in max-algebra, control theory, hypergraphs and other areas. Inf. Process. Lett. 110(4): 133-138 (2010) - [c44]Robert Nieuwenhuis:
SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering. CP 2010: 1-2 - [e7]Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov:
Decision Procedures in Software, Hardware and Bioware, 18.04. - 23.04.2010. Dagstuhl Seminar Proceedings 10161, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Germany 2010 [contents] - [i6]Nikolaj S. 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 - [i5]Nikolaj S. 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
2000 – 2009
- 2009
- [c43]Robert Nieuwenhuis:
SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms. SAT 2009: 1 - [c42]Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
Cardinality Networks and Their Applications. SAT 2009: 167-180 - [c41]Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. SAT 2009: 453-466 - 2008
- [j20]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): 3506-3509 (2008) - [c40]Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
The Barcelogic SMT Solver. CAV 2008: 294-298 - [c39]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: 1-8 - [c38]Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
Efficient Generation of Unsatisfiability Proofs and Cores in SAT. LPAR 2008: 16-30 - [c37]Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell:
The Max-Atom Problem and Its Relevance. LPAR 2008: 47-61 - [c36]Germain Faure, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell:
SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. SAT 2008: 77-90 - 2007
- [j19]Robert Nieuwenhuis, Albert Oliveras:
Fast congruence closure and extensions. Inf. Comput. 205(4): 557-580 (2007) - [c35]Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio:
Challenges in Satisfiability Modulo Theories. RTA 2007: 2-18 - [e6]Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis:
Deduction and Decision Procedures, 30.09. - 05.10.2007. Dagstuhl Seminar Proceedings 07401, Internationales Begegnungs- und Forschungszentrum fuer Informatik (IBFI), Schloss Dagstuhl, Germany 2007 [contents] - [i4]Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis:
07401 Executive Summary -- Deduction and Decision Procedures. Deduction and Decision Procedures 2007 - [i3]Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis:
07401 Abstracts Collection -- Deduction and Decision Procedures. Deduction and Decision Procedures 2007 - 2006
- [j18]Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). J. ACM 53(6): 937-977 (2006) - [c34]Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras:
SMT Techniques for Fast Predicate Abstraction. CAV 2006: 424-437 - [c33]Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Splitting on Demand in SAT Modulo Theories. LPAR 2006: 512-526 - [c32]Robert Nieuwenhuis, Albert Oliveras:
On SAT Modulo Theories and Optimization Problems. SAT 2006: 156-169 - [e5]Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov:
Deduction and Applications, 23.-28. October 2005. Dagstuhl Seminar Proceedings 05431, Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany 2006 [contents] - 2005
- [c31]Robert Nieuwenhuis, Albert Oliveras:
DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. CAV 2005: 321-334 - [c30]Robert Nieuwenhuis, Albert Oliveras:
Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. LPAR 2005: 23-46 - [c29]Robert Nieuwenhuis, Albert Oliveras:
Proof-Producing Congruence Closure. RTA 2005: 453-468 - [e4]Robert Nieuwenhuis:
Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings. Lecture Notes in Computer Science 3632, Springer 2005, ISBN 3-540-28005-7 [contents] - [i2]Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov:
05431 Executive Summary - Deduction and Applications. Deduction and Applications 2005 - [i1]Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov:
05431 Abstracts Collection - Deduction and Applications. Deduction and Applications 2005 - 2004
- [j17]Guillem Godoy, Robert Nieuwenhuis:
Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups. Constraints An Int. J. 9(3): 167-192 (2004) - [j16]Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela:
Fast Term Indexing with Coded Context Trees. J. Autom. Reason. 32(2): 103-120 (2004) - [j15]Guillem Godoy, Robert Nieuwenhuis:
Superposition with completely built-in Abelian groups. J. Symb. Comput. 37(1): 1-33 (2004) - [j14]Guillem Godoy, Robert Nieuwenhuis, Ashish Tiwari:
Classes of term rewrite systems with polynomial confluence problems. ACM Trans. Comput. Log. 5(2): 321-331 (2004) - [c28]Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
DPLL( T): Fast Decision Procedures. CAV 2004: 175-188 - [c27]Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli:
Abstract DPLL and Abstract DPLL Modulo Theories. LPAR 2004: 36-50 - 2003
- [j13]Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio:
Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. J. Autom. Reason. 30(1): 99-120 (2003) - [j12]Anatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov:
Stratified resolution. J. Symb. Comput. 36(1-2): 79-99 (2003) - [j11]Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch:
Deciding the confluence of ordered term rewrite systems. ACM Trans. Comput. Log. 4(1): 33-55 (2003) - [c26]Robert Nieuwenhuis, Albert Oliveras:
Congruence Closure with Integer Offsets. LPAR 2003: 78-90 - [e3]Robert Nieuwenhuis:
Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings. Lecture Notes in Computer Science 2706, Springer 2003, ISBN 3-540-40254-3 [contents] - 2002
- [j10]Robert Nieuwenhuis:
The impact of CASC in the development of automated deduction systems. AI Commun. 15(2-3): 77-78 (2002) - [j9]Robert Nieuwenhuis, José Miguel Rivero:
Practical Algorithms for Deciding Path Ordering Constraint Satisfaction. Inf. Comput. 178(2): 422-440 (2002) - 2001
- [c25]Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela:
Context Trees. IJCAR 2001: 242-256 - [c24]Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov:
On the Evaluation of Indexing Techniques for Theorem Proving. IJCAR 2001: 257-271 - [c23]Hubert Comon, Guillem Godoy, Robert Nieuwenhuis:
The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time. FOCS 2001: 298-307 - [c22]Guillem Godoy, Robert Nieuwenhuis:
On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. LICS 2001: 38-47 - [p1]Robert Nieuwenhuis, Albert Rubio:
Paramodulation-Based Theorem Proving. Handbook of Automated Reasoning 2001: 371-443 - [e2]Robert Nieuwenhuis, Andrei Voronkov:
Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings. Lecture Notes in Computer Science 2250, Springer 2001, ISBN 3-540-42957-3 [contents] - 2000
- [j8]Hubert Comon, Robert Nieuwenhuis:
Induction=I-Axiomatization+First-Order Consistency. Inf. Comput. 159(1-2): 151-186 (2000) - [c21]Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio:
Modular Redundancy for Theorem Proving. FroCoS 2000: 186-199 - [c20]Guillem Godoy, Robert Nieuwenhuis:
Paramodulation with Built-in Abelian Groups. LICS 2000: 413-424
1990 – 1999
- 1999
- [c19]Robert Nieuwenhuis:
Invited Talk: Rewrite-based Deduction and Symbolic Constraints. CADE 1999: 302-313 - [c18]Harald Ganzinger, Robert Nieuwenhuis:
Constraints and Theorem Proving. CCL 1999: 159-201 - [c17]Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio:
Paramodulation with Non-Monotonic Orderings. LICS 1999: 225-233 - [c16]Robert Nieuwenhuis, José Miguel Rivero:
Solved Forms for Path Ordering Constraints. RTA 1999: 1-15 - 1998
- [j7]Robert Nieuwenhuis:
Decidability and Complexity Analysis by Basic Paramodulation. Inf. Comput. 147(1): 1-21 (1998) - [c15]Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch:
Decision Problems in Ordered Rewriting. LICS 1998: 276-286 - 1997
- [j6]Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo:
Barcelona. J. Autom. Reason. 18(2): 171-176 (1997) - [j5]Robert Nieuwenhuis, Albert Rubio:
Paramodulation with Built-in AC-Theories and Symbolic Constraints. J. Symb. Comput. 23(1): 1-21 (1997) - [c14]Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo:
Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. CADE 1997: 49-52 - 1996
- [c13]Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo:
An Implementation Kernel for Theorem Proving with Equality Clauses. APPIA-GULP-PRODE 1996: 89-104 - [c12]Robert Nieuwenhuis:
Basic Paramodulation and Decidable Theories (Extended Abstract). LICS 1996: 473-482 - 1995
- [j4]Robert Nieuwenhuis, Albert Rubio:
Theorem Proving with Ordering and Equality Constrained Clauses. J. Symb. Comput. 19(4): 321-351 (1995) - [j3]Albert Rubio, Robert Nieuwenhuis:
A Total AC-Compatible Ordering Based on RPO. Theor. Comput. Sci. 142(2): 209-227 (1995) - [c11]Hubert Comon, Robert Nieuwenhuis, Albert Rubio:
Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract). LICS 1995: 375-385 - [c10]Robert Nieuwenhuis:
On Narrowing, Refutation Proofs and Constraints. RTA 1995: 56-70 - [e1]Robert Nieuwenhuis, Albert Rubio:
9th International Workshop on Unification, UNIF 1995, Sitges, Spain, April 2-3, 1995. 1995 [contents] - 1994
- [c9]Robert Nieuwenhuis, Albert Rubio:
AC-Superposition with Constraints: No AC-Unifiers Needed. CADE 1994: 545-559 - 1993
- [j2]Robert Nieuwenhuis:
Simple LPO Constraint Solving Methods. Inf. Process. Lett. 47(2): 65-69 (1993) - [c8]Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas:
Program Development: Completion Subsystem. PROSPECTRA Book 1993: 460-494 - [c7]Albert Rubio, Robert Nieuwenhuis:
A Precedence-Based Total AC-Compatible Ordering. RTA 1993: 374-388 - [c6]Pilar Nivela, Robert Nieuwenhuis:
Saturation of First-Order (Constrained) Clauses with the Saturate System. RTA 1993: 436-440 - 1992
- [c5]Robert Nieuwenhuis, Albert Rubio:
Theorem Proving with Ordering Constrained Clauses. CADE 1992: 477-491 - [c4]Robert Nieuwenhuis, Albert Rubio:
Basic Superposition is Complete. ESOP 1992: 371-389 - 1991
- [j1]Robert Nieuwenhuis, Pilar Nivela:
Efficient Deduction in Equality Horn Logic by Horn-Completion. Inf. Process. Lett. 39(1): 1-6 (1991) - 1990
- [c3]Robert Nieuwenhuis, Fernando Orejas:
Clausal Rewriting: Applications and Implementation. ADT 1990: 204-219 - [c2]Robert Nieuwenhuis, Fernando Orejas, Albert Rubio:
TRIP: An Implementation of Clausal Rewriting. CADE 1990: 667-668 - [c1]Robert Nieuwenhuis, Fernando Orejas:
Clausal Rewriting. CTRS 1990: 246-258
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-22 19:48 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
