Improving First-order Model Searching by Propositional Reasoning and Lemma Learning

The finite model generation problem in the first-order logic is a generalization of the propositional satisfiability (SAT) problem. An essential algorithm for solving the problem is backtracking search. In this paper, we show how to improve such a search procedure by lemma learning. For efficiency reasons, we represent the lemmas by propositional formulas and use a SAT solver to perform the necessary reasoning. We have extended the first-order model generator SEM, combining it with the SAT solver SATO. Experimental results show that the search time may be reduced significantly on many problems.

• Type: Conference
• Year: 2004
• Where: SAT
• Authors: Zhuo Huang, Hantao Zhang, Jian Zhang
• Keywords: Model Generation Problem, SAT 2004, Sat Solver, Sat Solver Sato