search

meelgroup / bosphorus

Bosphorus, ANF simplifier and solver, and ANF-to-CNF converter
Other
67 stars 18 forks source link

Number of variables #16

Closed saadislamm closed 4 years ago

saadislamm commented 4 years ago

I have a system of equations with 100 variables out of which I have fixed 25 variables and simplified the system of equations. Bosphorus still shows 100 variables instead of 75, as it looks at the indexes rather than counting the number of actual variables. Should I write a program to rename my whole system to a lower number of variables from x1 to x75 or does bosphorus handles it internally? I was wondering that it might be creating the missing variables by itself and taking more time to solve.

msoos commented 4 years ago

Hey,

It does that automatically internally. It leaves your variable numbering intact so if you want to use another system to solve it, you will be able to map the solutions back. However, internally it discards those 25 variables. I hope this helped!

Mate

msoos commented 4 years ago

Oh, by the way, do try refreshing the system -- I have just released a newer CryptoMiniSat that should be faster :) Cheers,

Mate

saadislamm commented 4 years ago

When we run the following command:

./bosphorus --allsol --anfread equations.txt --anfwrite out.anf --cnfwrite out.cnf --solvewrite solution

which sat solver is used by default? Because I noticed that even after deleting my CryptoMiniSat folder, it is still giving me solutions. How to set it to CryptoMiniSat? Or it has to be used independently?

msoos commented 4 years ago

It always uses CryptoMiniSat. It uses your installed CryptoMiniSat library. You probably have the library somewhere, e.g. at /usr/local/lib or /usr/lib/. Look for libcryptominisat5 :)