PV4 CaDiCaLproduces a satisfiability result for a formula

SAT solver uses Conflict Driven Clause Learning (CDCL) and inprocessing, built with the main aim being clean, understandable and modifiable.

Application domain/field

SAT solving

Type of tool

SAT solver

Internals

Local search, target phases (generalisation of phase saving), rephasing, lucky phase detection, bounded variable elimination, failed literal probing, clause subsumption/vivification, chronological backtracking, incremental solving, model based testing. License: MIT
SAT

Links

Related papers

Last publication date

2019

Related tools

ParaFROST (extension), Mobical (integrated model based tester), YalSAT (earlier experiment with local search), Lingeling (earlier experiment with lucky phases)

ProVerB specific



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