×

zbMATH — the first resource for mathematics

Nieuwenhuis, Robert

Compute Distance To:
Author ID: nieuwenhuis.robert Recent zbMATH articles by "Nieuwenhuis, Robert"
Published as: Nieuwenhuis, R.; Nieuwenhuis, Robert
Documents Indexed: 58 Publications since 1991, including 3 Books

Publications by Year

Citations contained in zbMATH

47 Publications have been cited 482 times in 356 Documents Cited by Year
Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\). Zbl 1326.68164
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
113
2006
Paramodulation-based theorem proving. Zbl 0997.03012
Nieuwenhuis, Robert; Rubio, Albert
60
2001
DPLL(\(T\)): Fast decision procedures. Zbl 1103.68616
Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
39
2004
Splitting on demand in SAT modulo theories. Zbl 1165.68480
Barrett, Clark; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
21
2006
Theorem proving with ordering and equality constrained clauses. Zbl 0844.68107
Nieuwenhuis, Robert; Rubio, Albert
21
1995
DPLL(\(T\)) with exhaustive theory propagation and its application to difference logic. Zbl 1081.68629
Nieuwenhuis, Robert; Oliveras, Albert
18
2005
On SAT modulo theories and optimization problems. Zbl 1187.68558
Nieuwenhuis, Robert; Oliveras, Albert
15
2006
Theorem proving with ordering constrained clauses. Zbl 0925.03076
Nieuwenhuis, Robert; Rubio, Albert
13
1992
Cardinality networks: a theoretical and empirical study. Zbl 1217.68200
Asín, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
12
2011
Proof-producing congruence closure. Zbl 1078.68661
Nieuwenhuis, Robert; Oliveras, Albert
11
2005
Induction = I-axiomatization + first-order consistency. Zbl 1046.68640
Comon, Hubert; Nieuwenhuis, Robert
11
2000
Curriculum-based course timetabling with SAT and MaxSAT. Zbl 1301.90023
Achá, Roberto Asín; Nieuwenhuis, Robert
10
2014
Hard problems in max-algebra, control theory, hypergraphs and other areas. Zbl 1206.68284
Bezem, Marc; Nieuwenhuis, Robert; Rodríguez-Carbonell, Enric
10
2010
Fast congruence closure and extensions. Zbl 1112.68116
Nieuwenhuis, Robert; Oliveras, Albert
10
2007
Abstract DPLL and abstract DPLL modulo theories. Zbl 1109.68097
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
9
2005
Exponential behaviour of the Butkovič-Zimmermann algorithm for solving two-sided linear systems in max-algebra. Zbl 1178.68637
Bezem, Marc; Nieuwenhuis, Robert; Rodríguez-Carbonell, Enric
8
2008
The max-atom problem and its relevance. Zbl 1182.68219
Bezem, Marc; Nieuwenhuis, Robert; Rodríguez-Carbonell, Enric
8
2008
Simple LPO constraint solving methods. Zbl 0781.68102
Nieuwenhuis, Robert
8
1993
Cardinality networks and their applications. Zbl 1247.68244
Asín, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
7
2009
Congruence closure with integer offsets. Zbl 1273.68326
Nieuwenhuis, Robert; Oliveras, Albert
6
2003
A total AC-compatible ordering based on RPO. Zbl 0873.68102
Rubio, Albert; Nieuwenhuis, Robert
6
1995
Challenges in satisfiability modulo theories. Zbl 1203.68189
Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert
5
2007
On the evaluation of indexing techniques for theorem proving. Zbl 0988.68595
Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei
5
2001
Efficient generation of unsatisfiability proofs and cores in SAT. Zbl 1182.68215
Asín, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
4
2008
SAT modulo the theory of linear arithmetic: Exact, inexact and commercial solvers. Zbl 1138.68537
Faure, Germain; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
4
2008
Decision procedures for SAT, SAT modulo theories and beyond. The BarcelogicTools. Zbl 1143.68579
Nieuwenhuis, Robert; Oliveras, Albert
4
2005
Superposition with completely built-in abelian groups. Zbl 1043.03011
Godoy, Guillem; Nieuwenhuis, Robert
4
2004
Decision problems in ordered rewriting. Zbl 0945.68520
Comon, H.; Narendran, P.; Nieuwenhuis, R.; Rusinowitch, M.
4
1998
Decidability and complexity analysis by basic paramodulation. Zbl 0927.68042
Nieuwenhuis, Robert
4
1998
A new look at BDDs for pseudo-Boolean constraints. Zbl 1252.68267
Abío, Ignasi; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric; Mayer-Eichberger, Valentin
3
2012
Context trees. Zbl 0988.68588
Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar
3
2001
Constraints and theorem proving. Zbl 0976.03518
Ganzinger, Harald; Nieuwenhuis, Robert
3
2001
Solved forms for path ordering constraints. Zbl 0943.68087
Nieuwenhuis, Robert; Rivero, José Miguel
3
1999
A parametric approach for smaller and better encodings of cardinality constraints. Zbl 1432.68412
Abío, Ignasi; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
2
2013
A framework for certified Boolean branch-and-bound optimization. Zbl 1213.68581
Larrosa, Javier; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
2
2011
Practical algorithms for unsatisfiability proof and core generation in SAT solvers. Zbl 1208.68195
Asín Achá, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
2
2010
Branch and bound for Boolean optimization and the generation of optimality certificates. Zbl 1247.68255
Larrosa, Javier; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
2
2009
Stratified resolution. Zbl 1024.03013
Degtyarev, Anatoli; Nieuwenhuis, Robert; Voronkov, Andrei
2
2003
Paramodulation with built-in AC-theories and symbolic constraints. Zbl 0878.68074
Nieuwenhuis, Robert; Rubio, Albert
2
1997
Reducing chaos in SAT-like search: finding solutions close to a given one. Zbl 1330.68266
Abío, Ignasi; Deters, Morgan; Nieuwenhuis, Robert; Stuckey, Peter J.
1
2011
BDDs for pseudo-Boolean constraints – revisited. Zbl 1330.68098
Abío, Ignasi; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
1
2011
Automated deduction – CADE-20. 20th international conference on automated deduction, Tallinn, Estonia, July 22–27, 2005. Proceedings. Zbl 1088.68008
Nieuwenhuis, Robert (ed.)
1
2005
Classes of term rewrite systems with polynomial confluence problems. Zbl 1367.68132
Godoy, Guillem; Nieuwenhuis, Robert; Tiwari, Ashish
1
2004
Fast term indexing with coded context trees. Zbl 1073.68077
Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar
1
2004
Rewriting techniques and applications. 14th international conference, RTA 2003, Valencia, Spain, June 9–11, 2003. Proceedings. Zbl 1029.00060
Nieuwenhuis, Robert (ed.)
1
2003
Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings. Zbl 1027.03010
Bofill, Miquel; Godoy, Guillem; Nieuwenhuis, Robert; Rubio, Albert
1
2003
Efficient deduction in equality Horn logic by Horn-completion. Zbl 0735.68075
Nieuwenhuis, Robert; Nivela, Pilar
1
1991
Curriculum-based course timetabling with SAT and MaxSAT. Zbl 1301.90023
Achá, Roberto Asín; Nieuwenhuis, Robert
10
2014
A parametric approach for smaller and better encodings of cardinality constraints. Zbl 1432.68412
Abío, Ignasi; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
2
2013
A new look at BDDs for pseudo-Boolean constraints. Zbl 1252.68267
Abío, Ignasi; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric; Mayer-Eichberger, Valentin
3
2012
Cardinality networks: a theoretical and empirical study. Zbl 1217.68200
Asín, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
12
2011
A framework for certified Boolean branch-and-bound optimization. Zbl 1213.68581
Larrosa, Javier; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
2
2011
Reducing chaos in SAT-like search: finding solutions close to a given one. Zbl 1330.68266
Abío, Ignasi; Deters, Morgan; Nieuwenhuis, Robert; Stuckey, Peter J.
1
2011
BDDs for pseudo-Boolean constraints – revisited. Zbl 1330.68098
Abío, Ignasi; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
1
2011
Hard problems in max-algebra, control theory, hypergraphs and other areas. Zbl 1206.68284
Bezem, Marc; Nieuwenhuis, Robert; Rodríguez-Carbonell, Enric
10
2010
Practical algorithms for unsatisfiability proof and core generation in SAT solvers. Zbl 1208.68195
Asín Achá, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
2
2010
Cardinality networks and their applications. Zbl 1247.68244
Asín, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
7
2009
Branch and bound for Boolean optimization and the generation of optimality certificates. Zbl 1247.68255
Larrosa, Javier; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
2
2009
Exponential behaviour of the Butkovič-Zimmermann algorithm for solving two-sided linear systems in max-algebra. Zbl 1178.68637
Bezem, Marc; Nieuwenhuis, Robert; Rodríguez-Carbonell, Enric
8
2008
The max-atom problem and its relevance. Zbl 1182.68219
Bezem, Marc; Nieuwenhuis, Robert; Rodríguez-Carbonell, Enric
8
2008
Efficient generation of unsatisfiability proofs and cores in SAT. Zbl 1182.68215
Asín, Roberto; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
4
2008
SAT modulo the theory of linear arithmetic: Exact, inexact and commercial solvers. Zbl 1138.68537
Faure, Germain; Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric
4
2008
Fast congruence closure and extensions. Zbl 1112.68116
Nieuwenhuis, Robert; Oliveras, Albert
10
2007
Challenges in satisfiability modulo theories. Zbl 1203.68189
Nieuwenhuis, Robert; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert
5
2007
Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\). Zbl 1326.68164
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
113
2006
Splitting on demand in SAT modulo theories. Zbl 1165.68480
Barrett, Clark; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
21
2006
On SAT modulo theories and optimization problems. Zbl 1187.68558
Nieuwenhuis, Robert; Oliveras, Albert
15
2006
DPLL(\(T\)) with exhaustive theory propagation and its application to difference logic. Zbl 1081.68629
Nieuwenhuis, Robert; Oliveras, Albert
18
2005
Proof-producing congruence closure. Zbl 1078.68661
Nieuwenhuis, Robert; Oliveras, Albert
11
2005
Abstract DPLL and abstract DPLL modulo theories. Zbl 1109.68097
Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
9
2005
Decision procedures for SAT, SAT modulo theories and beyond. The BarcelogicTools. Zbl 1143.68579
Nieuwenhuis, Robert; Oliveras, Albert
4
2005
Automated deduction – CADE-20. 20th international conference on automated deduction, Tallinn, Estonia, July 22–27, 2005. Proceedings. Zbl 1088.68008
Nieuwenhuis, Robert (ed.)
1
2005
DPLL(\(T\)): Fast decision procedures. Zbl 1103.68616
Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare
39
2004
Superposition with completely built-in abelian groups. Zbl 1043.03011
Godoy, Guillem; Nieuwenhuis, Robert
4
2004
Classes of term rewrite systems with polynomial confluence problems. Zbl 1367.68132
Godoy, Guillem; Nieuwenhuis, Robert; Tiwari, Ashish
1
2004
Fast term indexing with coded context trees. Zbl 1073.68077
Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar
1
2004
Congruence closure with integer offsets. Zbl 1273.68326
Nieuwenhuis, Robert; Oliveras, Albert
6
2003
Stratified resolution. Zbl 1024.03013
Degtyarev, Anatoli; Nieuwenhuis, Robert; Voronkov, Andrei
2
2003
Rewriting techniques and applications. 14th international conference, RTA 2003, Valencia, Spain, June 9–11, 2003. Proceedings. Zbl 1029.00060
Nieuwenhuis, Robert (ed.)
1
2003
Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings. Zbl 1027.03010
Bofill, Miquel; Godoy, Guillem; Nieuwenhuis, Robert; Rubio, Albert
1
2003
Paramodulation-based theorem proving. Zbl 0997.03012
Nieuwenhuis, Robert; Rubio, Albert
60
2001
On the evaluation of indexing techniques for theorem proving. Zbl 0988.68595
Nieuwenhuis, Robert; Hillenbrand, Thomas; Riazanov, Alexandre; Voronkov, Andrei
5
2001
Context trees. Zbl 0988.68588
Ganzinger, Harald; Nieuwenhuis, Robert; Nivela, Pilar
3
2001
Constraints and theorem proving. Zbl 0976.03518
Ganzinger, Harald; Nieuwenhuis, Robert
3
2001
Induction = I-axiomatization + first-order consistency. Zbl 1046.68640
Comon, Hubert; Nieuwenhuis, Robert
11
2000
Solved forms for path ordering constraints. Zbl 0943.68087
Nieuwenhuis, Robert; Rivero, José Miguel
3
1999
Decision problems in ordered rewriting. Zbl 0945.68520
Comon, H.; Narendran, P.; Nieuwenhuis, R.; Rusinowitch, M.
4
1998
Decidability and complexity analysis by basic paramodulation. Zbl 0927.68042
Nieuwenhuis, Robert
4
1998
Paramodulation with built-in AC-theories and symbolic constraints. Zbl 0878.68074
Nieuwenhuis, Robert; Rubio, Albert
2
1997
Theorem proving with ordering and equality constrained clauses. Zbl 0844.68107
Nieuwenhuis, Robert; Rubio, Albert
21
1995
A total AC-compatible ordering based on RPO. Zbl 0873.68102
Rubio, Albert; Nieuwenhuis, Robert
6
1995
Simple LPO constraint solving methods. Zbl 0781.68102
Nieuwenhuis, Robert
8
1993
Theorem proving with ordering constrained clauses. Zbl 0925.03076
Nieuwenhuis, Robert; Rubio, Albert
13
1992
Efficient deduction in equality Horn logic by Horn-completion. Zbl 0735.68075
Nieuwenhuis, Robert; Nivela, Pilar
1
1991
all top 5

