Approach

PB/CT implements the technique described in "Satisfiability Modulo the Theory of Costs: Foundations and Applications" by Cimatti et al (TACAS'10), which describes the theory of Costs.

This is a theory which seamlessly extends SMT solvers based on the DPLL(T) schema with the ability to reason with Pseudo-Boolean functions allowing for solving of optimization, Max-SMT, and related problems.

Motivation

The ideas described in the above mentioned paper have been implemented in the MathSAT SMT solver. It would be interesting to see how the theory of costs performs in other implementations of the DPLL(T) schema, and PB/CT is an attempt to validate this using the OpenSMT SMT solver as well as providing a basic open-source implementation of the theory of costs.

PB/CT implements a basic front-end to the SMT solver with a straight-forward translation of Pseudo-Boolean problems into SMT(Costs) as a basic example of the usage of the theory.

Download

Version 0.1.3 (2012-05-23)

• opensmt-ct-0.1.2.tgz (source code)
• pbct-0.1.2.tgz (source code)
• pbct-0.1.2-linux32.bz2 (32-bit Linux binary)

Version 0.1.2 (2010-07-06)

• opensmt-ct-0.1.2.tgz (source code)
• pbct-0.1.2.tgz (source code)
• pbct-0.1.2-linux32.bz2 (32-bit Linux binary)

Version 0.1.1 (2010-06-25)

• opensmt-ct-0.1.1.tgz (source code)
• pbct-0.1.1.tgz (source code)
• pbct-0.1.1-linux32.bz2 (32-bit Linux binary)

Version 0.1 (2010-06-12)

• opensmt-ct-0.1.tgz (source code)
• pbct-0.1.tgz (source code)
• pbct-0.1-linux32.bz2 (32-bit Linux binary)

License

PB/CT is released under the Gnu Public License, version 3.

Compilation

In order to compile PB/CT, you will need

• g++ version >= 4.3.2
• flex
• bison
• libtool
• The Gnu MP library, compiled with support for C++
• cmake

The solver can be built with the following sequence of commands:

Usage

pbct [options] file

--algorithm=type	Choose optimization algorithm. Can be one of linear (default), binary or adaptive which performs optimization using linear, binary and a simple heuristic algorithm respectively.
--bound=integer	Set an upper bound on the objective function, if any.
--model	Print the model, if satisfiable. If optimizing, will print the optimal model if one is found, or the currently best model if interrupted.
--opensmt-verbose=integer	Set verbosity for OpenSMT. If greater than 0, the output will no longer conform to the rules of the Pseudo-Boolean competition.

Acknowledgements

The efficient and open-source SMT solver OpenSMT has been developed by Roberto Bruttomesso, PB/CT would not have been possible without it.

PB/CT also uses this C++ parser provided by Olivier Roussel and Vasco Manquinho.

A word of warning

OpenSMT-CT is a modified version of OpenSMT which may or may not work in the same way as OpenSMT. If you're not using the theory of costs, using the original OpenSMT is recommended.