PV4 CryptoMiniSatproduces a satisfiability result for a formula in CNF

SAT solver optimized for cryptographic problems

Application domain/field

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
SAT

Links

Last commit date

7 October 2021

Related papers

https://doi.org/10.1007/978-3-642-02777-2_24 (SAT '09)

Last publication date

2009

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.