Технология трансляции комбинаторных проблем в булевы уравнения

Рассматриваются проблемы сведения некоторых комбинаторных задач к задачам поиска решений булевых уравнений. Приведены теоретические результаты, являющиеся базой технологии пропозиционального кодирования алгоритмов, вычисляющих дискретные функции. Описан программный комплекс Transalg – многофункциональный транслятор комбинаторных проблем в булевы уравнения. Приведены примеры использования комплекса Transalg для сведения задач криптоанализа к SAT-задачам. Рассмотрены основы техники трансляции оптимизационных задач 0-1–ЦЛП в SAT-задачи.