Yaga is an MCSat based [3] SMT solver. Currently, we implemented plugins for Boolean and rational variables which can be used to decide problems in quantifier-free linear real arithmetic. The Boolean plugin uses the typical mechanism of watched literals [6] to perform Boolean constraint propagation. The plugin for linear real arithmetic uses a similar mechanism of watched variables to keep track of variable bounds [5]. The last checked variable in each clause or a linear constraint is cached. Search for a non-falsified literal or an unassigned rational variable always starts from the last position. Additionally, we use the following heuristics:


  1. Gilles Audemard and Laurent Simon. On the Glucose SAT solver. International Journal on Artificial Intelligence Tools, 27(01):1840001, 2018.
  2. Armin Biere. Weaknesses of CDCL solvers. In Fields Institute Workshop on Theoretical Foundations of SAT Solving, 2016.
  3. Leonardo De Moura and Dejan Jovanovic. A model-constructing satisfiability calculus. In Verification, Model Checking, and Abstract Interpretation: 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings 14, pages 1–12. Springer, 2013.
  4. Niklas Een and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. SAT, 3569:61–75, 2005.
  5. Dejan Jovanovic, Clark Barrett, and Leonardo De Moura. The design and implementation of the model constructing satisfiability calculus. In 2013 Formal Methods in Computer-Aided Design, pages 173–180. IEEE, 2013.
  6. Matthew W Moskewicz, Conor F Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th annual Design Automation Conference, pages 530–535, 2001.
  7. Knot Pipatsrisawat and Adnan Darwiche. A lightweight component caching scheme for satisfiability solvers. In Theory and Applications of Satisfiability Testing–SAT 2007: 10th International Conference, Lisbon, Portugal, May 28–31, 2007. Proceedings 10, pages 294–299. Springer, 2007.

Student projects

We offer bachelor and master thesis as well as research projects extending the Yaga project. If you are interested, please contact us!