This package provides a Python implementation of Learning Modulo Theories.
This package requires
OptiMathSAT, you can find them here:
You will also need a slightly modified version of
Make sure that the
optimathsat binary is visible from the
experiments directory for some usage examples.
- Precision issues when converting from
floats to rationals.
If your numerical data is stored using
floats, make sure to write SMTLIB
problem that can actually tolerate the possible precision loss that occurs
when injecting the
floats into the problem file.
In other words, the underlying OMT solver may assume that the rational data is correct to infinite precision, which may produce intuitively wrong (yet formally correct!) solutions to the optimization problem, especially when using equality/inequality constraints.
You can build the in-depth documentation with
sphinx, just type:
sphinx-build -b html docs/source docs/build
The HTML documentation can be found in
- Stefano Teso, Roberto Sebastiani and Andrea Passerini, "Structured Learning Modulo Theories", 2014. link
- Roberto Sebastiani and Silvia Tomasi, "Optimization modulo theories with linear rational costs", 2015.
- Roberto Sebastiani and Patrick Trentin, "OptiMathSAT: a tool for Optimization Modulo Theories", 2015.
- Andreas Mueller and Sven Behnke, "PyStruct - Structured prediction in Python", JMLR, 2014. link.
- Ioannis Tsochantaridis et al., "Large margin methods for structured and interdependent output variables", 2005.
The project is supported by the CARITRO Foundation through grant 2014.0372.