62 citations · 70 across the 4 of their papers we have counts for
4 papers
IntSat: Integer Linear Programming by Conflict-Driven Constraint-Learning
Robert Nieuwenhuis, Albert Oliveras, Enric Rodriguez-Carbonell
State-of-the-art SAT solvers are nowadays able to handle huge real-world instances. The key to this success is the so-called Conflict-Driven Clause-Learning (CDCL) scheme, which en…
Incomplete SMT Techniques for Solving Non-Linear Formulas over the Integers
Cristina Borralleras, Daniel Larraz, Albert Oliveras +2
We present new methods for solving the Satisfiability Modulo Theories problem over the theory of Quantifier-Free Non-linear Integer Arithmetic, SMT(QF-NIA), which consists in decid…
Compositional Safety Verification with Max-SMT
Marc Brockschmidt, Daniel Larraz, Albert Oliveras +2
We present an automated compositional program verification technique for safety properties based on conditional inductive invariants. For a given program part (e.g., a single loop)…
A New Look at BDDs for Pseudo-Boolean Constraints
Ignasi Abío, Robert Nieuwenhuis, Albert Oliveras +2
Pseudo-Boolean constraints are omnipresent in practical applications, and thus a significant effort has been devoted to the development of good SAT encoding techniques for them. So…