Mjollnir: Quantifier elimination by lazy model enumeration. We propose a quantifier elimination scheme based on nested lazy model enumeration through SMT-solving, and projections. This scheme may be applied to any logic that fulfills certain conditions; we illustrate it for linear real arithmetic. The quantifier elimination problem for linear real arithmetic is doubly exponential in the worst case, and so is our method. We have implemented it and benchmarked it against other methods from the literature.

References in zbMATH (referenced in 14 articles )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Bacci, Giovanni; Bouyer, Patricia; Fahrenberg, Uli; Larsen, Kim G.; Markey, Nicolas; Reynier, Pierre-Alain: Optimal and robust controller synthesis using energy timed automata with uncertainty (2021)
  2. Lagniez, Jean-Marie; Lonca, Emmanuel; Marquis, Pierre: Definability for model counting (2020)
  3. Reynolds, Andrew; Kuncak, Viktor; Tinelli, Cesare; Barrett, Clark; Deters, Morgan: Refutation-based synthesis in SMT (2019)
  4. Akbari, Amir; Barton, Paul I.: An improved multi-parametric programming algorithm for flux balance analysis of metabolic networks (2018)
  5. Gläßle, T.; Gross, D.; Chaves, R.: Computational tools for solving a marginal problem with applications in Bell non-locality and causal modeling (2018)
  6. Reynolds, Andrew; King, Tim; Kuncak, Viktor: Solving quantified linear arithmetic by counterexample-guided instantiation (2017)
  7. Janota, Mikoláš; Klieber, William; Marques-Silva, Joao; Clarke, Edmund: Solving QBF with counterexample guided refinement (2016)
  8. John, Ajith K.; Chakraborty, Supratik: A layered algorithm for quantifier elimination from linear modular constraints (2016)
  9. Monniaux, David: A survey of satisfiability modulo theory (2016)
  10. Dvořák, Wolfgang; Järvisalo, Matti; Wallner, Johannes Peter; Woltran, Stefan: Complexity-sensitive decision procedures for abstract argumentation (2014)
  11. Brauer, Jörg; King, Andy; Kowalewski, Stefan: Abstract interpretation of microcontroller code: intervals meet congruences (2013)
  12. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2011)
  13. Janota, Mikoláš; Marques-Silva, Joao: Abstraction-based algorithm for 2QBF (2011)
  14. Monniaux, David: Quantifier elimination by lazy model enumeration (2010) ioport