Детальная информация

В данной работе рассматривается автоматический поиск заданных Булевых схем. Дано определение Булевой схемы, а также показано вычисление значений Булевых функций схемами. Дано определение задачи выполнимости, а также обоснована ее практическая значимость. Приведено описание алгоритма CDCL, используемого для решения задачи SAT, а также показан подход, позволяющий использовать преимущества многоядерной архитектуры при решении задачи SAT. Дано описание формата DIMACS CNF. Описан способ сведения задач о существовании комбинаторных объектов к задаче выполнимости и приведен пример такого сведения для задачи поиска решения Шидоку. Описано сведение задачи поиска заданной булевой схемы, вычисляющей некоторую булеву функцию, к задаче выполнимости. Разработана программа, выполняющая построение КНФ, которая выполнима тогда и только тогда, когда: существует решение для заданного экземпляра Шидоку, существует заданная Булева схема. Приведены примеры использования программы для поиска решения Шидоку и для поиска заданной Булевой схемы.

In the given work, an automatic search for given Boolean circuits is considered.The definition of a Boolean scheme is given, and the calculation of the values of Booleanfunctions is also shown. The definition of the satisfiability problem is given, and itspractical significance is substantiated. A description of the CDCL algorithm used to solvethe SAT problem is given, and an approach is shown that allows using the advantagesof the multicore architecture when solving the SAT problem. The description of theDIMACS CNF format is given. A method of reducing the problem of the existence ofcombinatorial objects to the problem of satisfiability is described, and an example ofsuch reduction for the problem of finding a solution to Shidoku is given. The reductionof the problem of searching for a given Boolean circuit that computes a certain Boolean function to the problem of satisfiability is described. A program has been developed thatconstructs the CNF, which is executable if and only if: there is a solution for a giveninstance of Shidoku, there is a given Boolean scheme. Examples of using the programfor finding a solution to Shidoku and for finding a given Boolean scheme are given.

• Автоматический поиск заданной булевой схемы
  • Введение
  • 1. Булевы схемы
  • 2. Задача выполнимости
  • 3. Разработанная программа
  • Заключение
  • Список использованных источников
  • Приложение. Исходный код