Software related to PhD Thesis Extending SAT Solver with Parity Reasoning
- cnf2cnf : fixes DIMACS cnf header clause and variable counts
- cnf2xcnf : extracts xor-constraints from CNF
- ec-minisat : minisat 2.0 with EC xor-deduction system
- subst-minisat : minisat 2.0 with SUBST xor-deduction system
- translations : translations to simulate EC and IGJ xor-deduction systems by adding redundant xor-constraints and auxiliary variables
- up-dsimplex-minisat : minisat 2.0 with incremental Gauss-Jordan elimination (IGJ xor-deduction system)
- up-minisat : minisat 2.0 with UP xor-deduction system
- xcnf-biconnected : finds biconnected xor-constraint components
- xcnf-clusters : finds connected xor-constraint components (also tool for extracting junction tree)
- xcnf-elim-internal : eliminates variables in XCNF that occur only in xor-part
- xcnf-matrix-sizes : computes matrix sizes of a given XCNF
- xcnf-preprocess : propagates unary and binary xor-constraints
- xcnf-simplify : performs propagation-preserving xor-simplification
- xcnf2cnf : complete or partial XCNF to CNF translation
- xcnf3xcnf : translates XCNF to 3-xor-normal form
The software is released under General Public License (version 3). See LICENSE for details.