v1.2.0

Support for SAT Modulo Symmetries for isomorph-free graph generation subject to QBF constraints. See also the AAAI 2025 paper titled Breaking Symmetries in Quantified Graph Search: A Comparative Study.

Out-of-order decisions

This release contains the version of the solver used for the paper titled 'Should Decisions in QCDCL Follow Prefix Order?' In particular, it contains the new feature of being able to make variable decision irrespective of dependencies, whether implicit or learned. This is activated with --out-of-order-decisions off|existential|universal|all. For this, the 3-watched-literal data structure was implemented, and it is automatically used when out-of-order decisions are active. It is also possible to run in ordinary dependencies-respecting mode with 3 watched literals, using --watched-literals 3.