TO DO
Historic note: Indra is originally, an ANF simplification tool forked from https://github.com/msoos/anfconv.
- Use
m4ri-20140914.tar.gz
andpolybori-0.8.3.tar.gz
that we have downloaded before-hand and uploaded into this repository - Use the bash script
setup.sh
which runs all commands below in sequential order (Includessudo
commands) - [Strongly recommended] Take a look at
setup.sh
and modify accordingly before executing
From https://bitbucket.org/malb/m4ri/downloads/, download m4ri-20140914.tar.gz
tar -xf m4ri-20140914.tar.gz
cd m4ri-20140914
./configure
make
sudo make install
From https://sourceforge.net/projects/polybori/files/polybori/0.8.3/, download polybori-0.8.3.tar.gz
tar -xf polybori-0.8.3.tar.gz
cd polybori-0.8.3
sudo scons devel-install
git clone https://github.com/msoos/cryptominisat.git
cd cryptominisat
mkdir build
cd build
cmake ..
make -j4
sudo make install
Note (For MacOS): If you encounter cryptominisat.h:30:10: fatal error: 'atomic' file not found
in #include <atomic>
during compilation, you may need to use CFLAGS='-stdlib=libc++' make
instead of just make
.
git clone https://github.com/cxjdavin/indra.git
cd indra
mkdir build
cd build
cmake ..
make -j4
Use cmake -DSTATICCOMPILE=ON ..
instead if you wish to compile statically. You may now run using the executable indra
in the build
directory.
Must have LLVM lit and stp OutputCheck. Please install with:
pip install lit
pip install OutputCheck
Run test suite via lit indra/tests
Suppose we have a system of 2 equations:
- x1 + x2 + x3 = 0
- x1 * x2 + x2 * x3 + 1 = 0
Write an ANF file readme.anf
as follows:
x1 + x2 + x3
x1*x2 + x2*x3 + 1
Running ./indra --anfread readme.anf --anfwrite readme.anf.out --custom --elsimp
will apply only the ElimLin simplification (ignoring other processes that the tool offers) to readme.anf
and write it out to readme.anf.out
. readme.anf.out
will then ßcontain the following:
c Executed arguments: --anfread readme.anf --anfwrite readme.anf.out --custom --elsimp
c -------------
c Fixed values
c -------------
x(2) + 1
c -------------
c Equivalences
c -------------
x(3) + x(1) + 1
c UNSAT : false
Explanation of simplification done:
- The first linear polynomial rearranged to
x1 = x2 + x3
to eliminate x1 from the other equations (in this case, there is only one other equation) - The second polynomial becomes
(x2 + x3) * x2 + x2 * x3 + 1 = 0
, which simplifies tox2 + 1 = 0
- Then, further simplification by substituting
x2 + 1 = 0
yieldsx1 + x3 + 1 = 0
The output of readme.anf.out
tells us that
- x2 = 1
- x1 != x3
i.e. There are 2 solutions:
- (x1, x2, x3) = (1,1,0)
- (x1, x2, x3) = (0,1,1)
See ./indra -h
for the full list of options.
(Note: Level N also prints everything from Level 0 to Level N-1)
Error messages
Basic ANF/CNF statistics
Some simplification information (e.g. Summary of each simplification step)
More detailed simplification information (e.g. Prints matrix sizes)
Even more detailed simplification information (e.g. Prints matrix before and after Gauss Jordan Elimination)
Warning! Data dump from this point onwards
- PolyBoRi cannot handle ring of sizes over approx 1 million (1048574). Do not run
indra
on instances with over a million variables.