Q3B-pBDD is an SMT solver based on Q3B, making use of partial BDDs instead of pairs of BDDs representing lower and upper bounds of a formula's model set. As well as Q3B, it is based on the CUDD library, which has been modified to cope with partial BDDs for this purpose.
The solver has been created at the Faculty of Informatics, Masaryk University as part of Matěj Pavlík's bachelor's thesis under Jan Strejček's supervision. (In the thesis, partial BDDs are called '3-valued BDDs'.)
Q3B-pBDD available at https://github.com/matejpavlik/Q3B
CUDD-3val available at https://github.com/matejpavlik/cudd-3val
Further algorithms for the tool have been developed under the Dean's Project "Vývoj nástroje Q3B s částečnými BDD".
Technical details and the code of the algorithms are published in this document (in Czech).