Technology for translating combinatorial problems into Boolean equations

The article is devoted to converting combinatorial problems into the problems of solving Boolean equations. Some theoretical results are presented as the basis of technology for propositional encoding of algorithms calculating discrete functions. Software system Transalg implementing the technology is described. Examples of using the Transalg for translating cryptoanalysis algorithms to SAT-problem are presented. The technics for translating 0-1-ILP optimization algorithms into SAT are considered too.