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 36 articles )

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

1 2 next

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

1 2 next