Program
Verification
Book

PV4 ⊧ plingelingproduces a satisfiability result for a formula

Parallel front-end of Lingeling SAT solver

Application domain/field

SAT solving
Boolean satisfiability

Type of tool

SAT solver

Expected input

SAT problem

Format:

Expected output

SATISFIABLE, UNSATISFIABLE or UNKNOWN indicating whether the SAT problem is satisfiable, unsatisfiable or it could not be determined.

Comments

License: MIT license

Links

Project page: http://fmv.jku.at/lingeling/
Repository (also contains Lingeling and Treengeling): https://github.com/arminbiere/lingeling
Last commit date: 15 May 2022 (default branch)
Last commit date: 15 May 2022 (last activity)

Related papers

http://fmv.jku.at/papers/BiereFazekasFleuryHeisinger-SAT-Competition-2020-solvers.pdf (SAT Competition '20)
http://fmv.jku.at/papers/Biere-SAT-Competition-2018-solvers.pdf (SAT Competition '18)
http://fmv.jku.at/papers/Biere-SAT-Competition-2017-solvers.pdf (SAT Competition '17)

Related tools

Lingeling, Treengeling

ProVerB specific

Markdown description: view/edit
Reason for this entry: uses Lingeling
Contained in the ProVerB22 dataset (paper + artefact)

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