The satisfiability problem in regular CNF-formulas
Issue date
1998Suggested citation
Manyà Serres, Felip;
Béjar Torres, Ramón;
Escalada Imaz, G.;
.
(1998)
.
The satisfiability problem in regular CNF-formulas.
Soft Computing, 1998, vol. 2, p. 116-123.
https://doi.org/10.1007/s005000050042.
Metadata
Show full item recordAbstract
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.