PV4 ⊧ Glucoseproduces a satisfiability result for a formula in CNF

Application domain/field

SAT solving

Type of tool

SAT solver

Expected input

CNF file

Format:

DIMACS format

Expected output

UNSAT or SAT. In case the output is SAT, you can also print the solution.

Internals

Heavily based on MiniSat