Верифікація програмного забезпечення на основі рішення SAT-задачі

Abstract

Для верифікації програмних продуктів використовується програмний комплекс Transalg призначений для зведення до булевого рівняння (і в тому числі до SAT-завдання) задач зведення полиномінальних обчислювальних дискретних функцій. З цією метою алгоритм обчислення функції записується на спеціальній Сподібній мові (ТА-мова), після чого відбувається трансляція отриманої ТА-програми в систему булевих рівнянь. На заключному етапі трансляції система приводиться до однієї з можливих нормальних форм («КНФ = 1», «ДНФ = 0», поліноміальні рівняння над полем GF ). Тому є актуальним розробка ефективних алгоритмів рішення SAT-задачі. Усі відомі алгоритми мають експоненціальну складність. У роботі розглядається можливість створення алгоритму субекспоненціальної складності для вирішення SATзадачі.