Tag: Grain of Salt
-
Fun facts about SAT solving (part 1)
Last time I gave a talk, I got some quite deserved fire about the way I approach SAT solving: in a more practical than scientific way. So, to give some food for thought for those who wish to approach SAT from a more scientific viewpoint, and to demonstrate to what lengths I have gone to […]
-
ANF to CNF conversion
Algebraic Normal Form, or simply ANF, is the form used to describe cryptographic functions. It looks like this: Where are binary variables, the sign is binary XOR, and the sign is binary AND. Every item that is connected with the XOR-s is called a monomial, and its degree is the number of independent variables inside […]
-
Gaussian elimination is released
The new CryptoMiniSat, version 2.4.2 now has on-the-fly Gaussian elimination compiled in by default. You can simply use it by issuing e.g. ./cryptominisat –gaussuntil=100 trivium-cipher.cnf and enjoy outputs such as:c gauss unit truths : 0c gauss called : 31323c gauss conflicts : 5893 (18.81 %)c gauss propagations : 7823 (24.98 %)c gauss useful : 43.79 […]