OptiLog
0.5.3

Contents:

  • Installation
  • End-user OptiLog API
    • 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
        • CNF
        • CNFException
        • Methods sumary
      • WCNF Formula
        • WCNF
        • WCNFException
        • Methods sumary
      • QCNF Formula
        • QCNF
        • QCNFException
        • Methods sumary
      • VarManager
        • VarManager.extend_vars()
        • VarManager.set_minimum_vars()
        • VarManager.add_var()
        • VarManager.max_var()
        • VarManager.new_var()
        • VarManager.get_lit()
      • Methods sumary
      • Formula Loading utilities
        • load_cnf()
        • load_wcnf()
        • load_qcnf()
      • Formula visualization
        • print_clauses_color()
    • Encoders Module
      • PB Encoder
        • Non-incremental encoders
        • Incremental encoders
    • Solvers Module
      • SAT Solver
        • Integrated SAT solvers
    • Tuning Module
      • Configurable parameters
        • Bool
        • Int
        • Real
        • Categorical
        • Choice
        • Dict
        • CfgCall
        • CfgCls
        • CfgObj
      • Configurable functions
        • Global configurable functions
        • Local configurable functions
        • Entrypoint functions
      • Configurable BlackBox
        • BlackBox Class as entrypoint
        • BlackBox Object as entrypoint
        • Extract BlackBox Command
        • BlackBox Class as global configurable
        • BlackBox as configurable parameter
      • Configurable utilities
        • The Choice parameter
      • Configuration scenario
        • TuningEntrypointType
        • TuningGlobalConfigurableType
        • GGAScenario
        • SMACScenario
      • Parsing Output
        • GGAParser
        • SMACParser
      • Usage example: Automatic Configuration of the Linear MaxSAT algorithm
    • Running Module
      • Introduction to the Running Module
      • Generating execution scenario
        • RunningSolverType
        • RunningScenario
        • Scenario with binary programs
        • Scenario with functions or BlackBox
      • Running the scenario
      • Examples for submit_file
        • Task Spooler
        • SGE
      • Parsing an execution scenario
        • parse_scenario()
        • ParsingInfo
    • BlackBox Module
      • Execution Constraints
        • ExecutionConstraints
        • RunSolver
        • DockerEnforcer
      • System Black Box
        • SystemBlackBox
        • BlackBoxRedirection
      • Satex Black Box
        • SatexBlackBox
  • Solver Developer
    • iSAT Interface
      • iSAT class
      • Solver states and Variables values
    • How to add a new solver to OptiLog
      • Implementing the iSAT interface
      • The Linking Functions
      • Compiling as a library
      • Loading the solver
  • Use Cases
    • The Slitherlink Problem
      • Modelling the Slitherlink Problem
      • Solving the Slitherlink Problem
        • Analyzing Inconsistent Subproblems
      • Tuning the Slitherlink Problem
      • Running the Slitherlink Problem
        • Processing Experimental Results
    • MaxSAT Competitions
      • Competition Generation
      • Competition Running
      • Competition Parsing
    • SAT Competitions
      • Competition Generation
      • Competition Running
      • Competition Parsing
  • References
  • Changelog
    • 0.5.3
    • 0.5.2
    • 0.5.1
    • 0.5.0
    • 0.4.2
    • 0.4.1
    • 0.3.6
    • 0.3.5
    • 0.3.4
    • 0.3.3
    • 0.3.2
    • 0.3.1
    • 0.3.0
  • License
OptiLog
  • Use Cases
  • The Slitherlink Problem
  • View page source

The Slitherlink Problem

In these sections, we show how to model, solve, tune and run a concrete problem using OptiLog. We focus on the Slitherlink problem, originally invented by Nikoli [Nikoli21] which was shown to be NP-Compete in [Yat03].

The Slitherlink Problem:

  • Modelling the Slitherlink Problem
  • Solving the Slitherlink Problem
  • Tuning the Slitherlink Problem
  • Running the Slitherlink Problem
Previous Next

© Copyright 2023, Logic and Optimization Group.

Built with Sphinx using a theme provided by Read the Docs.