The dissertation by Patrik Simons, titled "Extending and Implementing the Stable Model Semantics," focuses on developing an algorithm to compute stable models of logic programs. The author extends the stable model semantics to include three new types of rules: choice rules, cardinality rules, and weight rules. These extensions allow for more expressive logic programs, making them suitable for solving problems with compact representations. The dissertation outlines the stable model semantics and introduces the new rule types. It then presents the *smodels* procedure, which is an implementation of the extended semantics. The procedure is designed to compute stable models of logic programs and can be extended to find specific stable models, such as the lexicographically smallest one. Key contributions of the work include: 1. **New Rule Types**: Choice rules, cardinality rules, and weight rules are introduced to enhance the expressiveness of logic programs. 2. **Algorithm for Computing Stable Models**: The *smodels* procedure is described, which uses a backtracking search algorithm to find stable models. 3. **Heuristic for Minimizing Search Space**: A heuristic is derived to minimize the search space, improving the efficiency of the algorithm. The dissertation also discusses the implementation details of the *smodels* algorithm, including the use of lookahead to avoid testing every literal for failure and the implementation of source pointers and strongly connected components to reduce the search space. Additionally, it compares the *smodels* algorithm with other satisfiability solvers and propositional satisfiability checkers through experiments on various problems. Overall, the work demonstrates the effectiveness of the extended stable model semantics and the efficient implementation techniques, showing that the more expressive rules of the stable model semantics make it a superior method over propositional logic for problems with compact logic program representations.The dissertation by Patrik Simons, titled "Extending and Implementing the Stable Model Semantics," focuses on developing an algorithm to compute stable models of logic programs. The author extends the stable model semantics to include three new types of rules: choice rules, cardinality rules, and weight rules. These extensions allow for more expressive logic programs, making them suitable for solving problems with compact representations. The dissertation outlines the stable model semantics and introduces the new rule types. It then presents the *smodels* procedure, which is an implementation of the extended semantics. The procedure is designed to compute stable models of logic programs and can be extended to find specific stable models, such as the lexicographically smallest one. Key contributions of the work include: 1. **New Rule Types**: Choice rules, cardinality rules, and weight rules are introduced to enhance the expressiveness of logic programs. 2. **Algorithm for Computing Stable Models**: The *smodels* procedure is described, which uses a backtracking search algorithm to find stable models. 3. **Heuristic for Minimizing Search Space**: A heuristic is derived to minimize the search space, improving the efficiency of the algorithm. The dissertation also discusses the implementation details of the *smodels* algorithm, including the use of lookahead to avoid testing every literal for failure and the implementation of source pointers and strongly connected components to reduce the search space. Additionally, it compares the *smodels* algorithm with other satisfiability solvers and propositional satisfiability checkers through experiments on various problems. Overall, the work demonstrates the effectiveness of the extended stable model semantics and the efficient implementation techniques, showing that the more expressive rules of the stable model semantics make it a superior method over propositional logic for problems with compact logic program representations.