Overview

HTTPS SSH

PyLMT

This package provides a Python implementation of Learning Modulo Theories.

Requirements

This package requires numpy and OptiMathSAT, you can find them here:

You will also need a slightly modified version of pystruct:

Make sure that the optimathsat binary is visible from the $PATH environment variable.

Usage

See the experiments directory for some usage examples.

Common Issues

  • 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.

Documentation

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 docs/build/index.html.

References

  • 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.

Funding

The project is supported by the CARITRO Foundation through grant 2014.0372.