After greeting

[ImposterMido]

Sorry I can’t interpret -vH and -vM mapping into binary variables and bits could you please explain to me how determine exactly what are variables that contribute and make both hash and message variables, Thanks in advance !

[vsklad]

Named variable values can be specified in a few different forms, I will use binary and hexadecimal representation as examples.

-vH 0b010…000

The 0b prefix means that the subsequent characters represent binary values, 0=false, 1=true.

The variable H is defined (predefined) by the tool in the CNF file itself and is a sequence of 160 binary variables grouped into 5 32-bit words. Big-endian order applies, that is, the highest word comes first and the highest bit of each word comes first in the sequence. Therefore, any H value specified in the command line must be 160 bit long. In the above example, the “…” must be replaced with other 154 binary values such that the total number of bits (binary variable values) is 160.

Applying big endian order, the first binary value (0) is mapped to the first variable listed in the H definition from the CNF file which is also the highest bit of the first (highest) word of H. The second binary value (1) is mapped to the second highest bit of H and so on. The 160th (last) binary value is mapped to the lowest bit of the lowest word comprising H.

From practical perspective, it is difficult to operate with sequences of binary values as they are too long. For this reason, the tool supports hexadecimal format as well, although the mapping remains essentially the same. Each hexadecimal character represents sequence of 4 binary values and is mapped to 4 binary variables accordingly.

-vH 0x8dc19dbaebdceb30360c0e52c97dd6944e9889e9

The 0x prefix means that the subsequent characters specify hexadecimal value. The first hexadecimal digit is 8 which is equivalent to 0b0100. The same way, 0x8d is equivalent to 0b10001101 and so on.

The value in the above example consists of 40 hexadecimal digits each representing 4 bits (binary variable values) and therefore the whole value represents a sequence of 160 binary variable values.

M is another variable defined in the same way. It has a length of 512 bits grouped into 16 words 32 bits each and mapped to the corresponding sequence of binary variables as defined in the CNF file.

[ImposterMido]

