This report presents the development and implementation of an algorithm for computing the stable model semantics of logic programs. The stable model semantics is a form of nonmonotonic reasoning that allows for the representation of complex logical relationships. The algorithm, named smodels, is designed to efficiently compute stable models, which are the solutions to logic programming problems under this semantics. The report extends the stable model semantics to include three new types of rules: choice rules for encoding subsets of a set, cardinality rules for enforcing cardinality limits on subsets, and weight rules for expressing inequalities over weighted linear sums. These rules allow for more expressive logic programs that can be more compact and easier to solve. The algorithm is implemented with a focus on efficiency, including the use of lookahead techniques to avoid unnecessary testing of literals and heuristics to minimize the search space. The algorithm is compared with three satisfiability solvers, demonstrating that the heuristic can be improved by breaking ties, although the method for breaking ties remains an open question. The report also shows that the more expressive rules of the stable model semantics make it preferable to propositional logic when a problem has a more compact logic program representation. The implementation of the algorithm is detailed, including the use of efficient techniques such as backtracking, pruning, and the use of strongly connected components and source pointers to optimize the search process. The algorithm is tested on various problems, including 3-SAT, pigeon-hole problems, Hamiltonian cycles, error-correcting codes, and bin-packing, demonstrating its effectiveness and efficiency. The report concludes that the stable model semantics provides a powerful and expressive framework for logic programming, with the smodels algorithm offering an efficient and effective method for computing stable models. The algorithm's ability to handle complex rules and its efficient implementation make it a valuable tool for solving a wide range of logic programming problems.This report presents the development and implementation of an algorithm for computing the stable model semantics of logic programs. The stable model semantics is a form of nonmonotonic reasoning that allows for the representation of complex logical relationships. The algorithm, named smodels, is designed to efficiently compute stable models, which are the solutions to logic programming problems under this semantics. The report extends the stable model semantics to include three new types of rules: choice rules for encoding subsets of a set, cardinality rules for enforcing cardinality limits on subsets, and weight rules for expressing inequalities over weighted linear sums. These rules allow for more expressive logic programs that can be more compact and easier to solve. The algorithm is implemented with a focus on efficiency, including the use of lookahead techniques to avoid unnecessary testing of literals and heuristics to minimize the search space. The algorithm is compared with three satisfiability solvers, demonstrating that the heuristic can be improved by breaking ties, although the method for breaking ties remains an open question. The report also shows that the more expressive rules of the stable model semantics make it preferable to propositional logic when a problem has a more compact logic program representation. The implementation of the algorithm is detailed, including the use of efficient techniques such as backtracking, pruning, and the use of strongly connected components and source pointers to optimize the search process. The algorithm is tested on various problems, including 3-SAT, pigeon-hole problems, Hamiltonian cycles, error-correcting codes, and bin-packing, demonstrating its effectiveness and efficiency. The report concludes that the stable model semantics provides a powerful and expressive framework for logic programming, with the smodels algorithm offering an efficient and effective method for computing stable models. The algorithm's ability to handle complex rules and its efficient implementation make it a valuable tool for solving a wide range of logic programming problems.