Cited by 558 Authors

17 Weidenbach, Christoph
16 Nieuwenhuis, Robert
14 Tinelli, Cesare
12 Barrett, Clark W.
11 Voronkov, Andrei
10 Bonacina, Maria Paola
9 Lierler, Yuliya
9 Reynolds, Andrew
9 Sebastiani, Roberto
8 de Moura, Leonardo
8 Lynch, Christopher A.
7 Baumgartner, Peter
7 Gaubert, Stéphane
7 Meseguer Guaita, José
7 Ranise, Silvio
7 Waldmann, Uwe
6 Echenim, Mnacho
6 Ghilardi, Silvio
6 Ringeissen, Christophe
5 Allamigeon, Xavier
5 Blanchette, Jasmin Christian
5 Fontaine, Pascal
5 Horbach, Matthias
5 Korovin, Konstantin
5 Oliveras, Albert
5 Rodríguez-Carbonell, Enric
5 Rubio, Albert
5 Rusinowitch, Michaël
5 Schaub, Torsten H.
4 Bofill, Miquel
4 Bromberger, Martin
4 Bruttomesso, Roberto
4 Cimatti, Alessandro
4 Déharbe, David
4 Ganzinger, Harald
4 Gebser, Martin
4 Griggio, Alberto
4 Hustadt, Ullrich
4 Jovanović, Dejan
4 Kapur, Deepak
4 Kirchner, Hélène
4 Maratea, Marco
4 Nicolini, Enrica
4 Peltier, Nicolas
4 Schmidt, Renate A.
4 Stump, Aaron
4 Subramani, Krishnan
4 Tran, Duc-Khanh
4 Villaret, Mateu
3 Ansótegui, Carlos
3 Baader, Franz
3 Bright, Curtis
3 Butkovič, Peter
3 Codish, Michael
3 Conchon, Sylvain
3 Degtyarev, Anatoli Ivanovich
3 Deters, Morgan
3 Ganesh, Vijay
3 Grigor’ev, Dmitriĭ Yur’evich
3 Hillenbrand, Thomas
3 Johansson, Moa
3 Katz, Ricardo David
3 King, Andy
3 Kirchner, Claude
3 Kotsireas, Ilias S.
3 Kröning, Daniel
3 Larrosa, Javier
3 Löchner, Bernd
3 Manquinho, Vasco M.
3 Marques-Silva, João P.
3 Motik, Boris
3 Sharygina, Natasha
3 Song, Xiaoyu
3 Strichman, Ofer
3 Stuckey, Peter James
3 Sturm, Thomas F.
3 Tiwari, Ashish Kumar
3 Wojciechowski, Piotr J.
3 You, Jia-Huai
3 Zhang, Yan
2 Ábrahám, Erika
2 Alberti, Francesco
2 Areces, Carlos
2 Atserias, Albert
2 Bachmair, Leo
2 Banković, Milan
2 Bansal, Kshitij
2 Benchimol, Pascal
2 Binh, Nguyen Thanh
2 Bodirsky, Manuel
2 Borgwardt, Stefan
2 Bozzano, Marco
2 Chen, Shuwei
2 Christ, Jürgen
2 Comon, Hubert
2 Contejean, Evelyne
2 de Cat, Broes
2 De Oliveira, Diego Caminha B.
2 Dershowitz, Nachum
2 Dodaro, Carmine
...and 458 more Authors
all top 5

