A minimal independent set calculator and CNF minimizer that uses a combination of steps to simplify a CNF such that its count stays the same. Name is taken from the Hindu myth where Arjun is known for being the "one who concentrates the most". This system is also used as a preprocessor for our tool ApproxMC and should be used in front of GANAK. For the paper, see here.
Note that the simplification part of Arjun contains code from SharpSAT-td by Tuukka Korhonen and Matti Jarvisalo, see this PDF and this code for details. Note that treewidth-decomposition is not part of Arjun.
It is strongly recommended to not build, but to use the precompiled binaries as in our release. In case you need to build, please see the GitHub Actions file for instructions.
Run it on your instance and it will give you a reduced independent set:
$ ./arjun input.cnf output.cnf
c [arjun] original sampling set size: 500
c ind 1 4 5 20 31 0
[...]
c [arjun] Done dumping. T: 1.0406
This means that your input independent set of your input formula input.cnf,
which had a size of 500 has been reduced to 5, which is ony 1% of the original
set. The simplified formula with the smaller independent set has been output to
output.cnf. The final simplified will contain a line such as:
c MUST MULTIPLY BY 1024
This means that the final count of the CNF must be multiplied by 2^10 (i.e. 1024) in order to get the correct count. Note that if you forget to multiply, the count will be wrong. So you must multiply.
In case you are only interested in a reduced independent set, use:
$ ./arjun input.cnf
c [arjun] original sampling set size: 500
c ind 1 4 5 20 31 0
This will not write an output file, but only display the reduced independent set.