LogicNG Tutorial

This tutorial offers a gentle introduction into the usage and algorithms of LogicNG. We accompany Beatrice, the founder of a bike shop, by facing different incidents.

Along this, we proceed from modelling a real-world problem into a configuration problem that can be solved with LogicNG to using the efficient SAT- and MaxSAT-solvers in LogicNG.

In the tutorial, you will see applications for the following content:

  • Formulate a real-world problem in LogicNG-syntax in chapter 1
  • Different operations that you can perform on formulas, such as substituting the formulas or restricting the ruleset in chapter 2
  • An example for formula functions for analyzing the rule set in chapter 3
  • Propositions, what they are and how to use them in chapter 4
  • SAT Solving, including backbones, explanations and model enumeration and counting in chapter 5
  • MaxSAT Solving in chapter 6

The code for this can be found under doc/tutorial/BicycleShopTutorial.java. Have fun!