Reducing Symmetries to Generate Easier SAT Instances |
| |
Authors: | Jian Zhang Zhuo Huang |
| |
Affiliation: | Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100080, China |
| |
Abstract: | Finding countermodels is an effective way of disproving false conjectures. In first-order predicate logic, model finding is an undecidable problem. But if a finite model exists, it can be found by exhaustive search. The finite model generation problem in the first-order logic can also be translated to the satisfiability problem in the propositional logic. But a direct translation may not be very efficient. This paper discusses how to take the symmetries into account so as to make the resulting problem easier. A static method for adding constraints is presented, which can be thought of as an approximation of the least number heuristic (LNH). Also described is a dynamic method, which asks a model searcher like SEM to generate a set of partial models, and then gives each partial model to a propositional prover. The two methods are analyzed, and compared with each other. |
| |
Keywords: | Finite model searching SAT symmetries the least number heuristic |
本文献已被 ScienceDirect 等数据库收录! |
|