How to count the number of solutions to an ANF input?

[msoos]

Basically, you can translate your ANF to CNF, and that CNF will have a "c ind X Y Z 0" line. You can now read this CNF with CryptoMiniSat and get all the solutions:

soos@tiresias:build$ cat a.anf
x1 + x2 + x3 + x0
x1 + x2 + 1
soos@tiresias:build$ ./bosphorus --anfread a.anf --cnfwrite a.cnf
c Bosphorus SHA revision 47edb6b2cd98c6fbc3bffcc35dbf2569bc29f58e
c Executed with command line: ./bosphorus --anfread a.anf --cnfwrite a.cnf
[...]
soos@tiresias:build$ cat a.cnf
p cnf 4 4
2 3 0
-2 -3 0
1 4 0
-1 -4 0
c ind 1 2 3 4 0
soos@tiresias:build$ ./cryptominisat5 --maxsol 1000 a.cnf
[...]
c Number of solutions found until now:      4
s UNSATISFIABLE

So this means, the original ANF had 4 solutions. If the original ANF has many solutions, you can use ApproxMC to count the number of solutions:

soos@tiresias:build$ ./approxmc a.cnf
[...]
c [appmc] Number of solutions is: 4*2**0
s mc 4

Note that ApproxMC is much more suitable if you have many more solutions.