Cited in 54 Serials

48 Journal of Automated Reasoning
19 Information and Computation
17 Theory and Practice of Logic Programming
15 Formal Methods in System Design
14 Journal of Symbolic Computation
13 Theoretical Computer Science
13 Constraints
12 Artificial Intelligence
9 Annals of Mathematics and Artificial Intelligence
4 Logical Methods in Computer Science
3 Information Processing Letters
3 Annals of Operations Research
3 Applicable Algebra in Engineering, Communication and Computing
3 The Journal of Logic and Algebraic Programming
3 ACM Transactions on Computational Logic
2 Journal of Computer and System Sciences
2 Journal of Optimization Theory and Applications
2 Computers & Operations Research
2 International Journal of Algebra and Computation
2 MSCS. Mathematical Structures in Computer Science
2 Linear Algebra and its Applications
2 Computational Complexity
2 Top
2 Theory of Computing Systems
2 Mathematics in Computer Science
2 Journal of Logical and Algebraic Methods in Programming
1 Acta Informatica
1 Communications in Algebra
1 Acta Universitatis Palackianae Olomucensis. Facultas Rerum Naturalium. Mathematica
1 Fuzzy Sets and Systems
1 Information Sciences
1 Notre Dame Journal of Formal Logic
1 Science of Computer Programming
1 Annals of Pure and Applied Logic
1 Journal of Computer Science and Technology
1 Algorithmica
1 Discrete & Computational Geometry
1 International Journal of Approximate Reasoning
1 SIAM Journal on Matrix Analysis and Applications
1 Formal Aspects of Computing
1 Journal of Global Optimization
1 European Journal of Operational Research
1 SIAM Review
1 Journal of Heuristics
1 Soft Computing
1 Journal of Combinatorial Optimization
1 Journal of Systems Science and Complexity
1 Journal of Applied Mathematics
1 Journal of Machine Learning Research (JMLR)
1 Journal of Zhejiang University. Science A
1 Mathematical Programming Computation
1 Central European Journal of Computer Science
1 Izvestiya Irkutskogo Gosudarstvennogo Universiteta. Seriya Matematika
1 SIAM Journal on Applied Algebra and Geometry

Citations by Year