SATIRE: A new incremental satisfiability engine. We introduce SATIRE, a new satisfiability solver that is particularly suited to verification and optimization problems in electronic design automation. SATIRE builds on the most recent advances in satisfiability research, and includes two new features to achieve even higher performance: a facility for incrementally solving sets of related problems, and the ability to handle non-CNF constraints. We provide experimental evidence showing the effectiveness of these additions to classical satisfiability solver

References in zbMATH (referenced in 39 articles )

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

1 2 next

  1. Le Berre, Daniel; Marquis, Pierre; Wallon, Romain: On weakening strategies for PB solvers (2020)
  2. Schrammel, Peter; Kroening, Daniel; Brain, Martin; Martins, Ruben; Teige, Tino; Bienmüller, Tom: Incremental bounded model checking for embedded software (2017)
  3. De Ita Luna, Guillermo; Marcial-Romero, J. Raymundo; Hernández, José A.: The incremental satisfiability problem for a two conjunctive normal form (2016)
  4. Kroening, Daniel; Strichman, Ofer: Decision procedures. An algorithmic point of view (2016)
  5. Ivrii, Alexander; Ryvchin, Vadim; Strichman, Ofer: Mining backbone literals in incremental SAT. A new kind of incremental data (2015)
  6. Creus, Carles; Godoy, Guillem: Automatic evaluation of context-free grammars (system description) (2014)
  7. Nadel, Alexander; Ryvchin, Vadim; Strichman, Ofer: Ultimately incremental SAT (2014)
  8. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)
  9. Eggersglüß, Stephan; Drechsler, Rolf: High quality test pattern generation and Boolean satisfiability. (2012)
  10. Gebser, Martin; Kaufmann, Roland; Schaub, Torsten: Gearing up for effective ASP planning (2012)
  11. Nadel, Alexander; Ryvchin, Vadim; Strichman, Ofer: Preprocessing in incremental SAT (2012)
  12. Barrett, Edd; King, Andy: Range and set abstraction using SAT (2010)
  13. Soh, Takehide; Inoue, Katsumi; Tamura, Naoyuki; Banbara, Mutsunori; Nabeshima, Hidetomo: A SAT-based method for solving the two-dimensional strip packing problem (2010)
  14. Wille, Robert; Drechsler, Rolf: Towards a design flow for reversible logic (2010)
  15. Drechsler, R.; Eggersglüß, S.; Fey, G.; Tille, D.: Test pattern generation using Boolean proof engines (2009)
  16. Kroening, Daniel; Strichman, Ofer: A framework for satisfiability modulo theories (2009)
  17. Masalagiu, Cristian; Chin, Wei-Ngan; Andrei, Ştefan; Alaiba, Vasile: A rigorous methodology for specification and verification of business processes (2009)
  18. Fey, Görschwin; Drechsler, Rolf: Robustness and usability in modern design flows (2008)
  19. Gershman, Roman; Koifman, Maya; Strichman, Ofer: An approach for extracting a small unsatisfiable core (2008)
  20. Mouhoub, Malek: Systematic versus local search and GA techniques for incremental SAT (2008)

1 2 next