markusa4/satsuma: satsuma version 1.4

Read full text
Authors: Markus Anders
Cited by: 0

Abstract

New fixing mode Added a new symmetry-breaking mode: fix. Fixing performs symmetry breaking by adding unit and binary clauses. Users now explicitly choose between fixing and lex-leader constraints. The fixing algorithm automatically iterates. The implementation is tightly integrated with the Schreier-Sims algorithm from dejavu. Support for substitution redundancy proofs in fixing mode, both binary and ASCII. The fixing approach is covered in detail in the SAT 2026 and TACAS 2026 papers. Cliquer Cliquer can be optionally compiled with the project Options --reorder and --reorder-cliquer control reordering of matrix models using clique-based heuristics General Added support to remove (explicit) equivalent literals --preprocess-cnf-eq Added and lowered many limits after large-scale testing on Anniversary track Bug fixes Added many smaller fixes and robustness improvements. Improved handling of edge cases in specialized detection algorithms.

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
14 May 2026