СПЕЦПРОЦЕССОР ДЛЯ ЗАДАЧИ ВЫПОЛНИМОСТИ БУЛЕВЫХ ФОРМУЛ
SPECIAL-PURPOSE PROCESSOR FOR BOOLEAN SATISFIABILITY PROBLEM

k
m
Изобретение относится к вычислительной технике, в частности к специализированным процессорам с высокой степенью параллелизма. Спецпроцессор предназначен для решения задачи о выполнимости булевых функций, заданных в конъюнктивной нормальной форме (CNF), имеющих N=2 переменных и до М=2 дизъюнкций (CLAUSE).
Известен параллельный спецпроцессор для решения задач о выполнимости булевых формул, реализуемый на реконфигурируемой аппаратуре. Спецпроцессор решает задачу выполнимости, используя параллельные аппаратурно-реализованные обратные связи (parallel backtrace). Спецпроцессор содержит блок управления и синхронизации, а также блоки логики переменных, литералов и дизъюнкций (US 6292916 B1, 18.09.2001).
Спецпроцессор выполняет параллельно-последовательное решение задачи и обладает высокой степенью параллелизма, одновременно оперируя со всеми переменными и всеми дизъюнкциями булевой формулы загруженными в его матрицу.
Недостатками спецпроцессора является его избыточная структурная сложность, равно как и сложность алгоритма решения задачи, а также связанное с этой избыточной сложностью замедление скорости работы.
Известен высокопараллельный спецпроцессор для решения задач о выполнимости булевых формул, наиболее близкий по своей технической сущности к предлагаемому изобретению и выбранный в качестве прототипа. Данный спецпроцессор содержит интерфейсный блок, устройство управления и процессорный блок, выполненный в виде матрицы. Процессорный блок является устройством параллельной записи и считывания с многоразрядным адресным входом, входом сброса и одним выходом. Для перебора возможных значений переменных в спецпроцессоре используется счетчик (RU 2074415 С1, 27.02.1997).
В спецпроцессоре реализуется алгоритм, основанный на нахождении и объединении невыполняющих наборов булевой формулы, заданной в конъюнктивной нормальной форме. Спецпроцессор выполняет решение задачи в параллельно последовательном режиме. Логические переменные, фигурирующие в задаче, разделяются на два типа, при этом переменные второго типа рассматриваются последовательно.
Недостаток спецпроцессора, выбранного в качестве прототипа, его избыточная структурная сложность, обусловленная выделением двух типов переменных и двух типов поднаборов переменных. Упомянутое разделение переменных и поднаборов порождает сложную структуру контура управления, что замедляет решение задачи.
Технический результат изобретения - снижение сложности спецпроцессора, и повышение скорости решения задачи о выполнимости булевых функций. Технический результат достигается упрощением структуры спецпроцессора, основой которого является сумматор-аккумулятор, приоритетная цепочка и матрица, содержащая N×M однотипных ячеек (CELL). После записи информации об анализируемой булевой формуле в триггеры ячеек матрицы спецпроцессор функционирует как сумматор-аккумулятор, имеющий обратную связь выхода с входом, т.е. как конечный автомат с простейшей структурой. Время решения задачи сокращается благодаря приоритетной цепочке, позволяющей (когда это возможно) в каждом такте работы спецпроцессора отбрасывать значительное число неперспективных наборов переменных.
Технический результат достигается тем, что предлагаемый спецпроцессор содержит N-разрядный сумматор-аккумулятор, вход сброса которого является входом сброса спецпроцессора, вход синхронизации является входом синхронизации спецпроцессора, вход разрешения записи является первым управляющим входом спецпроцессора, а информационный вход подключен к выходу приоритетной цепочки; первый и второй дешифраторы, m-разрядный и k-разрядный информационные входы которых являются соответственно первым и вторым информационными входами спецпроцессора, а управляющий вход второго дешифратора является вторым управляющим входом спецпроцессора; М последовательно пронумерованных блоков дизъюнкции (CLAUSE), каждый из которых содержит первый элемент «ИЛИ» и N последовательно пронумерованных ячеек (CELL), каждая из которых содержит первый RS-триггер, D-триггер, элемент суммирования по модулю два, первый, второй и третий элементы «И», второй и третий элементы «ИЛИ»; причем в каждой ячейке выход первого элемента «И» соединен с входом разрешения D-триггера и установочным входом первого RS-триггера, выход которого соединен с первыми входами второго элемента «И» и второго элемента «ИЛИ», выход которого соединен с первым входом третьего элемента «И», выход которого, в свою очередь, соединен с первым входом третьего элемента «ИЛИ», второй вход второго элемента «И» подключен к выходу элемента суммирования по модулю два, первый вход которого подключен к выходу D-триггера; в каждом блоке дизъюнкции вторые входы третьих элементов «И» подключены к инверсному выходу первого элемента «ИЛИ», второй вход второго элемента «ИЛИ» и инверсный вход третьего элемента «И» младшей ячейки блока обнулены, а соответствующие входы второго элемента «ИЛИ» и третьего элемента «И» каждой из остальных ячеек блока подключены к выходу второго элемента «ИЛИ» предшествующей ячейки; вторые входы элементов суммирования по модулю два ячеек, имеющих в блоках дизъюнкции одинаковый номер, подключены к разряду с соответствующим номером N-разрядного информационного выхода сумматора-аккумулятора, одновременно являющегося первым выходом спецпроцессора; вторые входы третьих элементов «ИЛИ» ячеек блока дизъюнкции, имеющего младший номер обнулены, а вторые входы третьих элементов «ИЛИ» ячеек остальных блоков дизъюнкции подключены к выходам третьих элементов «ИЛИ» соответствующих по номеру ячеек предшествующего блока дизъюнкции, при этом выход третьего элемента «ИЛИ» каждой из ячеек старшего блока дизъюнкции соединен с соответствующим разрядом входа приоритетной цепочки и с одним из входов четвертого элемента «ИЛИ», инверсный вход которого подключен к первому управляющему входу спецпроцессора, а инверсный выход является вторым выходом спецпроцессора; информационные входы всех D-триггеров соединены и являются третьим информационным входом спецпроцессора; первые входы первых элементов «И» одноименных ячеек всех блоков дизъюнкции подключены к соответствующему разряду N-разрядного выхода второго дешифратора, а все вторые входы первых элементов «И» ячеек блока дизъюнкции объединены и подключены к разряду, соответственно номеру блока дизъюнкции, M-разрядного выхода первого дешифратора; выход переноса сумматора-аккумулятора подключен к установочному входу второго RS-триггера, выход которого является третьим выходом спецпроцессора; кроме того, входы сброса и синхронизации всех триггеров подключены к входу сброса и к входу синхронизации спецпроцессора.
На фиг.1 представлена схема спецпроцессора, содержащего М блоков однотипных блоков дизъюнкции (CLAUSE).
На фиг.2 приведена схема блока дизъюнкции, содержащего N однотипных ячеек (CELL).
На фиг.3 приведена схема ячейки (CELL) предлагаемого спецпроцессора.
На фиг.4 приведена временная диаграмма, иллюстрирующая функционирование спецпроцессора при обработке формулы, не имеющей выполняющего набора переменных.
На фиг.5 приведена временная диаграмма, иллюстрирующая функционирование спецпроцессора при обработке формулы, имеющей выполняющий набор переменных.
На фиг.6 представлена таблица 1, содержащая 18 дизъюнкций, из которых скомпонованы формулы в примерах, использованных при описании функционирования спецпроцессора.
На фиг.7 представлена таблица 2, содержащая 18 логических формул в конъюнктивной нормальной форме, выполняющие наборы для этих формул и число тактов, затраченных на нахождение каждого набора.
На фиг.8 представлен вариант схемы управления спецпроцессором.
Предлагаемый спецпроцессор для задачи выполнимости булевых формул содержит N-разрядный сумматор-аккумулятор 1, вход сброса которого является входом 2 сброса спецпроцессора, вход синхронизации является входом 3 синхронизации спецпроцессора, вход разрешения записи является первым управляющим входом 4 спецпроцессора, а информационный вход подключен к выходу приоритетной цепочки 5; первый 6 и второй 7 дешифраторы, m-разрядный и k-разрядный информационные входы которых являются соответственно первым 8 и вторым 9 информационными входами спецпроцессора, а управляющий вход второго дешифратора 7 является вторым управляющим входом 10 спецпроцессора; М последовательно пронумерованных блоков дизъюнкции (CLAUSE), каждый из которых содержит первый элемент «ИЛИ» 11 и N последовательно пронумерованных ячеек (CELL) каждая из которых содержит первый RS-триггер 12, D-триггер 13, элемент суммирования по модулю два 14, первый 15, второй 16 и третий 17 элементы «И», второй 18 и третий 19 элементы «ИЛИ»; причем в каждой ячейке выход первого элемента «И» 15 соединен с входом разрешения D-триггера 13 и установочным входом первого RS-триггера 12, выход которого соединен с первыми входами второго элемента «И» 16 и второго элемента «ИЛИ» 18, выход которого соединен с первым входом третьего элемента «И» 17, выход которого, в свою очередь, соединен с первым входом третьего элемента «ИЛИ» 19, второй вход второго элемента «И» 16 подключен к выходу элемента суммирования по модулю два 14, первый вход которого подключен к выходу D-триггера 13; в каждом блоке дизъюнкции вторые входы третьих элементов «И» 17 подключены к инверсному выходу первого элемента «ИЛИ» 11, второй вход второго элемента «ИЛИ» 18 и инверсный вход третьего элемента «И» 17 младшей ячейки блока обнулены, а соответствующие входы второго элемента «ИЛИ» 18 и третьего элемента «И» 17 каждой из остальных ячеек блока подключены к выходу второго элемента «ИЛИ» 18 предшествующей ячейки; вторые входы элементов суммирования по модулю два 14 ячеек, имеющих в блоках дизъюнкции одинаковый номер, подключены к разряду с соответствующим номером N-разрядного информационного выхода сумматора-аккумулятора 1, одновременно являющегося первым выходом 20 спецпроцессора; вторые входы третьих элементов «ИЛИ» 19 ячеек блока дизъюнкции, имеющего младший номер, обнулены, а вторые входы третьих элементов «ИЛИ» 19 ячеек остальных блоков дизъюнкции подключены к выходам третьих элементов «ИЛИ» 19 соответствующих по номеру ячеек предшествующего блока дизъюнкции, при этом выход третьего элемента «ИЛИ» 19 каждой из ячеек старшего блока дизъюнкции соединен с соответствующим разрядом входа приоритетной цепочки 5 и с одним из входов четвертого элемента «ИЛИ» 21, инверсный вход которого подключен к первому управляющему входу 4 спецпроцессора, а инверсный выход является вторым выходом 22 спецпроцессора; информационные входы всех D-триггеров соединены и являются третьим информационным входом 23 спецпроцессора; первые входы первых элементов «И» 15 одноименных ячеек всех блоков дизъюнкции подключены к соответствующему разряду N-разрядного выхода второго дешифратора 7, а все вторые входы первых элементов «И» 15 ячеек блока дизъюнкции объединены и подключены к разряду, соответственно номеру блока дизъюнкции, M-разрядного выхода первого дешифратора 6; выход переноса сумматора-аккумулятора 1 подключен к установочному входу второго RS-триггера 24, выход которого является третьим выходом 25 спецпроцессора; кроме того, входы сброса и синхронизации всех триггеров подключены к входу 2 сброса и к входу 3 синхронизации спецпроцессора.
Работу спецпроцессора рассмотрим совместно с одним из возможных вариантов реализации устройства управления, представленным на фиг.8.
В процессе работы предлагаемого спецпроцессора используется естественная кодировка булевой формулы, представленной в конъюнктивной нормальной форме. Запись формулы начинается с маркера, в качестве которого использован восклицательный знака «!». За маркером начала следуют записанные через запятую «,» литералы - номера переменных без знака или со знаком «-», входящих в одну дизъюнкцию. Использование знака «-» означает, что в дизъюнкции используется инверсное значение переменной. Запись переменных, принадлежащих дизъюнкции, заканчивается маркером точка с запятой «;» в случае, если дизъюнкция не является последней, и маркером точка «.», если дизъюнкция является последней в записи функции.
Например, функция
0
2
1
3
4
5
7
0
1
2
6
4
5
3
7
F=(¬Х+¬Х+¬Х+Х+Х+¬Х+Х)(Х+Х+Х)(Х+¬Х+Х+¬Х+¬Х),
записывается в эквивалентном виде
Y!-0,-2,-1,3,4,-5,7;0,1,2;6,-4,5,-3,-7.
Для рассматриваемой булевой функции N=8 (k=3), М=3.
Спецпроцессор и его устройство управления оперируют со следующей последовательностью k+3-разрядных информационных слов в буферном ОЗУ:
/Y!/-0,/-2,/-1,/3,/4,/-5,/7;/0,/1,/2;/6,/-4,/5,/-3/-7./
Информационные слова, имеющие последовательные адреса, разделены маркером «/».
Используемые при записи формулы знаки препинания кодируются следующим образом «!»=>00, «,»=>01, «;»=>10, «.»=>11. Для кодирования знаков препинания используются разряды k+3, k+2. Разряд k+1 используется для кодирования инверсии переменной. При работе представленного на фиг.8 варианта устройства управления k-разрядный код Y не используется.
После снятия сигнала сброса устройство управления на основании информации, записанной в ОЗУ, осуществляет установку D-триггеров и первых RS-триггеров ячеек блоков дизъюнкции. При этом текущий номер блока дизъюнкции определяется кодом, поступающим с выхода счетчика дизъюнкций на первый информационный вход 8 спецпроцессора, а номер ячейки в блоке дизъюнкции определяется младшими k-разрядами слова ОЗУ, поступающими на второй информационный вход 9 спецпроцессора. Единичное значение на выходе первого RS-триггера свидетельствует о том, что соответствующая переменная включена в составе соответствующей дизъюнкции.
На третий информационный вход 23 спецпроцессора подается несущий информацию об инверсии переменной разряд k+1 слова ОЗУ. Этот разряд поступает на информационные входы всех D-триггеров и записывается в триггер выбранной ячейки. Единичное значение на выходе D-триггера свидетельствует о том, что соответствующая переменная в составе соответствующей дизъюнкции инвертирована.
Код «.» устанавливает RS-триггер устройства управления, при этом процесс записи информации в триггеры ячеек блоков дизъюнкции прекращается, одновременно разрешается работа сумматора-аккумулятора 1.
Состояние инверсного выхода элемента «ИЛИ» 11 каждого блока дизъюнкции определяет, является ли соответствующая дизъюнкции действующей. Действующей называется дизъюнкция, все литералы которой равны нулю при наборе значений булевых переменных заданным состоянием выхода сумматора-аккумулятора 1. Вторые элементы «ИЛИ» 18 и третьи элементы «И» 17 в каждом из блоков дизъюнкции образуют приоритетную цепочку так, что в блоке действующей дизъюнкции единичное значение принимает выход третьего элемента «И» 17 ячейки, соответствующей младшей переменной.
j
j
Выходы третьих элементов «И» 17 ячеек блоков дизъюнкции собраны поразрядно по «ИЛИ», реализованному на двухвходовых третьих элементах «ИЛИ» 19, при этом выход элемента «ИЛИ» 19 старшего блока дизъюнкции соединен с соответствующим разрядом входа приоритетной цепочки 5. Приоритетная цепочка 5 выбирает действующую дизъюнкцию, младшая переменная которой является старшей по сравнению с младшими переменными других действующих дизъюнкций. Приоритетный выбор дизъюнкции направлен на исключение максимального числа неперспективных наборов переменных. Если в разряде j выхода приоритетной цепочки 5 присутствует единица, код в сумматоре-аккумуляторе 1 увеличивается на 2, что соответствует отбраковке 2 наборов переменных в одном такте работы спецпроцессора.
После записи информации об анализируемой булевой формуле в триггеры ячеек матрицы спецпроцессор функционирует как сумматор-аккумулятор, имеющий обратную связь выхода (SUAC) с входом, т.е. как конечный автомат с простейшей структурой.
Ситуация, когда все разряды выхода (BACK) приоритетной цепочки 5 обнулены, соответствует нахождению выполняющего набора булевой формулы, поскольку набор на выходе сумматора-аккумулятора 1 не порождает ни одной действующей дизъюнкции. В таком случае на инверсном выходе четвертого элемента «ИЛИ» 21, являющегося вторым выходом 22 (SAT) спецпроцессора, устанавливается единичное значение.
Загруженная в спецпроцессор булева формула невыполнима, если единица появляется на выходе переноса (N_SAT) сумматора-аккумулятора 1. Единица, появившаяся на выходе переноса сумматора-аккумулятора 1, запоминается во втором RS-триггере 24, выход которого является третьим выходом 25 спецпроцессора.
Графа (СТ) на временных диаграммах, представленных на фиг.4 и фиг.5, представляет в шестнадцатиричной системе число тактов (CLK) работы спецпроцессора в режиме конечного автомата (SJOB=1).
Работа спецпроцессора проиллюстрирована на примере булевых формул, составленных из конъюнкций, представленных в таблице 1 на фиг.6.
N
Временная диаграмма на фиг.4 иллюстрирует работу спецпроцессора на примере невыполнимой формулы F, являющейся конъюнкцией всех восемнадцати дизъюнкций, представленных в таблице 1 (фиг.6).
N
0
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
F=C·C·C·C·C·C·C·C·C·C·C·C·C·C·C·C·C·C.
N
7
6
5
4
3
2
1
0
В таблице 2 (фиг.7) приведены восемнадцать выполнимых формул, каждая их которых получена удалением из невыполнимой формулы F одной из дизъюнкций. Для каждой из таких формул приведен выполняющий набор, начиная со старших переменных (Х, Х, X, Х, Х, Х, Х, Х), и число тактов работы спецпроцессора.
1
Временная диаграмма, иллюстрирующая обработку формулы F, представлена на фиг.5.