|
Title:
|
The satisfiability problem in regular CNF-formulas
|
|
Author:
|
Manyà Serres, Felip; Béjar Torres, Ramón; Escalada Imaz, G.
|
|
Notes:
|
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.
This research is partially supported by ‘‘La Paeria’’ and the projects TIC96-1038-C04-03 and TIC96-0721-C02-02 funded by the CICYT. The work of the second author is supported by a doctoral scholarship of the CIRIT (Generalitat de Catalunya). |
|
Subject(s):
|
-Multiple-valued regular CNF-formulas
-Satisfiability problem
-Threshold |
|
Rights:
|
(c) Springer Verlag, 1998
info:eu-repo/semantics/restrictedAccess |
|
Document type:
|
article
publishedVersion |
|
Published by:
|
Springer Verlag
|
|
Share:
|
|
