Robert Nieuwenhuis

CoRR, 2024

2021

Employee Scheduling With SAT-Based Pseudo-Boolean Constraint Solving.

[BibT_eX]

[DOI]

Emma Rollon

IEEE Access, 2021

A Heuristic Approach to the Design of Optimal Cross-Docking Boxes.

[BibT_eX]

[DOI]

IEEE Access, 2021

2020

Decision levels are stable: towards better SAT heuristics.

[BibT_eX]

[DOI]

Adrià Lozano

Proceedings of the LPAR 2020: 23rd International Conference on Logic for Programming, 2020

2016

Improving IntSat by expressing disjunctions of bounds as linear constraints.

[BibT_eX]

[DOI]

AI Commun., 2016

2015

SAT-Based Techniques for Integer Linear Constraints.

[BibT_eX]

[DOI]

Proceedings of the Global Conference on Artificial Intelligence, 2015

2014

Curriculum-based course timetabling with SAT and MaxSAT.

[BibT_eX]

[DOI]

Roberto Javier Asín Achá

Ann. Oper. Res., 2014

The IntSat Method for Integer Linear Programming.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2014

2013

To Encode or to Propagate? The Best Choice for Each Constraint in SAT.

[BibT_eX]

[DOI]

Peter J. Stuckey

Proceedings of the Principles and Practice of Constraint Programming, 2013

A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming, 2013

Harald Ganzinger's Legacy: Contributions to Logics and Programming.

[BibT_eX]

[DOI]

Proceedings of the Programming Logics - Essays in Memory of Harald Ganzinger, 2013

2012

A New Look at BDDs for Pseudo-Boolean Constraints.

[BibT_eX]

[DOI]

Valentin Mayer-Eichberger

J. Artif. Intell. Res., 2012

SAT and SMT Are Still Resolution: Questions and Challenges.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

2011

A Framework for Certified Boolean Branch-and-Bound Optimization.

[BibT_eX]

[DOI]

Javier Larrosa

J. Autom. Reason., 2011

Decision Procedures in Soft, Hard and Bio-ware - Follow Up (Dagstuhl Seminar 11272).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2011

Cardinality Networks: a theoretical and empirical study.

[BibT_eX]

[DOI]

Constraints An Int. J., 2011

BDDs for Pseudo-Boolean Constraints - Revisited.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

Reducing Chaos in SAT-Like Search: Finding Solutions Close to a Given One.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing - SAT 2011, 2011

2010

Hard problems in max-algebra, control theory, hypergraphs and other areas.

[BibT_eX]

[DOI]

Inf. Process. Lett., 2010

Practical algorithms for unsatisfiability proof and core generation in SAT solvers.

[BibT_eX]

[DOI]

Roberto Javier Asín Achá

AI Commun., 2010

10161 Executive Summary - Decision Procedures in Software, Hardware and Bioware.

[BibT_eX]

[DOI]

Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

10161 Abstracts Collection - Decision Procedures in Software, Hardware and Bioware.

[BibT_eX]

[DOI]

Proceedings of the Decision Procedures in Software, Hardware and Bioware, 18.04., 2010

SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering.

[BibT_eX]

[DOI]

Proceedings of the Principles and Practice of Constraint Programming - CP 2010, 2010

2009

SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates.

[BibT_eX]

[DOI]

Javier Larrosa

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

Cardinality Networks and Their Applications.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2009

2008

Exponential behaviour of the Butkovic-Zimmermann algorithm for solving two-sided linear systems in max-algebra.

[BibT_eX]

[DOI]

Discret. Appl. Math., 2008

SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers.

[BibT_eX]

[DOI]

Germain Faure

Proceedings of the Theory and Applications of Satisfiability Testing, 2008

The Max-Atom Problem and Its Relevance.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

Efficient Generation of Unsatisfiability Proofs and Cores in SAT.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2008

A Write-Based Solver for SAT Modulo the Theory of Arrays.

[BibT_eX]

[DOI]

Miquel Bofill

Proceedings of the Formal Methods in Computer-Aided Design, 2008

The Barcelogic SMT Solver.

[BibT_eX]

[DOI]

Miquel Bofill

Proceedings of the Computer Aided Verification, 20th International Conference, 2008

2007

Fast congruence closure and extensions.

[BibT_eX]

[DOI]

Inf. Comput., 2007

Challenges in Satisfiability Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 18th International Conference, 2007

07401 Abstracts Collection -- Deduction and Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

07401 Executive Summary -- Deduction and Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Decision Procedures, 30.09. - 05.10.2007, 2007

2006

Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(<i>T</i>).

[BibT_eX]

[DOI]

Cesare Tinelli

J. ACM, 2006

On SAT Modulo Theories and Optimization Problems.

[BibT_eX]

[DOI]

Proceedings of the Theory and Applications of Satisfiability Testing, 2006

Splitting on Demand in SAT Modulo Theories.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2006

SMT Techniques for Fast Predicate Abstraction.

[BibT_eX]

[DOI]

Shuvendu K. Lahiri

Proceedings of the Computer Aided Verification, 18th International Conference, 2006

2005

Proof-Producing Congruence Closure.

[BibT_eX]

[DOI]

Proceedings of the Term Rewriting and Applications, 16th International Conference, 2005

Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2005

05431 Abstracts Collection - Deduction and Applications.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

05431 Executive Summary - Deduction and Applications.

[BibT_eX]

[DOI]

Proceedings of the Deduction and Applications, 23.-28. October 2005, 2005

DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 17th International Conference, 2005

2004

Classes of term rewrite systems with polynomial confluence problems.

[BibT_eX]

[DOI]

Ashish Tiwari

ACM Trans. Comput. Log., 2004

Superposition with completely built-in Abelian groups.

