The satisfiability problem in regular CNF-formulas

Manyà Serres, Felip; Béjar Torres, Ramón; Escalada Imaz, G.

doi:https://doi.org/10.1007/s005000050042

View/Open

003864.pdf (319.0Kb)
Sol·licita una còpia

Issue date

1998

Author

Manyà Serres, Felip

Béjar Torres, Ramón

Escalada Imaz, G.

Suggested 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.

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.

URI

http://hdl.handle.net/10459.1/57193

DOI

https://doi.org/10.1007/s005000050042

Is part of

Soft Computing, 1998, vol. 2, p. 116-123