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