This repository contains a Python framework for reasoning with uncertainty. This is joint work with Erik Quaeghebeur. N.B. This is ongoing work, so not everything is finished yet.
In the paper The CONEstrip algorithm (SMPS 2012), an algorithm is defined that determines whether a finitely generated general convex cone contains the origin.
Uncertainty models such as sets of desirable gambles and (conditional) lower previsions can be represented as convex cones. Checking the consistency of and drawing inferences from such models requires solving feasibility and optimization problems. We consider finitely generated such models. For closed cones, we can use linear programming; for conditional lower prevision-based cones, there is an efficient algorithm using an iteration of linear programs. We present an efficient algorithm for general cones that also uses an iteration of linear programs.
In the paper A propositional CONEstrip algorithm (IPMU 2014) a generalization of the CONEstrip algorithm is presented.
We present a variant of the CONEstrip algorithm for checking whether the origin lies in a finitely generated convex cone that can be open, closed, or neither. This variant is designed to deal efficiently with problems where the rays defining the cone are specified as linear combinations of propositional sentences. The variant differs from the original algorithm in that we apply row generation techniques. The generator problem is WPMaxSAT, an optimization variant of SAT; both can be solved with specialized solvers or integer linear programming techniques. We additionally show how optimization problems over the cone can be solved by using our propositional CONEstrip algorithm as a preprocessor. The algorithm is designed to support consistency and inference computations within the theory of sets of desirable gambles. We also make a link to similar computations in probabilistic logic, conditional probability assessments, and imprecise probability theory.
In the CONEstrip algorithm several linear programming problems need to be solved. This has been implemented using Z3. Note that it is also possible to solve them with a library like cddlib.
The propositional CONEstrip algorithm is defined in terms of WPMaxSAT problems. We note that WPMaxSAT problems can be conveniently expressed using the propositional logic of Z3. Hence, also this algorithm has been implemented using Z3.
A detailed specification of the implementation can be found in https://wiegerw.github.io/CONEstrip/pdf/main.pdf. Note that this is not a tutorial, but rather a precise description of the algorithms that were implemented.
The code is available as the PyPI package CONEstrip. It can be installed using
pip install CONEstrip
The code is available under the Boost Software License 1.0. A local copy is included in the repository.
For testing the Toy Parser Generator package is used. This package is available under the GNU Lesser General Public License v2.1 license. A local copy is included in the repository.