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. The second best thing to use is Nix. Simply install nix and then:

nix shell github:meelgroup/arjun

Then you will have arjun binary available and ready to use.

If this is somehow not what you want, you can also build it. See the GitHub Action for the specific set of steps.

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.