The satisfiability problem in regular CNF-formulas |
| |
Authors: | F. Manyà R. Béjar G. Escalada-Imaz |
| |
Affiliation: | Department d’Informàtica, Universitat de Lleida (UdL), Pla?a Victor Siurana, 1, 25003 Lleida, Spain e-mail:{felip,ramon}@eup.udl.es, ES Artificial Intelligence Research Institute, IIIA-CSIC, Campus UAB, 08193 Bellaterra, Spain e-mail:gonzalo@iiia.csic.es, ES
|
| |
Abstract: | In this paper we deal with the propositional satisfiability (SAT) problem for a kind of multiple-valued clausal forms known as regular CNF-formulas and extend some known results from classical logic to this kind of formulas. We present a Davis–Putnam-style satisfiability checking procedure for regular CNF-formulas equipped with suitable data structures and prove its completeness. Then, we describe a series of experiments for regular random 3-SAT instances. We observe that, for the regular 3-SAT problem with this procedure, there exists a threshold of the ratio of clauses to variables such that (i) the most computationally difficult instances tend to be found near the threshold, (ii) there is a sharp transition from satisfiable to unsatisfiable instances at the threshold and (iii) the value of the threshold increases as the number of truth values considered increases. Instances in the hard part provide benchmarks for the evaluation of regular satisfiability solvers. |
| |
Keywords: | Multiple-valued regular CNF-formulas satisfiability problem threshold benchmarks. |
本文献已被 SpringerLink 等数据库收录! |
|