Geodesic
Software translating of combinatorial problems to propositional logic
Prikladnaâ diskretnaâ matematika, no. 12 (2010), pp. 81-82 Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice de l'article

A technology for translating different combinatorial problems to the tasks of finding solutions of logical (Boolean) equations is presented. Theoretical possibility of translations of that sort was shown by S. Cook in 1971. The report is expected to describe in detail Transalg – the new translator of algorithms to the propositional logic. Unlike previous developments this translator allows obtaining propositional encodings for algorithms computing arbitrary everywhere defined Register Machine-computable discrete functions. Actually a program computing this function should be written in a special high level (C-like) language. Translator was used for obtaining propositional encodings of some encryption algorithms, algorithms describing functioning the gene networks of a certain class and for translating the problems from 0-1 ILP to SAT. 
@article{PDM_2010_12_a39,
     author = {I. V. Otpuschennikov and A. A. Semenov},
     title = {Software translating of combinatorial problems to propositional logic},
     journal = {Prikladna\^a diskretna\^a matematika},
     pages = {81--82},
     year = {2010},
     number = {12},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/PDM_2010_12_a39/}
}
TY  - JOUR
AU  - I. V. Otpuschennikov
AU  - A. A. Semenov
TI  - Software translating of combinatorial problems to propositional logic
JO  - Prikladnaâ diskretnaâ matematika
PY  - 2010
SP  - 81
EP  - 82
IS  - 12
UR  - http://geodesic.mathdoc.fr/item/PDM_2010_12_a39/
LA  - ru
ID  - PDM_2010_12_a39
ER  - 
%0 Journal Article
%A I. V. Otpuschennikov
%A A. A. Semenov
%T Software translating of combinatorial problems to propositional logic
%J Prikladnaâ diskretnaâ matematika
%D 2010
%P 81-82
%N 12
%U http://geodesic.mathdoc.fr/item/PDM_2010_12_a39/
%G ru
%F PDM_2010_12_a39
I. V. Otpuschennikov; A. A. Semenov. Software translating of combinatorial problems to propositional logic. Prikladnaâ diskretnaâ matematika, no. 12 (2010), pp. 81-82. http://geodesic.mathdoc.fr/item/PDM_2010_12_a39/

[1] Massacci F., Marraro L., “Logical Cryptanalysis as a SAT Problem”, J. Automated Reasoning, 24:1–2 (2000), 165–203 | DOI | MR | Zbl

[2] Buranov E. V., “Programmnaya translyatsiya protsedur logicheskogo kriptoanaliza simmetrichnykh shifrov”, Vestnik Tomskogo gosuniversiteta, 2004, Prilozhenie No 9(1), 60–65

[3] http://www.veripool.org/

[4] Berkeley Logic Synthesis and Verification Group, ABC: A System for Sequential Synthesis and Verification http://www.eecs.berkeley.edu/~alanmi/abc/

[5] Semenov A. A, “Translyatsiya algoritmov vychisleniya diskretnykh funktsii v vyrazheniya propozitsionalnoi logiki”, Prikladnye algoritmy v diskretnom analize, Ser. Diskretnyi analiz i informatika, 2, Izd-vo IGU, Irkutsk, 2008, 70–98

[6] Een N., Sorensson N., “Translating Pseudo-Boolean Constraints into SAT”, J. Satisfiabil., Boolean Model. Computat., 2006, no. 2, 1–25