PV4 ⊧ ParaFROSTproduces a satisfiability result for a formulaSAT solver that uses Conflict Driven Clause Learning (CDCL) with GPU acceleration of pre- and inprocessing, tuned for bounded model checking.
- SAT solving
- Boolean satisfiability
Type of toolSAT solver
UNSATISFIABLE or an error indicating e.g. out of memory or a timeout.