Ok I did 1 quick reading on the proposed paper by K2TSET. An guess what just as I said. There are comments that prommest heaven, just as it was mention.
But quickly you see that this one REAL objective is only compare speed of diferent SAT solvers.
As I mention conclusion is more encrypted that the crypto they are trying to break. I ignore none CSA crypto analisys.
But even when it mention
"we were able to break 20 rounds of the CSA block cipher"
"We run the experiments on a Computer with 4 Six-Core AMD Opteron Processors 8435 operating at
2.6 GHZ. This Computer has 64 GB RAM and runs a 64 bit Linux (Ubuntu 13.10) as operating system."
it does not describe the Full Method, tools and file used. In particular set of equation used. on page 41 it show description on "5.1.1 CSA Equation Generator"
Code:
def encodelinear (p):
if p. deg () != 1: raise ValueError ( " polynomial must be of degree 1" )
if
len (p) == 1: #raise ValueError (" polynomial must have length > 1")
v = p. vars_as_monomial (). variables ()[0]
r = str (v. index()+1)+" 0"
if not p. has_constant_part ():
r = "-"+r
return r
var = l i s t (p. vars_as_monomial (). variables ())
idx = [v. index()+1 for v in var ]
if not p. has_constant_part (): #idx [-1] = -idx [-1]
return "x"+("+x" . join (map(lambda x: str (x) , idx )))
else :
return "x"+("+x" . join (map(lambda x: str (x) , idx)))+ "+1"
return p
Is this python?
There is also mention to "5.1.2 Converter of Non-linear Equations to Linear Equations"
Now let me show you my understanding of results from page 43.
I know you focus in:
"In test case20, we notice that Minisat was not able to solve the problem even within 2 weeks. This was
also the case for Cryptominisat3, Lingeling, Glucose and Riss3g. On the other hand Cryptominisat2 was
the fastest sat solver and it needs only 12 hours."
"In fact, we were able in our tests to solve only 20 rounds out of 55 and all 20 cases were
satisfiable."
So you think WAO got the Key on 12 Hours. Let me tell you YOU ARE WRONG. You still do not understand what this is about.
What it said is (satisfiable):
"In fact, we were able in our tests to solve only 20 rounds out of 55 and all 20 cases were
satisfiable."
For them "satisfiable" means a solution. For us "satisfiable" means a "Posible Solution". And a Posible Solution means in reality a FAKE solution with 0.000........0000000000x posibiity that you find the correct one.
PD: important to convince you. YOU will expect that less rounds means less chance to get results. Now look at table in page 43. Lets take MIN column just as an example.
1 round about .009 hours
5 round about .025 hours
10 round about .087 hours
15 round about 9.345 hours
See how it ONLY goes up. You could even conclude 1 round is better!
Conclusion finding a "satisfiable" solution does not mean finding the REAL one.