-
Chapter and Conference Paper
Generating Modulo-2 Linear Invariants for Hardware Model Checking
We present an algorithm to automatically extract inductive modulo-2 linear invariants from a design. This algorithm makes use of basic linear algebra and is realized on top of an incremental SAT solver. The ex...
-
Chapter and Conference Paper
Computing Interpolants without Proofs
We describe an incremental algorithm for computing interpolants for a pair ϕ A , ϕ B of formulas in propositional logic. ...
-
Chapter and Conference Paper
Perfect Hashing and CNF Encodings of Cardinality Constraints
We study the problem of encoding cardinality constraints (threshold functions) on Boolean variables into CNF. Specifically, we propose new encodings based on (perfect) hashing that are efficient in terms of th...
-
Chapter and Conference Paper
On Efficient Computation of Variable MUSes
In this paper we address the following problem: given an unsatisfiable CNF formula \({\mathcal{F}}\) , find a minimal su...