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 for
  • x meaning 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

Crypto

Full source code