Skip to main content

7 Result(s)

within Conference Paper Remove this filter Alexander Ivrii Remove this filter

and

  1. No Access

    Chapter and Conference Paper

    Finding All Minimal Safe Inductive Sets

    Computing minimal (or even just small) certificates is a central problem in automated reasoning and, in particular, in automated formal verification. For unsatisfiable formulas in CNF such certificates take th...

    Ryan Berryhill, Alexander Ivrii… in Theory and Applications of Satisfiability … (2018)

  2. No Access

    Chapter and Conference Paper

    Mining Backbone Literals in Incremental SAT

    In incremental SAT solving, information gained from previous similar instances has so far been limited to learned clauses that are still relevant, and heuristic information such as activity weights and scores....

    Alexander Ivrii, Vadim Ryvchin… in Theory and Applications of Satisfiability … (2015)

  3. No Access

    Chapter and Conference Paper

    Speeding up MUS Extraction with Preprocessing and Chunking

    In this paper we present several improvements to extraction of a minimal unsatisfiable subformula (MUS) of a Boolean formula. As our first contribution, we describe model rotation on preprocessed formulas and ...

    Valeriy Balabanov, Alexander Ivrii in Theory and Applications of Satisfiability … (2015)

  4. No Access

    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...

    Gadi Aleksandrowicz, Alexander Ivrii… in Hardware and Software: Verification and Te… (2014)

  5. No Access

    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. ...

    Hana Chockler, Alexander Ivrii… in Hardware and Software: Verification and Te… (2013)

  6. No Access

    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...

    Yael Ben-Haim, Alexander Ivrii… in Theory and Applications of Satisfiability … (2012)

  7. No Access

    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...

    Anton Belov, Alexander Ivrii, Arie Matsliah… in Theory and Applications of Satisfiability … (2012)