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!