Robert Nieuwenhuis
Robert Nieuwenhuis
Professor of Computer Science, Tech. Univ. Catalonia (UPC), Barcelona
Verified email at cs.upc.edu - Homepage
TitleCited byYear
Solving SAT and SAT modulo theories: from an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL (T)
R Nieuwenhuis, A Oliveras, C Tinelli
Journal of the ACM (JACM) 53 (6), 937-977, 2006
8632006
Paramodulation-Based Theorem Proving.
R Nieuwenhuis, A Rubio
Handbook of automated reasoning 1, 371-443, 2001
4102001
DPLL(T): Fast Decision Procedures
H Ganzinger, G Hagen, R Nieuwenhuis, A Oliveras, C Tinelli
International Conference on Computer Aided Verification, 175-188, 2004
3732004
On SAT modulo theories and optimization problems
R Nieuwenhuis, A Oliveras
International conference on theory and applications of satisfiability …, 2006
1532006
DPLL (T) with exhaustive theory propagation and its application to difference logic
R Nieuwenhuis, A Oliveras
International Conference on Computer Aided Verification, 321-334, 2005
1512005
Theorem proving with ordering and equality constrained clauses
R Nieuwenhuis, A Rubio
Journal of Symbolic Computation 19 (4), 321-351, 1995
1471995
Cardinality networks: a theoretical and empirical study
R Asín, R Nieuwenhuis, A Oliveras, E Rodríguez-Carbonell
Constraints 16 (2), 195-221, 2011
1312011
Abstract DPLL and abstract DPLL modulo theories
R Nieuwenhuis, A Oliveras, C Tinelli
International Conference on Logic for Programming Artificial Intelligence …, 2005
1222005
Splitting on demand in SAT modulo theories
C Barrett, R Nieuwenhuis, A Oliveras, C Tinelli
International Conference on Logic for Programming Artificial Intelligence …, 2006
1102006
SMT techniques for fast predicate abstraction
SK Lahiri, R Nieuwenhuis, A Oliveras
International Conference on Computer Aided Verification, 424-437, 2006
1092006
The barcelogic SMT solver
M Bofill, R Nieuwenhuis, A Oliveras, E Rodríguez-Carbonell, A Rubio
International Conference on Computer Aided Verification, 294-298, 2008
1032008
Basic superposition is complete
R Nieuwenhuis, A Rubio
European Symposium on Programming, 371-389, 1992
1011992
Theorem proving with ordering constrained clauses
R Nieuwenhuis, A Rubio
International Conference on Automated Deduction, 477-491, 1992
991992
Proof-producing congruence closure
R Nieuwenhuis, A Oliveras
International Conference on Rewriting Techniques and Applications, 453-468, 2005
942005
Simple LPO constraint solving methods
R Nieuwenhuis
Information Processing Letters 47 (2), 65-69, 1993
861993
Curriculum-based course timetabling with SAT and MaxSAT
RA Achá, R Nieuwenhuis
Annals of Operations Research 218 (1), 71-91, 2014
802014
Fast congruence closure and extensions
R Nieuwenhuis, A Oliveras
Information and Computation 205 (4), 557-580, 2007
782007
Induction= I-axiomatization+ first-order consistency
H Comon, R Nieuwenhuis
Information and Computation 159 (1-2), 151-186, 2000
682000
Cardinality networks and their applications
R Asín, R Nieuwenhuis, A Oliveras, E Rodríguez-Carbonell
International Conference on Theory and Applications of Satisfiability …, 2009
652009
AC-superposition with constraints: No AC-unifiers needed
R Nieuwenhuis, A Rubio
International Conference on Automated Deduction, 545-559, 1994
651994
The system can't perform the operation now. Try again later.
Articles 1–20