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

Project page: https://www.princeton.edu/~chaff/zchaff.html

Last commit date

Last release mentioned on the project page is from 12 March 2007.

Related papers

https://doi.org/10.1007/11527695_27 (SAT '04)

Last publication date

2004

ProVerB specific

View/edit source (Markdown)



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