# 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

Remco Bloemen
Math & Engineering
https://2π.com