Robert Nieuwenhuis

103 papers A* 11A 23B 9Journal 34Unranked 20

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Using execution logs for improving Pseudo-Boolean propagation. Artif. Intell. Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao
2025	A	`conf`	Symbolic Conflict Analysis in Pseudo-Boolean Optimization. SAT Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao
2024	J	`jnl`	IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning. CoRR Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2024	J	`jnl`	IntSat: integer linear programming by conflict-driven constraint learning. Optim. Methods Softw. Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2024	A	`conf`	Speeding up Pseudo-Boolean Propagation. SAT Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Rui Zhao
2021	J	`jnl`	A Heuristic Approach to the Design of Optimal Cross-Docking Boxes. IEEE Access Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2021	J	`jnl`	Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving. IEEE Access Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Emma Rollon
2020	B	`conf`	Decision levels are stable: towards better SAT heuristics. LPAR Robert Nieuwenhuis, Adrià Lozano, Albert Oliveras, Enric Rodríguez-Carbonell
2016	J	`jnl`	Improving IntSat by expressing disjunctions of bounds as linear constraints. AI Commun. Roberto Asín, Marc Bezem, Robert Nieuwenhuis
2015	—	`conf`	SAT-Based Techniques for Integer Linear Constraints. GCAI Robert Nieuwenhuis
2014	J	`jnl`	A New Look at BDDs for Pseudo-Boolean Constraints. CoRR Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Valentin Mayer-Eichberger
2014	J	`jnl`	Curriculum-based course timetabling with SAT and MaxSAT. Ann. Oper. Res. Roberto Javier Asín Achá, Robert Nieuwenhuis
2014	A	`conf`	The IntSat Method for Integer Linear Programming. CP Robert Nieuwenhuis
2013	A	`conf`	A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints. CP Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2013	—	`conf`	Harald Ganzinger's Legacy: Contributions to Logics and Programming. Programming Logics Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, Reinhard Wilhelm
2013	A	`conf`	To Encode or to Propagate? The Best Choice for Each Constraint in SAT. CP Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Peter J. Stuckey
2012	J	`jnl`	A New Look at BDDs for Pseudo-Boolean Constraints. J. Artif. Intell. Res. Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Valentin Mayer-Eichberger
2012	A	`conf`	SAT and SMT Are Still Resolution: Questions and Challenges. IJCAR Robert Nieuwenhuis
2011	J	`jnl`	A Framework for Certified Boolean Branch-and-Bound Optimization. J. Autom. Reason. Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2011	A	`conf`	BDDs for Pseudo-Boolean Constraints - Revisited. SAT Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2011	J	`jnl`	Cardinality Networks: a theoretical and empirical study. Constraints An Int. J. Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2011	J	`jnl`	Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272). Dagstuhl Reports Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2011	A	`conf`	Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One. SAT Ignasi Abío, Morgan Deters, Robert Nieuwenhuis, Peter J. Stuckey
2010	—	`conf`	10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2010	—	`conf`	10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware. Decision Procedures in Software, Hardware and Bioware Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2010	—	`ed.`	Decision Procedures in Software, Hardware and Bioware, 18.04. - 23.04.2010 Decision Procedures in Software, Hardware and Bioware Nikolaj S. Bjørner, Robert Nieuwenhuis, Helmut Veith, Andrei Voronkov
2010	J	`jnl`	Hard problems in max-algebra, control theory, hypergraphs and other areas. Inf. Process. Lett. Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
2010	J	`jnl`	Practical algorithms for unsatisfiability proof and core generation in SAT solvers. AI Commun. Roberto Javier Asín Achá, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2010	A	`conf`	SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering. CP Robert Nieuwenhuis
2009	A	`conf`	Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates. SAT Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2009	A	`conf`	Cardinality Networks and Their Applications. SAT Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2009	A	`conf`	SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms. SAT Robert Nieuwenhuis
2008	B	`conf`	A Write-Based Solver for SAT Modulo the Theory of Arrays. FMCAD Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
2008	B	`conf`	Efficient Generation of Unsatisfiability Proofs and Cores in SAT. LPAR Roberto Asín, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2008	J	`jnl`	Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra. Discret. Appl. Math. Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
2008	A	`conf`	SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers. SAT Germain Faure, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
2008	A*	`conf`	The Barcelogic SMT Solver. CAV Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
2008	B	`conf`	The Max-Atom Problem and Its Relevance. LPAR Marc Bezem, Robert Nieuwenhuis, Enric Rodríguez-Carbonell
2007	—	`conf`	07401 Abstracts Collection -- Deduction and Decision Procedures. Deduction and Decision Procedures Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
2007	—	`conf`	07401 Executive Summary -- Deduction and Decision Procedures. Deduction and Decision Procedures Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
2007	—	`conf`	Challenges in Satisfiability Modulo Theories. RTA Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio
2007	—	`ed.`	Deduction and Decision Procedures, 30.09. - 05.10.2007 Deduction and Decision Procedures Franz Baader, Byron Cook, Jürgen Giesl, Robert Nieuwenhuis
2007	J	`jnl`	Fast congruence closure and extensions. Inf. Comput. Robert Nieuwenhuis, Albert Oliveras
2006	—	`ed.`	Deduction and Applications, 23.-28. October 2005 Deduction and Applications Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
2006	A	`conf`	On SAT Modulo Theories and Optimization Problems. SAT Robert Nieuwenhuis, Albert Oliveras
2006	A*	`conf`	SMT Techniques for Fast Predicate Abstraction. CAV Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras
2006	J	`jnl`	Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL( J. ACM Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2006	B	`conf`	Splitting on Demand in SAT Modulo Theories. LPAR Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2005	—	`conf`	05431 Abstracts Collection - Deduction and Applications. Deduction and Applications Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
2005	—	`conf`	05431 Executive Summary - Deduction and Applications. Deduction and Applications Franz Baader, Peter Baumgartner, Robert Nieuwenhuis, Andrei Voronkov
2005	A	`ed.`	Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings CADE Robert Nieuwenhuis
2005	A*	`conf`	DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic. CAV Robert Nieuwenhuis, Albert Oliveras
2005	B	`conf`	Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. LPAR Robert Nieuwenhuis, Albert Oliveras
2005	—	`conf`	Proof-Producing Congruence Closure. RTA Robert Nieuwenhuis, Albert Oliveras
2004	B	`conf`	Abstract DPLL and Abstract DPLL Modulo Theories. LPAR Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2004	J	`jnl`	Classes of term rewrite systems with polynomial confluence problems. ACM Trans. Comput. Log. Guillem Godoy, Robert Nieuwenhuis, Ashish Tiwari
2004	J	`jnl`	Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups. Constraints An Int. J. Guillem Godoy, Robert Nieuwenhuis
2004	A*	`conf`	DPLL( T): Fast Decision Procedures. CAV Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli
2004	J	`jnl`	Fast Term Indexing with Coded Context Trees. J. Autom. Reason. Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
2004	J	`jnl`	Superposition with completely built-in Abelian groups. J. Symb. Comput. Guillem Godoy, Robert Nieuwenhuis
2003	B	`conf`	Congruence Closure with Integer Offsets. LPAR Robert Nieuwenhuis, Albert Oliveras
2003	J	`jnl`	Deciding the confluence of ordered term rewrite systems. ACM Trans. Comput. Log. Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch
2003	J	`jnl`	Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings. J. Autom. Reason. Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
2003	—	`ed.`	Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings RTA Robert Nieuwenhuis
2003	J	`jnl`	Stratified resolution. J. Symb. Comput. Anatoli Degtyarev, Robert Nieuwenhuis, Andrei Voronkov
2002	J	`jnl`	Practical Algorithms for Deciding Path Ordering Constraint Satisfaction. Inf. Comput. Robert Nieuwenhuis, José Miguel Rivero
2002	J	`jnl`	The impact of CASC in the development of automated deduction systems. AI Commun. Robert Nieuwenhuis
2001	A	`conf`	Context Trees. IJCAR Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela
2001	B	`ed.`	Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, LPAR 2001, Havana, Cuba, December 3-7, 2001, Proceedings LPAR Robert Nieuwenhuis, Andrei Voronkov
2001	A*	`conf`	On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. LICS Guillem Godoy, Robert Nieuwenhuis
2001	A	`conf`	On the Evaluation of Indexing Techniques for Theorem Proving. IJCAR Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov
2001	—	`ch.`	Paramodulation-Based Theorem Proving. Handbook of Automated Reasoning Robert Nieuwenhuis, Albert Rubio
2001	A*	`conf`	The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time. FOCS Hubert Comon, Guillem Godoy, Robert Nieuwenhuis
2000	J	`jnl`	Induction=I-Axiomatization+First-Order Consistency. Inf. Comput. Hubert Comon, Robert Nieuwenhuis
2000	—	`conf`	Modular Redundancy for Theorem Proving. FroCoS Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
2000	A*	`conf`	Paramodulation with Built-in Abelian Groups. LICS Guillem Godoy, Robert Nieuwenhuis
1999	—	`conf`	Constraints and Theorem Proving. CCL Harald Ganzinger, Robert Nieuwenhuis
1999	A	`conf`	Invited Talk: Rewrite-based Deduction and Symbolic Constraints. CADE Robert Nieuwenhuis
1999	A*	`conf`	Paramodulation with Non-Monotonic Orderings. LICS Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio
1999	—	`conf`	Solved Forms for Path Ordering Constraints. RTA Robert Nieuwenhuis, José Miguel Rivero
1998	J	`jnl`	Decidability and Complexity Analysis by Basic Paramodulation. Inf. Comput. Robert Nieuwenhuis
1998	A*	`conf`	Decision Problems in Ordered Rewriting. LICS Hubert Comon, Paliath Narendran, Robert Nieuwenhuis, Michaël Rusinowitch
1997	J	`jnl`	Barcelona. J. Autom. Reason. Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo
1997	A	`conf`	Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses. CADE Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo
1997	J	`jnl`	Paramodulation with Built-in AC-Theories and Symbolic Constraints. J. Symb. Comput. Robert Nieuwenhuis, Albert Rubio
1996	—	`conf`	An Implementation Kernel for Theorem Proving with Equality Clauses. APPIA-GULP-PRODE Robert Nieuwenhuis, José Miguel Rivero, Miguel Ángel Vallejo
1996	A*	`conf`	Basic Paramodulation and Decidable Theories (Extended Abstract). LICS Robert Nieuwenhuis
1995	—	`ed.`	9th International Workshop on Unification, UNIF 1995, Sitges, Spain, April 2-3, 1995. UNIF Robert Nieuwenhuis, Albert Rubio
1995	J	`jnl`	A Total AC-Compatible Ordering Based on RPO. Theor. Comput. Sci. Albert Rubio, Robert Nieuwenhuis
1995	—	`conf`	On Narrowing, Refutation Proofs and Constraints. RTA Robert Nieuwenhuis
1995	A*	`conf`	Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract) LICS Hubert Comon, Robert Nieuwenhuis, Albert Rubio
1995	J	`jnl`	Theorem Proving with Ordering and Equality Constrained Clauses. J. Symb. Comput. Robert Nieuwenhuis, Albert Rubio
1994	A	`conf`	AC-Superposition with Constraints: No AC-Unifiers Needed. CADE Robert Nieuwenhuis, Albert Rubio
1993	—	`conf`	A Precedence-Based Total AC-Compatible Ordering. RTA Albert Rubio, Robert Nieuwenhuis
1993	—	`conf`	Program Development: Completion Subsystem. PROSPECTRA Book Hubert Bertling, Harald Ganzinger, Renate Schäfers, Robert Nieuwenhuis, Fernando Orejas
1993	—	`conf`	Saturation of First-Order (Constrained) Clauses with the RTA Pilar Nivela, Robert Nieuwenhuis
1993	J	`jnl`	Simple LPO Constraint Solving Methods. Inf. Process. Lett. Robert Nieuwenhuis
1992	A	`conf`	Basic Superposition is Complete. ESOP Robert Nieuwenhuis, Albert Rubio
1992	A	`conf`	Theorem Proving with Ordering Constrained Clauses. CADE Robert Nieuwenhuis, Albert Rubio
1991	J	`jnl`	Efficient Deduction in Equality Horn Logic by Horn-Completion. Inf. Process. Lett. Robert Nieuwenhuis, Pilar Nivela
1990	—	`conf`	Clausal Rewriting. CTRS Robert Nieuwenhuis, Fernando Orejas
1990	—	`conf`	Clausal Rewriting: Applications and Implementation. ADT Robert Nieuwenhuis, Fernando Orejas
1990	A	`conf`	TRIP: An Implementation of Clausal Rewriting. CADE Robert Nieuwenhuis, Fernando Orejas, Albert Rubio