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


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


Related papers

Last publication date


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.