reducing symmetries to generate easier sat instances

	reducing symmetries to generate easier sat instances
	Zhang Jian; Zhuo Huang
	2005
发表期刊	Electronic Notes in Theoretical Computer Science
卷号	125 期号:3 页码:149-164
摘要	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.
收录类别	ei
关键词	Finite Model Searching Sat Symmetries The Least Number Heuristic
部门归属	计算机科学国家重点实验室
语种	英语
内容类型	期刊论文
URI标识	http://ir.iscas.ac.cn/handle/311060/3130
专题	基础软件与系统重点实验室
推荐引用方式 GB/T 7714	Zhang Jian,Zhuo Huang. reducing symmetries to generate easier sat instances[J]. Electronic Notes in Theoretical Computer Science,2005,125(3):149-164.
APA	Zhang Jian,&Zhuo Huang.(2005).reducing symmetries to generate easier sat instances.Electronic Notes in Theoretical Computer Science,125(3),149-164.
MLA	Zhang Jian,et al."reducing symmetries to generate easier sat instances".Electronic Notes in Theoretical Computer Science 125.3(2005):149-164.

条目包含的文件
文件名称/大小	文献类型	版本类型	开放类型	使用许可
200512503149.pdf（253KB）			开放获取	--	请求全文