[BibT_eX]

[DOI]

J. Symb. Comput., 2004

Fast Term Indexing with Coded Context Trees.

[BibT_eX]

[DOI]

Harald Ganzinger

J. Autom. Reason., 2004

Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups.

[BibT_eX]

[DOI]

Constraints An Int. J., 2004

Abstract DPLL and Abstract DPLL Modulo Theories.

[BibT_eX]

[DOI]

Cesare Tinelli

Proceedings of the Logic for Programming, 2004

DPLL( T): Fast Decision Procedures.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification, 16th International Conference, 2004

2003

Deciding the confluence of ordered term rewrite systems.

[BibT_eX]

[DOI]

ACM Trans. Comput. Log., 2003

Stratified resolution.

[BibT_eX]

[DOI]

Anatoli Degtyarev

Andrei Voronkov

J. Symb. Comput., 2003

Paramodulation and Knuth-Bendix Completion with Nontotal and Nonmonotonic Orderings.

[BibT_eX]

[DOI]

J. Autom. Reason., 2003

Congruence Closure with Integer Offsets.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, 2003

2002

Practical Algorithms for Deciding Path Ordering Constraint Satisfaction.

[BibT_eX]

[DOI]

Inf. Comput., 2002

The impact of CASC in the development of automated deduction systems.

[BibT_eX]

[DOI]

AI Commun., 2002

2001

On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups.

[BibT_eX]

[DOI]

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

The Confluence of Ground Term Rewrite Systems is Decidable in Polynomial Time.

[BibT_eX]

[DOI]

Hubert Comon

Proceedings of the 42nd Annual Symposium on Foundations of Computer Science, 2001

On the Evaluation of Indexing Techniques for Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

Context Trees.

[BibT_eX]

[DOI]

Harald Ganzinger

Proceedings of the Automated Reasoning, First International Joint Conference, 2001

Paramodulation-Based Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

Induction=I-Axiomatization+First-Order Consistency.

[BibT_eX]

[DOI]

Hubert Comon

Inf. Comput., 2000

Paramodulation with Built-in Abelian Groups.

[BibT_eX]

[DOI]

Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, 2000

Modular Redundancy for Theorem Proving.

[BibT_eX]

[DOI]

Proceedings of the Frontiers of Combining Systems, 2000

1999

Solved Forms for Path Ordering Constraints.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 10th International Conference, 1999

Paramodulation with Non-Monotonic Orderings.

[BibT_eX]

[DOI]

Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, 1999

Constraints and Theorem Proving.

[BibT_eX]

[DOI]

Harald Ganzinger

Proceedings of the Constraints in Computational Logics: Theory and Applications, 1999

Invited Talk: Rewrite-based Deduction and Symbolic Constraints.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1999

1998

Decidability and Complexity Analysis by Basic Paramodulation.

[BibT_eX]

[DOI]

Inf. Comput., 1998

Decision Problems in Ordered Rewriting.

[BibT_eX]

[DOI]

Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science, 1998

1997

Paramodulation with Built-in AC-Theories and Symbolic Constraints.

[BibT_eX]

[DOI]

J. Symb. Comput., 1997

Barcelona.

[BibT_eX]

[DOI]

Miguel Ángel Vallejo

J. Autom. Reason., 1997

Dedan: A Kernel of Data Structures and Algorithms for Automated Deduction with Equality Clauses.

[BibT_eX]

[DOI]

Miguel Ángel Vallejo

Proceedings of the Automated Deduction, 1997

1996

Basic Paramodulation and Decidable Theories (Extended Abstract).

[BibT_eX]

[DOI]

Proceedings of the Proceedings, 1996

An Implementation Kernel for Theorem Proving with Equality Clauses.

[BibT_eX]

Miguel Ángel Vallejo

Proceedings of the 1996 Joint Conf. on Declarative Programming, 1996

1995

A Total AC-Compatible Ordering Based on RPO.

[BibT_eX]

[DOI]

Theor. Comput. Sci., 1995

Theorem Proving with Ordering and Equality Constrained Clauses.

[BibT_eX]

[DOI]

J. Symb. Comput., 1995

On Narrowing, Refutation Proofs and Constraints.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 6th International Conference, 1995

Orderings, AC-Theories and Symbolic Constraint Solving (Extended Abstract)

[BibT_eX]

[DOI]

Hubert Comon

Proceedings of the Proceedings, 1995

1994

AC-Superposition with Constraints: No AC-Unifiers Needed.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

Simple LPO Constraint Solving Methods.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1993

A Precedence-Based Total AC-Compatible Ordering.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

Saturation of First-Order (Constrained) Clauses with the <i>Saturate</i> System.

[BibT_eX]

[DOI]

Proceedings of the Rewriting Techniques and Applications, 5th International Conference, 1993

Program Development: Completion Subsystem.

[BibT_eX]

[DOI]

Proceedings of the Program Development by Specification and Transformation, 1993

1992

Basic Superposition is Complete.

[BibT_eX]

[DOI]

Proceedings of the ESOP '92, 1992

Theorem Proving with Ordering Constrained Clauses.

[BibT_eX]

[DOI]

Proceedings of the Automated Deduction, 1992

1991

Efficient Deduction in Equality Horn Logic by Horn-Completion.

[BibT_eX]

[DOI]

Inf. Process. Lett., 1991

1990

Clausal Rewriting.

[BibT_eX]

[DOI]

Fernando Orejas

Proceedings of the Conditional and Typed Rewriting Systems, 1990

TRIP: An Implementation of Clausal Rewriting.

[BibT_eX]

[DOI]

Fernando Orejas

Proceedings of the 10th International Conference on Automated Deduction, 1990

Clausal Rewriting: Applications and Implementation.

[BibT_eX]

[DOI]