PV4 ⊧ CryptoMiniSatproduces a satisfiability result for a formula in CNF

SAT solver optimized for cryptographic problems

Application domain/field

• SAT solving
• Cryptography

Type of tool

SAT solver

Expected input

Boolean formula in conjunctive normal form (CNF)

Format:

DIMACS format with the extension of XOR clauses.

Expected output

SATISFIABLE, UNSATISFIABLE or UNKNOWN

Internals

They extended the solver's input language with the XOR operation which is often used in cryptographic