Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver.

References in zbMATH (referenced in 154 articles )

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

1 2 3 ... 6 7 8 next

  1. Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan: Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (2022)
  2. Stehr, Mark-Oliver; Kim, Minyoung; Talcott, Carolyn L.: A probabilistic approximate logic for neuro-symbolic learning and reasoning (2022)
  3. Bjørner, Nikolaj; Levatich, Maxwell; Lopes, Nuno P.; Rybalchenko, Andrey; Vuppalapati, Chandrasekar: Supercharging plant configurations using Z3 (2021)
  4. Luteberget, Bjørnar; Claessen, Koen; Johansen, Christian; Steffen, Martin: SAT modulo discrete event simulation applied to railway design capacity analysis (2021)
  5. Mann, Makai; Wilson, Amalee; Zohar, Yoni; Stuntz, Lindsey; Irfan, Ahmed; Brown, Kristopher; Donovick, Caleb; Guman, Allison; Tinelli, Cesare; Barrett, Clark: Smt-Switch: a solver-agnostic C++ API for SMT solving (2021)
  6. Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare: On solving quantified bit-vector constraints using invertibility conditions (2021)
  7. Pimpalkhare, Nikhil; Mora, Federico; Polgreen, Elizabeth; Seshia, Sanjit A.: MedleySolver: online SMT algorithm selection (2021)
  8. Subramani, K.; Wojciechowski, P.: On the parametrized complexity of Read-once refutations in UTVPI+ constraint systems (2021)
  9. Winkler, Sarah; Moser, Georg: Runtime complexity analysis of logically constrained rewriting (2021)
  10. Bonacina, Maria Paola; Graham-Lengrand, Stéphane; Shankar, Natarajan: Conflict-driven satisfiability for theory combination: transition system and completeness (2020)
  11. Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph: A complete and terminating approach to linear integer solving (2020)
  12. Calvanese, Diego; Ghilardi, Silvio; Gianola, Alessandro; Montali, Marco; Rivkin, Andrey: SMT-based verification of data-aware processes: a model-theoretic approach (2020)
  13. Durán, Francisco; Eker, Steven; Escobar, Santiago; Martí-Oliet, Narciso; Meseguer, José; Rubio, Rubén; Talcott, Carolyn: Programming and symbolic computation in Maude (2020)
  14. Rümmer, Philipp: Competition report: CHC-COMP-20 (2020)
  15. Sebastiani, Roberto; Trentin, Patrick: \textscOptiMathSAT: a tool for optimization modulo theories (2020)
  16. Semenov, Alexander; Otpuschennikov, Ilya; Gribanova, Irina; Zaikin, Oleg; Kochemazov, Stepan: Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems (2020)
  17. Wojciechowski, Piotr; Chandrasekaran, R.; Subramani, K.: Analyzing fractional Horn constraint systems (2020)
  18. Akgün, Özgür; Gent, Ian; Kitaev, Sergey; Zantema, Hans: Solving computational problems in the theory of word-representable graphs (2019)
  19. Bofill, Miquel; Manyà, Felip; Vidal, Amanda; Villaret, Mateu: New complexity results for Łukasiewicz logic (2019)
  20. Borralleras, Cristina; Larraz, Daniel; Rodríguez-Carbonell, Enric; Oliveras, Albert; Rubio, Albert: Incomplete SMT techniques for solving non-linear formulas over the integers (2019)

1 2 3 ... 6 7 8 next