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!