| Publication | Date of Publication | Type |
|---|
Using execution logs for improving pseudo-Boolean propagation
Artificial Intelligence | 2026-03-09 | Paper |
| Speeding up pseudo-Boolean propagation | 2026-02-03 | Paper |
IntSat: integer linear programming by conflict-driven constraint learning
Optimization Methods & Software | 2024-08-12 | Paper |
Clausal rewriting
Conditional and Typed Rewriting Systems | 2023-03-09 | Paper |
A precedence-based total AC-compatible ordering
Rewriting Techniques and Applications | 2022-12-09 | Paper |
On narrowing, refutation proofs and constraints
Rewriting Techniques and Applications | 2022-12-09 | Paper |
AC-superposition with constraints: no AC-unifiers needed
Automated Deduction — CADE-12 | 2020-01-21 | Paper |
Dedam: A kernel of data structures and algorithms for automated deduction with equality clauses
Automated Deduction—CADE-14 | 2019-10-01 | Paper |
| Completeness of cutting planes revisited | 2019-07-24 | Paper |
Improving IntSat by expressing disjunctions of bounds as linear constraints
AI Communications | 2017-11-07 | Paper |
Classes of term rewrite systems with polynomial confluence problems
ACM Transactions on Computational Logic | 2017-07-12 | Paper |
Deciding the confluence of ordered term rewrite systems
ACM Transactions on Computational Logic | 2017-06-13 | Paper |
Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
Journal of the ACM | 2015-12-04 | Paper |
Curriculum-based course timetabling with SAT and MaxSAT
Annals of Operations Research | 2014-11-26 | Paper |
A parametric approach for smaller and better encodings of cardinality constraints
Lecture Notes in Computer Science | 2014-05-12 | Paper |
Harald Ganzinger's legacy: contributions to logics and programming
Programming Logics | 2013-04-19 | Paper |
A New Look at BDDs for Pseudo-Boolean Constraints
Journal of Artificial Intelligence Research | 2012-12-03 | Paper |
SAT and SMT are still resolution: questions and challenges
Automated Reasoning | 2012-09-05 | Paper |
Reducing chaos in SAT-like search: finding solutions close to a given one
Theory and Applications of Satisfiability Testing - SAT 2011 | 2011-06-17 | Paper |
BDDs for pseudo-Boolean constraints -- revisited
Theory and Applications of Satisfiability Testing - SAT 2011 | 2011-06-17 | Paper |
Cardinality networks: a theoretical and empirical study
Constraints | 2011-05-25 | Paper |
A framework for certified Boolean branch-and-bound optimization
Journal of Automated Reasoning | 2011-04-05 | Paper |
Hard problems in max-algebra, control theory, hypergraphs and other areas
Information Processing Letters | 2010-09-02 | Paper |
Practical algorithms for unsatisfiability proof and core generation in SAT solvers
AI Communications | 2010-06-17 | Paper |
| Congruence closure with integer offsets | 2010-02-24 | Paper |
Cardinality Networks and Their Applications
Lecture Notes in Computer Science | 2009-07-07 | Paper |
Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates
Lecture Notes in Computer Science | 2009-07-07 | Paper |
Exponential behaviour of the Butkovič-Zimmermann algorithm for solving two-sided linear systems in max-algebra
Discrete Applied Mathematics | 2009-03-04 | Paper |
The Max-Atom Problem and Its Relevance
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Efficient Generation of Unsatisfiability Proofs and Cores in SAT
Logic for Programming, Artificial Intelligence, and Reasoning | 2009-01-27 | Paper |
Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
Splitting on Demand in SAT Modulo Theories
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
Theory and Applications of Satisfiability Testing – SAT 2008 | 2008-05-27 | Paper |
Challenges in Satisfiability Modulo Theories
Lecture Notes in Computer Science | 2008-01-02 | Paper |
On SAT Modulo Theories and Optimization Problems
Lecture Notes in Computer Science | 2007-09-04 | Paper |
Fast congruence closure and extensions
Information and Computation | 2007-04-16 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2006-01-10 | Paper |
Term Rewriting and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
Logic for Programming, Artificial Intelligence, and Reasoning
Lecture Notes in Computer Science | 2005-11-10 | Paper |
Computer Aided Verification
Lecture Notes in Computer Science | 2005-08-25 | Paper |
Constraint solving for term orderings compatible with abelian semigroups, monoids and groups
Constraints | 2005-03-15 | Paper |
Fast term indexing with coded context trees
Journal of Automated Reasoning | 2004-08-16 | Paper |
Superposition with completely built-in abelian groups
Journal of Symbolic Computation | 2004-06-22 | Paper |
Practical algorithms for deciding path ordering constraint satisfaction.
Information and Computation | 2003-11-02 | Paper |
Stratified resolution
Journal of Symbolic Computation | 2003-08-25 | Paper |
Paramodulation and Knuth-Bendix completion with nontotal and nonmonotonic orderings
Journal of Automated Reasoning | 2003-06-09 | Paper |
Induction = I-axiomatization + first-order consistency.
Information and Computation | 2003-01-14 | Paper |
| Paramodulation-based theorem proving | 2002-08-27 | Paper |
| scientific article; zbMATH DE number 1765674 (Why is no real title available?) | 2002-07-10 | Paper |
| scientific article; zbMATH DE number 1765673 (Why is no real title available?) | 2002-07-10 | Paper |
| scientific article; zbMATH DE number 1688812 (Why is no real title available?) | 2002-01-09 | Paper |
| scientific article; zbMATH DE number 1538015 (Why is no real title available?) | 2000-12-03 | Paper |
| scientific article; zbMATH DE number 1405617 (Why is no real title available?) | 2000-02-23 | Paper |
| scientific article; zbMATH DE number 1392288 (Why is no real title available?) | 2000-01-24 | Paper |
Decidability and complexity analysis by basic paramodulation
Information and Computation | 1999-11-29 | Paper |
| scientific article; zbMATH DE number 1348468 (Why is no real title available?) | 1999-10-10 | Paper |
Paramodulation with built-in AC-theories and symbolic constraints
Journal of Symbolic Computation | 1997-05-28 | Paper |
A total AC-compatible ordering based on RPO
Theoretical Computer Science | 1997-02-28 | Paper |
Theorem proving with ordering and equality constrained clauses
Journal of Symbolic Computation | 1995-09-04 | Paper |
Simple LPO constraint solving methods
Information Processing Letters | 1993-10-17 | Paper |
Efficient deduction in equality Horn logic by Horn-completion
Information Processing Letters | 1992-06-27 | Paper |
