Generating CNF

Remco Bloemen

2015-08-26

https://github.com/msoos/cryptominisat/

Example usage

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