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

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!

Contributors

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

Repositories

• https://github.com/d3sformal/yaga

Contact

• Martin Blicha
• Jan Kofroň