PV4 ⊧ zChaff (or any alternative capitalisation)produces a satisfiability result for a formula in CNF

SAT solver

Application domain/field

Type of tool

SAT solver

Expected input

SAT problem

Format:

CNF file

Expected output

SAT, UNSAT, ABORT : TIME OUT, ABORT : MEM OUT, UNKNOWN indicating whether the SAT problem is satisfiable, unsatisfiable, or it could not be determined.

Internals

zChaff is an implementation of the Chaff algorithm.
SAT

Links

Related papers

Zchaff2004: An Efficient SAT Solver (SAT '04)

Last publication date

2004

ProVerB specific


ProVerB is a part of SLEBoK. Last updated: February 2023.