I am afraid you got me wrong i mean the var of H and M in the cnf output file that determine which variables constitute each of H and M for example -vM {{1/32/1}/8/32 and so on all i need to know how to get exactly each and every variable of the 512 bit of M and 256 of H and if it is possible to print it out in a file separately contain all H variables by name and M by name

[ImposterMido]

So when i try to encode the hash and message values manually i know how to assign each variable with the specific value of it ( i know i can assign it by tool but i need to try manually)

[vsklad]

-vM {{1/32/1}/16/32}

It is interpreted as follows:

The innermost sequence of binary variable numbers is {1/32/1}. This means a sequence of 32 variables, the first one is 1, the increment is also 1. It is equivalent to {1, 2, 3, … 32}.

The outermost sequence is {…/16/32} i.e. it is a repetition of the inner sequence 16 times with increment 32 applied to each binary variable each time. The second element of this sequence will therefore be: {33, 34, 35, … 64} and so on.

Altogether the 16 elements with 32 variables each in this case constitute a sequence of binary variable numbers from 1 to 512. That is, the first value (highest bit of the first word of M) corresponds to binary variable number 1, the second highest to binary variable number 2 and so on. The last (lowest) bit of the last word of M corresponds to binary variable number 512.

[ImposterMido]

Thanks a lot but sometimes the variables can be as follows ended by /490 or /553 only i cant relate to it , regarding hash variables sometimes the 32bit words is as follow {{41290/31/-2}, -41150} regarding the -2 what does it exactly means and regarding -41150 does it mean that it is the negation of the actual value of 41150 so it is 1 so its constant to be negation so its 0 and vise versa if its zero in the so it equals to 1

[ImposterMido]

Also when encoding sha256 as 1014 bit message the hash values are {96500/32/-2}\7\63 how does this count for 256 bit ?

[vsklad]

{{41290/31/-2}, -41150}

It is interpreted as follows: {41290/31/-2} is a sequence of 31 binary variables, the first one is number 41290, the increment is -2. This corresponds to the sequence: {41290, 41288, 41286, … 41230}

Then the last element is -41150 which means binary variable number 41150 negated.

Because the tool defines the structure for M and H, the additional inner levels of the sequence expression is “flattened” to match that structure I.e. the whole expression corresponds to the sequence of 31+1=32 elements:

{41290, 41288, 41286, … 41230, -41150}

[vsklad]

{96500/32/-2}/7/63

Exactly the same rules apply. This expression is a sequence of 7 words 32 bits each. The first word is {96500, 96498, 96496,… 96438} Each subsequent word is obtained by adding 63 to each variable number in the preceding word.

[ImposterMido]

So to sum up to make sure i am getting you right 1- the /63 means that next word start as 96563 and so on is that right ? 2- the -41150 the variable is negated meaning that if the hash value binary values translates so 41150 is 1 so the the end of the word is opposite to it 0 and if its 0 so the last one is -41150 so 1 is that right ?

[vsklad]

1 - yes 2 - to avoid confusion, if the last bit of the word is 0 then this corresponds to expression -41150, that is, the binary variable 41150 negated, which means that the value of the binary variable 41150 is 1. Vice versa, if the last bit of the word is 1 then the value of the binary variable 41150 is 1.

[ImposterMido]

Thanks for your help but the last question and sorry for any inconvenience, since i know all the variable that corresponds to hash and message can i use the hash variables as input to the message of another instance any ideas to utilize this idea ?

[ImposterMido]

In order to utilize this idea the only problem is the - variables thats why i asked a-lot about it

[vsklad]

I understand you would like to combine two CNF SAT instances into one, mapping a subset of variables from one instance to a subset of the variables in the other instance. Also, I assume that this is not about encoding multi-block messages because the tool already supports that.

Assuming that each instance has unique variable numbers without overlap, the clauses from the two CNF files can be concatenated, and equality clauses added for each pair of the variables: 1 -10000 0 -1 10000 0 which states that the variable 1 is equal to the variable 10000.

OR 1 10000 0 -1 -10000 0 which means that the variable 1 is equal the variable 10000 negated.

However, the variable numbers do overlap. To overcome this, you can probably: 1) modify the tool to encode different instances using different ranges of variable numbers OR 2) modify the tool to encode the two instances together OR 3) make your own tool that would reassign variable numbers in an instance to be from the desired range

[vsklad]

actually, I forgot to mention, you can avoid negated variables in the sequence definitions using a command line parameter:

    -n | --normalize_variables
        reindex binary variables such that no negations are present 
        within named variable definitions within the output file;
        may add aditional clauses/equations as necessary
        supported for encode/process commands

[ImposterMido]

Since i am not able to modify this code unfortunately, i was thinking of 2 ways 1- since the first instance will end with variables 41000 and for example the hash variables are 40744 to 41000 so to use it as message variables i will rename the M variables of second instance which starts from 1 till 256 to be 40744 till 41000 and then the rest of variables are changed accordingly so the new instance will be as extension of the 1st instance and the H variables of 1st instance are the same of M of 2nd one what do you think of that ?

[vsklad]

sure this should be fine

[ImposterMido]

Could you please give me example of the command including normalizing variables ! by this way the message and hash could be assigned and by solving an instance which has no specific message or hash when I interpret the variables that corresponds to M and H i got the hash and its pre image (message) is that right if so i will try tomorrow and confirm with you if every thing is ok to close the issue thanks for help can’t be more grateful !

[ImposterMido]

Sorry for inconvenience to make it easier is there any way to make the -vH bits are always the last 256 bits of the encoded instance so if it has 41500 variables variables from 41244 to 41500 are hash bits and so the message variables according to block size to be the first … bits ? of course without affecting the quality of the encoded instance

[vsklad]

1) please just add "-n" to the command line 2) unfortunately the tool does not support this; you can do this manually if you wish by introducing additional variables and adding clauses that define equivalence, e.g. if you add variables 100000...100159 and the first bit of H is represented by variable 41500 then the following clauses should be added: 41500 -100000 0 -41500 100000 0

[ImposterMido]

Thanks very much for your help !