A new symmetry detecting and breaking library. This is based on Jo Devriendt's BreakID code. It has been re-licensed by the original author to be MIT and hence it's realeased as MIT here. All modifications by Mate Soos.
git clone https://github.com/meelgroup/breakid
cd breakid
mkdir build && cd build
cmake ..
makeBreakID detects symmetries in your input CNF file and creates a new CNF file that has your original CNF in it, along with some new variables and clauses that help break most symmetries:
./breakid myfile.cnf symmetry-broken-output.cnf
c BreakID version [...]
c Detecting symmetry groups...
c Finished symmetry breaking. T: 3.78 s T-out: N T-rem: 1.00
c Num generators: 42
[...]
c Constructing symmetry breaking formula...
[...]
c regular symmetry breaking clauses added: 3007
c row interchangeability breaking clauses added: 0
c total symmetry breaking clauses added: 3007
c auxiliary variables introduced: 988The symmetry-broken CNF has been written to symmetry-broken-output.cnf. This
CNF has 3007 more clauses and 988 extra variables. The system took 3.78s to
find the generators for the symmetries, and it found a total of 42 generators.
In case you are interested in the generators, you can increase verbosity with
--verb N, and see the generators themselves.
If you run ./breakid with the option --help, you will be given all the
different options your can pass.
Check out the breakid-main.cpp file for example usage and the breakid.hpp
header file for the API. The library should be fairly simple to use, but please do
ask away in case something is unclear.
To obtain the example CNFs:
git submodule update --init
cd examples
This folder contains highly symmetrical test cnfs. Particular attention goes to instances in channel and counting, which both exhibit row interchangeability due to high-level variable or value interchangeability.