Skip to main content

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)