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

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

1 2 next

  1. Creus, Carles; Godoy, Guillem: Automatic evaluation of context-free grammars (system description) (2014)
  2. Brauer, Jörg; King, Andy: Transfer function synthesis without quantifier elimination (2012)
  3. Eggersglüß, Stephan; Drechsler, Rolf: High quality test pattern generation and Boolean satisfiability. (2012)
  4. Barrett, Edd; King, Andy: Range and set abstraction using SAT (2010)
  5. Soh, Takehide; Inoue, Katsumi; Tamura, Naoyuki; Banbara, Mutsunori; Nabeshima, Hidetomo: A SAT-based method for solving the two-dimensional strip packing problem (2010)
  6. Wille, Robert; Drechsler, Rolf: Towards a design flow for reversible logic (2010)
  7. Drechsler, R.; Eggersglüß, S.; Fey, G.; Tille, D.: Test pattern generation using Boolean proof engines (2009)
  8. Kroening, Daniel; Strichman, Ofer: A framework for satisfiability modulo theories (2009)
  9. Masalagiu, Cristian; Chin, Wei-Ngan; Andrei, Ştefan; Alaiba, Vasile: A rigorous methodology for specification and verification of business processes (2009)
  10. Fey, Görschwin; Drechsler, Rolf: Robustness and usability in modern design flows (2008)
  11. Gershman, Roman; Koifman, Maya; Strichman, Ofer: An approach for extracting a small unsatisfiable core (2008)
  12. Mouhoub, Malek: Systematic versus local search and GA techniques for incremental SAT (2008)
  13. Amla, Nina; McMillan, Kenneth L.: Combining abstraction refinement and SAT-based model checking (2007)
  14. Fränzle, Martin; Herde, Christian: HySAT: An efficient proof engine for bounded model checking of hybrid systems (2007)
  15. Ganai, Malay K.; Talupur, Muralidhar; Gupta, Aarti: SDSAT: Tight integration of small domain encoding and lazy approaches in solving difference logic. (2007)
  16. Aloul, Fadi A.: Search techniques for SAT-based Boolean optimization (2006)
  17. Biere, Armin; Heljanko, Keijo; Junttila, Tommi; Latvala, Timo; Schuppan, Viktor: Linear encodings of bounded LTL model checking (2006)
  18. Gupta, Aarti; Ganai, Malay K.; Wang, Chao: SAT-based verification methods and applications in hardware verification (2006)
  19. Khasidashvili, Zurab; Nadel, Alexander; Palti, Amit; Hanna, Ziyad: Simultaneous SAT-based model checking of safety properties (2006)
  20. Amla, Nina; Du, Xiaoqun; Kuehlmann, Andreas; Kurshan, Robert P.; McMillan, Kenneth L.: An analysis of sAT-based model checking techniques in an industrial environment (2005)

1 2 next