Study Of First-order Logic Model Search Problem

Huang Zhuo (Computer Software & Theory) Directed by Zhang JianThe algorithms and tools to solve first-order logic model searching (FOLMS) problem with finite domain size are studied in this thesis. The satisfiability(SAT) problem in the prepositional logic and FOLMS are classic problems of computer science, which are important in theory and have wide applications in a lot of real-world problems. SAT has been throughly researched in recent years, and many algorithms and tools have been developed. In comparison with SAT, the algorithms and tools of FOLMS seem inefficient, although some progress has been made in this field. This thesis focuses on how to utilize the results of SAT research in FOLMS.A new algorithm to reduce the FOLMS to SAT is presented. Its can utilize the efficient SAT solvers more conveniently and the efficiency of conversion is improved. How to reduce the search space by adding constraints for eliminating symmetries is also discussed. The experiments show the effectiveness of the new algorithm and the constraints added. An automatic tool based on this algorithm is also described.A new FOLMS algorithm improved by lemma learning is presented. Lemma learning is an important technique of SAT research. For efficient reasons, the lemmas are represented in propositional formulas and a SAT solver is used to perform the necessary reasoning. Based on this algorithm, a new first-order model generator called SEMLL is developed, as the extension of the first-order model generator SEM.