## Overview

# Description

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:

- Variable order. Yaga uses a generalization of the VSIDS heuristic implementation from MiniSat [8]. Variable score is increased for each variable involved in conflict derivation. Variables of all types (i.e., Boolean and rational variables) are ranked using this heuristic.
- Restart scheme. We use a simplified restart scheme from the Glucose solver [1]. The solver maintains an exponential average of glucose level (LBD) of all learned clauses [2] and an exponential LBD average of recently learned clauses. Yaga restarts when the recent LBD average exceeds the global average by some threshold.
- Clause deletion. Yaga deletes subsumed learned clauses on restart [4].
- Clause minimization. Learned clauses are minimized using self-subsuming resolution introduced in MiniSat [8].
- Value caching. Similarly to phase-saving heuristics used in SAT solvers [7], Yaga caches values of decided rational variables [5]. It preferably uses cached values for rational variables. If a cached value is not available, the solver tries to find a small integer or a fraction with a small denominator which is a power of two.
- Bound caching. We keep a stack of variable bounds for each rational variable. When the solver backtracks, it lazily removes obsolete bounds from the stack. Bounds computed at a decision level lower than the backtrack level do not have to be recomputed.

## References

- Gilles Audemard and Laurent Simon. On the Glucose SAT solver. International Journal on Artificial Intelligence Tools, 27(01):1840001, 2018.
- Armin Biere. Weaknesses of CDCL solvers. In Fields Institute Workshop on Theoretical Foundations of SAT Solving, 2016.
- 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.
- Niklas Een and Armin Biere. Effective preprocessing in SAT through variable and clause elimination. SAT, 3569:61–75, 2005.
- 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.
- 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.
- 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!

## Contributors

- Drahomír Hanák <drahomir.hanak@gmail.com>
- Martin Blicha <blicha@d3s.mff.cuni.cz>
- Jan Kofroň <jan.kofron@d3s.mff.cuni.cz>