Counting the number of solutions after ANF->CNF conversion

[hadipourh]

Hi,

I'd like to use the Bosphorus as a CNF to ANF converter in my new tool. However, I want to become sure whether the CNF reader works correctly. The following example taken from the previous closed issues represents that the CNF reader doesn't work properly. It should be noted that I reproduced the following results via the new version and noticed that there is still the same issue in the new version.

The attached file, contains the CNF of Skinny-128 Sbox in 'dimacs' format. The number of solutions for the given CNF must be 256, since it actually describe an 8-bit Sbox, and it is known that the number of possible (input, output) pairs, for a given 8-bit bijective Sbox must be 256. The CNF file has been attached, however you can reproduce it via the following command in SageMath:

from sage.crypto.sbox import SBox
s = SBox([0x65 , 0x4c , 0x6a , 0x42 , 0x4b , 0x63 , 0x43 , 0x6b , 0x55 , 0x75 , 0x5a , 0x7a , 0x53 , 0x73 , 0x5b , 0x7b ,0x35 , 0x8c , 0x3a , 0x81 , 0x89 , 0x33 , 0x80 , 0x3b , 0x95 , 0x25 , 0x98 , 0x2a , 0x90 , 0x23 , 0x99 , 0x2b ,0xe5 , 0xcc , 0xe8 , 0xc1 , 0xc9 , 0xe0 , 0xc0 , 0xe9 , 0xd5 , 0xf5 , 0xd8 , 0xf8 , 0xd0 , 0xf0 , 0xd9 , 0xf9 ,0xa5 , 0x1c , 0xa8 , 0x12 , 0x1b , 0xa0 , 0x13 , 0xa9 , 0x05 , 0xb5 , 0x0a , 0xb8 , 0x03 , 0xb0 , 0x0b , 0xb9 ,0x32 , 0x88 , 0x3c , 0x85 , 0x8d , 0x34 , 0x84 , 0x3d , 0x91 , 0x22 , 0x9c , 0x2c , 0x94 , 0x24 , 0x9d , 0x2d ,0x62 , 0x4a , 0x6c , 0x45 , 0x4d , 0x64 , 0x44 , 0x6d , 0x52 , 0x72 , 0x5c , 0x7c , 0x54 , 0x74 , 0x5d , 0x7d ,0xa1 , 0x1a , 0xac , 0x15 , 0x1d , 0xa4 , 0x14 , 0xad , 0x02 , 0xb1 , 0x0c , 0xbc , 0x04 , 0xb4 , 0x0d , 0xbd ,0xe1 , 0xc8 , 0xec , 0xc5 , 0xcd , 0xe4 , 0xc4 , 0xed , 0xd1 , 0xf1 , 0xdc , 0xfc , 0xd4 , 0xf4 , 0xdd , 0xfd ,0x36 , 0x8e , 0x38 , 0x82 , 0x8b , 0x30 , 0x83 , 0x39 , 0x96 , 0x26 , 0x9a , 0x28 , 0x93 , 0x20 , 0x9b , 0x29 ,0x66 , 0x4e , 0x68 , 0x41 , 0x49 , 0x60 , 0x40 , 0x69 , 0x56 , 0x76 , 0x58 , 0x78 , 0x50 , 0x70 , 0x59 , 0x79 ,0xa6 , 0x1e , 0xaa , 0x11 , 0x19 , 0xa3 , 0x10 , 0xab , 0x06 , 0xb6 , 0x08 , 0xba , 0x00 , 0xb3 , 0x09 , 0xbb ,0xe6 , 0xce , 0xea , 0xc2 , 0xcb , 0xe3 , 0xc3 , 0xeb , 0xd6 , 0xf6 , 0xda , 0xfa , 0xd3 , 0xf3 , 0xdb , 0xfb ,0x31 , 0x8a , 0x3e , 0x86 , 0x8f , 0x37 , 0x87 , 0x3f , 0x92 , 0x21 , 0x9e , 0x2e , 0x97 , 0x27 , 0x9f , 0x2f ,0x61 , 0x48 , 0x6e , 0x46 , 0x4f , 0x67 , 0x47 , 0x6f , 0x51 , 0x71 , 0x5e , 0x7e , 0x57 , 0x77 , 0x5f , 0x7f ,0xa2 , 0x18 , 0xae , 0x16 , 0x1f , 0xa7 , 0x17 , 0xaf , 0x01 , 0xb2 , 0x0e , 0xbe , 0x07 , 0xb7 , 0x0f , 0xbf ,0xe2 , 0xca , 0xee , 0xc6 , 0xcf , 0xe7 , 0xc7 , 0xef , 0xd2 , 0xf2 , 0xde , 0xfe , 0xd7 , 0xf7 , 0xdf , 0xff])
print(s.cnf(format = 'dimacs'))

CNF file: skinny64_sbox.zip I solved the above SAT problem via your nice tool, called CryptoMiniSat5 with the following command:

cryptominisat5 --verb 0 --maxsol 500 skinny64_sbox.cnf > solutions.txt

As you can see in solutions.zip, there are only 256 different solutions for this SAT problem. Let's simplify this CNF with the Bosphorus, to see whether it keeps the number of solutions unchanged or not. I simplified it via the following command:

./bosphorus --cnfread skinny64_sbox.cnf --cnfwrite simplified.cnf

The simplified version of the above SAT problem, has been included in the simplified.zip. When I solved the simplified.cnf with the CryptoMiniSat5, I observed that it has more than 256 solutions. I solved it via the following command:

cryptominisat5 --verb 0 --maxsol 500 simplified.cnf > solutions1.txt

As you can see in solutions1.txt file, there are more than 256 different solutions for the simplified CNF! So, I think the Bosphorus doesn't prereserve the equality. Let me know if I am wrong please.

Kind regards, Hosein

Originally posted by @hadipourh in https://github.com/meelgroup/bosphorus/issues/11#issuecomment-594105794

[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 eaed7eac38f319728721136b5597b160228f6a8c 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