Program
Verification
Book

PV4 ⊧ lingelingproduces a satisfiability result for a formula

SAT solver

Application domain/field

SAT solving
Boolean Satisfiability problem

Type of tool

SAT solver

Expected input

SAT problem

Expected output

SATISFIABLE, UNSATISFIABLE or UNKNOWN indicating whether the SAT problem is satisfiable, unsatisfiable or it couldn't be determined.

Comments

Released under the MIT license

Links

Project page: http://fmv.jku.at/lingeling/
Repository: 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/Biere-SAT-Competition-2018-solvers.pdf (SAT Competition '18)
http://fmv.jku.at/papers/Biere-SAT-Competition-2017-solvers.pdf (SAT Competition '17)
http://fmv.jku.at/papers/Biere-SAT-Competition-2016-solvers.pdf (SAT Competition '16)
Clause Elimination for SAT and QSAT (JAIR '15)

Last publication date

2018

Related tools

plingeling: Parallel front-end

ProVerB specific

Markdown description: view/edit
Reason for this entry: used by Alloy Analyzer
Contained in the ProVerB22 dataset (paper + artefact)

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