Counting the number of solutions after ANF->CNF conversion about bosphorus

[a1880]

Could it be that the number of solutions is higher now due to additional switching variables?
If you sort and filter the solutions with respect to the original input variables, the number of different solutions could be 256 as expected.

Greetings,

Axel

[msoos]

Hi,

First of all, thanks for the message. Indeed, @a1880 is on the right track -- we don't guarantee equivalent number of solutions. However, you can get the number of solutions as well. The way to do this is:

1. Get the CNF from Bosphorus by running: ./bosphorus --anfread myanf.anf --cnfwrite mycnf.cnf --solmap mysolmap.txt

2. Take the solution-var variables in mysolmap.txt, shift them up by 1, and add them to the CNF as c ind VAR1 VAR2 ... VARN 0 For example, if you have:

Internal-ANF-var 7 = solution-var 0
Internal-ANF-var 6 = solution-var 1
Internal-ANF-var 2 = solution-var 2
Internal-ANF-var 8 = solution-var 48
Internal-ANF-var 1 = solution-var 98

Write c ind 1 2 3 49 5 99 at the top of the CNF file (after p cnf ...).

3. Run on CryptoMiniSat with:
   ./cryptominisat --maxsol 1000000 mycnf.cnf

Alternatively, you can run a projected model counter such as ApproxMC, it will use the projection set. This will work much better for large number of solutions (>500).

[msoos]

(Actually, this is such a great question, I will now fix this in the README and make it part of it)

[msoos]

Yay! I have now improved bosphorus so you don't need to do all that complicated stuff above! You can just do this:

./bosphorus --anfread task2.txt  --cnfwrite x.cnf
cryptominisat --maxsol 10000 x.cnf 

The projection set is automatically written to the CNF :) Also, you can use approximate counting too!

./bosphorus --anfread task2.txt  --cnfwrite x.cnf
approxmc x.cnf

I hope this helps. Also, I thanked you personally @hadipourh for this in the commit eaed7ea and added a howto to the README :) Thanks again,

Mate

[hadipourh]

Dear Axel and dear Mate,

Thanks for your answers. The new feature added by Mate, makes the solution counting much easier. I appreciate it a lot.

As far as I know, the problem of ANF to CNF conversion has been well studied so far, and Bosphorus is one of the most efficient tools to do this task. However, to the best of my knowledge Bosphorus uses an extremely naive approach to convert a CNF to ANF in which the given CNF is translated to a set of ANF-s clause by clause. Hence, each clause is converted to an ANF individually without taking into account that whether there is an overlap between multiple clauses. Hence, it'd be very good if Bosphorus could support the more advanced methods such as the one proposed in On conversions from CNF to ANF. So, do you have a plan to improve the CNF to ANF converter of Bosphorus? If so, the Bosphorus will be a great bridge from the world of SAT solvers to the world of Algebraic methods.

Best wishes,
Hosein

[msoos]

Hi,

That sounds like a great project for you to do it! I strongly recommend that you get working at once to implement it. You can start creating a Pull Request once you are done, please see here how:

https://docs.github.com/en/github/collaborating-with-issues-and-pull-requests/creating-a-pull-request

We'll be glad to merge it, in case its quality is such that it can be merged with Bosphorus and it has associated test cases and/or fuzz tests as we have now.

Good luck with the work, and please let us know when you are done,

Mate

[hadipourh]

Hi,

I am creating a new tool in which CNF->ANF conversion is necessary. So, I'm currently implementing the algorithm proposed in On conversions from CNF to ANF. Let me know please if there is a better method.
Given that Polybori is simply accessible via the SageMath, I'd prefer to create a preliminary prototype building upon the SageMath at first. Next, I'll try my best to work on Bosphorus, if I have enough time. I also will be happy if I can add it to the Bosphorus, and will inform you if I could do it.

Kind regards,
Hosein