PV1 S3 (versions: S3P, S3#, S3N)calculates the upper bound for the model count for a given formula

String model counter

Application domain/field

Type of tool

String solver/model counter

Expected input

Format:

Expected output

Upper bound for the model count?

Internals

The model counting problem is about counting the number of satisfiable assignments for a constraint formula. This was built on top of S3P, an earlier version of the same tool, which has been built on top of Z3.

Comments

There is a newer version of this tool available under the name S3N (last release on 26 November 2020).

Links

Related papers

Related tools

ProVerB specific



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