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, instead it is here.

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.

**Quickest build (auto-fetch the FetchContent-capable deps):

mkdir build && cd build
cmake ..
make -j8

To build a static binary, you first need to build GMP with static library support:

wget https://ftp.gnu.org/gnu/gmp/gmp-6.3.0.tar.xz
tar xf gmp-6.3.0.tar.xz
cd gmp-6.3.0
./configure --enable-static --enable-cxx --enable-shared --with-pic
make -j8
sudo make install
cd ..

Then point CMake to the installed GMP static libraries (note: use /usr/local/lib/, not a custom build directory, as those may be compiled for the wrong architecture):

mkdir build && cd build
cmake -DBUILD_SHARED_LIBS=OFF \
    -DGMPXX_LIBRARY=/usr/local/lib/libgmpxx.a \
    -DGMP_INCLUDE_DIR=/usr/local/include \
    ..
make -j8

Run it on your instance and it will write a simplified CNF with a reduced independent set:

$ ./arjun input.cnf output.cnf
c o [arjun] Input file: input.cnf
c o [arjun] Output file: output.cnf
[...]
c o [arjun] dumped simplified problem to 'output.cnf'
c o [arjun] All done. T: 1.04

All of Arjun's own log lines start with c o (comment + o for "output"). The simplified CNF written to output.cnf will contain (among other things) a line such as:

c p show 1 4 5 20 31 0
c p optshow 1 4 5 20 31 7 0
c MUST MULTIPLY BY 1024 0

c p show is the reduced independent / projection set (see the Headers section below). The c MUST MULTIPLY BY 1024 0 line says the count of the simplified CNF must be multiplied by 1024 in order to get the correct count of the original formula. If you forget to multiply, the count will be wrong.

In case you are only interested in a reduced independent set (no simplified CNF output), omit the output file:

$ ./arjun input.cnf
[...]
c o [arjun] final set size:       5 percent of original:  1.000 %
c p show 1 4 5 20 31 0
c p optshow 1 4 5 20 31 7 0
c MUST MULTIPLY BY 1
c o [arjun] All done. T: 1.04

Arjun does not write an output file in this mode; the reduced projection set is printed to stdout as c p show ... 0.

Beyond the standard p cnf header and clauses, Arjun's DIMACS parser understands the following comment-style extensions:

Arjun supports several top-level modes, selected via command-line flags:

• Default (unweighted model counting preprocessing) — minimize the independent set and simplify the CNF while preserving its model count.

• Weighted counting — pass --mode 1. Required if your input uses c p weight lines or c t wmc / c t pwmc. Weights are tracked through simplification.

• ApproxMC preset — pass --appmc. Sets simplification defaults tuned for use as an ApproxMC front-end (different oracle / Puura iteration settings).

• Synthesis (--synth) — instead of producing a simplified CNF, compute a Boolean function for each defined (non-input) variable in terms of the projection-set variables (Manthan-style counterexample-guided repair). When an output path is given, Arjun writes a Verilog file with the synthesized functions:

  ./arjun --synth input.cnf output.v