| Abstract
|
In this paper, we introduce the notion of … In this paper, we introduce the notion of redundant clauses tocharacterize the structure of SAT instances. We identify severalinteresting features of redundant clauses that provide compellingevidence of the correlation between the percentage of redundantclauses and the hardness of instances. We propose a definition ofweighted clause-to-variable ratio (WCV), which substantiallyimproves the classic clause-to-variable (m/n) ratio in predictingsearch cost and explaining phase phenomenon. arch cost and explaining phase phenomenon.
|
| Address
|
Barcelona, Spain. +
|
| Author
|
Honglei Zeng +,
Sheila A. McIlraith +
|
| Bibtype
|
inproceedings +
|
| Booktitle
|
(extended abstract), CP-2005 (the Eleventh International Conference on Principles and Practice of Constraint Programming) +
|
| Key
|
KSL-05-10 +
|
| Modification dateThis property is a special property in this wiki.
|
1 May 2009 13:35:54 +
|
| Month
|
October +
|
| Tag
|
Computer science +
|
| Title
|
The Role of Redundant Clauses in Solving Satisfiability Problems +
|
| Tr id
|
KSL-05-10 +
|
| Year
|
2005 +
|
| Categories |
Proceeding Paper,
Publication,
KSL Technical Report
|
