End-user OptiLog API

The functionality of OptiLog is divided in seven main modules. The user can model problems, load and manipulate Boolean formulas, encode Pseudo-Boolean and Cardinality constraints, call different SAT solvers, automatically configure functions, run experiments, and encapsulate external applications in black-boxes to be used in python.

Contents:

• Modelling Module
  • Basic Problem Modelling
  • Operators and parsing options
  • Equivalence of Python operators, Expression classes, and textual description
  • Solving a Problem with a SAT solver
  • Encoding Pseudo Boolean Expressions
• Formulas Module
  • CNF Formula
  • WCNF Formula
  • QCNF Formula
  • VarManager
  • Methods sumary
  • Formula Loading utilities
  • Formula visualization
• Encoders Module
  • PB Encoder
• Solvers Module
  • SAT Solver
• Tuning Module
  • Configurable parameters
  • Configurable functions
  • Configurable BlackBox
  • Configurable utilities
  • Configuration scenario
  • Parsing Output
  • Usage example: Automatic Configuration of the Linear MaxSAT algorithm
• Running Module
  • Introduction to the Running Module
  • Generating execution scenario
  • Running the scenario
  • Examples for submit_file
  • Parsing an execution scenario
• BlackBox Module
  • Execution Constraints
  • System Black Box
  • Satex Black Box