返回Google圖書搜尋

A Two Phase Algorithm for Solving a Class of Hard Satisfiability Problems

Joost P. WarnersJohannes Pieter WarnersHans van Maaren

出版	CWI, 1998
URL	http://books.google.com.hk/books?id=fmpvHAAACAAJ&hl=&source=gbs_api

註釋Abstract: "The DIMACS suite of satisfiability (SAT) benchmarks contains a set of instances that are very hard for existing algorithms. These instances arise from learning the parity function on 32 bits. In this paper we develop a two phase algorithm that is capable of solving these instances. In the first phase, a polynomially solvable subproblem is identified and solved. Using the solution to this problem, we can considerably restrict the size of the search-space in the second phase of the algorithm, which is an extension of the well-known Davis-Putnam-Loveland algorithm for SAT problems. We conclude with reporting on our computational results on the parity instances."