An analysis of lemmas extracted from model generation proofs for Sudoku (number place) puzzle - toward lemma generalization

摘要

We can prune search spaces of "Sudoku Puzzle" with lemmas which are extracted from model generation proofs. These lemmas are represented as ground expressions and applicable to very special situations. This paper analyses lemmas so as to generalize them. The analysis gives a lemma generalization method.