Software translating of combinatorial problems to propositional logic

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.