PV2 PCSatgenerates an SMT problem from a pfwCSP spec, requires an external solver

Satisfiability checking tool for pfwCSP based on stratified Counterexample-guided Inductive Synthesis (CEGIS).

Application domain/field

Type of tool

Satisfiability checker (for pfwCSP)

Expected input


Expected output

sat, unsat or unknown?


Uses Z3 pfwCSP: new class of predicate Constraint Satisfaction Problems. This allows constraints that are arbitrary (i.e. possibly non-Horn) clauses modulo first-order theories over predicate variables that can be functional predicates, well-founded predicates or ordinary predicates. This is a generalization over Constrained Horn Clauses.


Note: the authors sometimes call PCSat a (second-order) constraint solver


Related papers

Constraint-Based Relational Verification (CAV '21)

Last publication date

15 July 2021

ProVerB specific

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