Generating CNF
% Remco Bloemen % 2015-08-26
https://github.com/msoos/cryptominisat/
Example usage
m = vec_from_hex(
"01000000" +
"xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx0000000000000000" +
"xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx" +
"533bff42" +
"1900db99" +
"________")
h = sha256(m, rounds)
k = sha256(h, rounds)
vec_equals(k[-n:], vec_const(n, 0))
cnf_solve()
Features
SAT solving
- Special argument detection (
cnf_is_special)- One of the arguments is constant
- Some arguments are identical or negatives
Boolean circuits
- Simple boolean operations (
cir_and,cir_nand,cir_or,cir_nor)- Take a variable number of arguments
- Constant propagation False ∧ ⋯ → False
- Recognize cases such as A ∧ ¬A ∧ ⋯ → False
- Reduce redundant clauses B ∧ B ∧ ⋯ → B ∧ ⋯
- Zero overhead when given just one argument
- Complex boolean operations (
cir_xor,cir_xnor)- Reduce redundant clauses A ⊕ A ⊕ A → A
- Reduce redundant clauses A ⊕ ¬A ⊕ ⋯ → True
- Propagate constants A ⊕ True → ¬A
- No temporary variables introduced, but exponential in the number of arguments
- Full-adder (
cir_full_adder)- Optimal circuit without temporary variables in common case
- Fall-back to Tseitin circuit when arguments are special for better constant propagation
Bit vectors
- Bitvectors from hexadecimal (
vec_from_hex)- Unlimited length hexadecimal constants, with:
_meaning a free nibble, to be solved forxmeaning a random nibble
Integers
- Operations on Bitvectors (
vec_and,vec_xor, etc..) - Addition of bitvector (
vec_add) ** - Add do not calculate carry on last bit
