Transformation of CNF via resolution
Prikladnaâ diskretnaâ matematika, no. 10 (2009), pp. 91-93
Voir la notice de l'article provenant de la source Math-Net.Ru
This paper describes a method for equivalent transformation of CNF associated with important problems of cryptographic analysis of asymmetric ciphers. The method can reduce amount of disjuncts and resolve some variables. It can be used as a CNF preprocessor to increase the efficiency of SAT solvers.
@article{PDM_2009_10_a46,
author = {I. G. Khnykin},
title = {Transformation of {CNF} via resolution},
journal = {Prikladna\^a diskretna\^a matematika},
pages = {91--93},
publisher = {mathdoc},
number = {10},
year = {2009},
language = {ru},
url = {http://geodesic.mathdoc.fr/item/PDM_2009_10_a46/}
}
I. G. Khnykin. Transformation of CNF via resolution. Prikladnaâ diskretnaâ matematika, no. 10 (2009), pp. 91-93. http://geodesic.mathdoc.fr/item/PDM_2009_10_a46/