How formal methods save Christmas

In chapter Processing Wish Lists SAT solver helps to process propositional logic formulas. The wish list in DIMACS format is available here. It can be processed using, e.g., MiniSat. The example was executed using MiniSat v1.14 for Windows.

In chapter Organizing Secret Santa a puzzle of assigning employees to be Secret Santas is modeled and solved using Alloy. The Alloy code is available here as well as the Alloy theme used for the visualization. The example was executed using Alloy 4.2RC.

In chapter Guiding the Sleds a three way crossing is modeled using SMV. The example is based on traffic lights example from the tutorial Getting started with SMV by McMillan. The initial and the fixed version are available here and here. The example was executed using NuSMV 2.5.4.

In chapter Setting up Christmas Trees FORMULA computes ways to set up christmas trees on a special market place. The example is based on the N-Queens example from the FORMULA project site. The modified version for the Christmas story is available here. The example is also available and can directly be executed in Microsoft's RiSE4fun FORMULA.