Software translating of combinatorial problems to propositional logic.pdf Интенсивный рост производительности современных вычислительных архитектурсделал возможным решение комбинаторных задач таких размерностей, которые казалисьнепреодолимыми еще 15-20 лет назад. В связи с этим возникли новые направленияв компьютерной алгебре и вычислительных отраслях дискретной математикии математической логики. Одной из наиболее актуальных в этом смысле областейявляется решение логических (булевых) уравнений. В последние 10 лет наблюдаетсясущественный прогресс в разработке алгоритмов, эффективных на практически важныхклассах логических уравнений.К логическим уравнениям эффективно сводятся многочисленные комбинаторныезадачи. Однако при практическом осуществления соответствующих сведений приходитсясталкиваться с различными препятствиями (разнородность структур данных;отсутствие идеологии, применимой к широкому классу проблем, и др.). Сказанноеозначает актуальность проблемы разработки многофункционального транслятора,осуществляющего сведение различных комбинаторных задач к задачам поиска решенийлогических уравнений. Следует отметить, что во многих имеющихся разработкахданная проблема так или иначе решалась (см. [1-4]). Однако во всех этих случаях осуществляласьтрансляция некоторого «узкого» класса проблем, ограниченного конкретнойпредметной областью. Комплекс Verilog [3] используется при описании логическихсхем, и все его базовые конструкции ориентированы на специалистов в схемотехнике.Комплекс ABC [4] предназначен для решения задач синтеза и верификации логическихсхем; схемы могут быть описаны в различных форматах, однако предполагается,что пользователь эти описания каким-либо образом получил (например, используяVerilog).В работе излагаются общие принципы построения нового многофункциональноготранслятора Transalg. Данный программный комплекс позволяет осуществлять пропозициональноекодирование алгоритмов, не предполагая узкоспециальных знаний упользователя. Язык Transalg - это фактически самостоятельный язык с С-подобнымсинтаксисом. Семантика языка определяет правила построения логических уравненийпо соответствующему описанию алгоритма. Ниже приведены основные этапы трансляцииалгоритмов в комплексе Transalg.1) Анализ текста программы и построение дерева синтаксического разбора.2) Обход построенного дерева, выполнение семантических действий: «пропозициональнаясвертка» условных переходов (см. [5]) за счет преобразований Цейтина,построение систем логических уравнений.3) Приведение систем логических уравнений к нормальным формам; преобразованиев формат И-НЕ графов.Пропозициональные кодировки многих алгоритмов, реализованные в транслятореTransalg, по объему существенно меньше известных аналогов (например, пропозициональнаякодировка алгоритма DES компактнее кодировки, представленной в [1], болеечем в два раза).Дополнительной возможностью комплекса Transalg является сведение к SAT (илик системе логических уравнений в любой нормальной форме) задач 0-1-целочисленноголинейного программирования (0-1-ЦЛП). Получаемые кодировки по компактноститакже превосходят известные аналоги [6].

Скачать электронную версию публикации