СПЕЦПРОЦЕССОР ДЛЯ ЗАДАЧИ ВЫПОЛНИМОСТИ БУЛЕВЫХ ФОРМУЛ

Изобретение относится к вычислительной технике, в частности к специализированным процессорам. Спецпроцессор предназначен для решения задачи о выполнимости булевых функций, заданных в конъюнктивной нормальной форме (CNF), имеющих N переменных и до М=2^K дизъюнктов (CLAUSE).

Известен спецпроцессор для решения задач о выполнимости булевых формул, который содержит интерфейсный блок, устройство управления и процессорный блок, выполненный в виде матрицы. Процессорный блок является устройством параллельной записи и считывания с многоразрядным адресным входом, входом сброса и одним выходом. Для перебора возможных значений переменных в спецпроцессоре используется счетчик (RU 2074415 С1, 27.02.1997).

В спецпроцессоре реализуется алгоритм, основанный на нахождении и объединении невыполняющих наборов булевой формулы, заданной в конъюнктивной нормальной форме. Спецпроцессор выполняет решение задачи в параллельно последовательном режиме. Логические переменные, фигурирующие в задаче, разделяются на два типа, при этом переменные второго типа рассматриваются последовательно.

Недостаток спецпроцессора в его избыточной структурной сложности, обусловленной выделением двух типов переменных и двух типов поднаборов переменных. Упомянутое разделение переменных и поднаборов порождает сложную структуру контура управления, что замедляет решение задачи.

Известен высокопараллельный спецпроцессор для решения задач о выполнимости булевых формул, наиболее близкий по своей технической сущности к предлагаемому изобретению и выбранный в качестве прототипа. Основой спецпроцессора является сумматор аккумулятор, приоритетная цепочка и матрица, содержащая N×M однотипных ячеек (CELL). После записи информации об анализируемой булевой формуле в триггеры ячеек матрицы спецпроцессор функционирует как сумматор-аккумулятор, имеющий обратную связь выхода с входом, т.е. как конечный автомат (RU 2515206 С1, 12.03.2014).

Время решения задачи сокращается благодаря приоритетной цепочке, позволяющей (когда это возможно) в каждом такте работы спецпроцессора отбрасывать значительное число неперспективных наборов переменных.

Недостаток спецпроцессора, выбранного в качестве прототипа, - его избыточная сложность, обусловленная наличием большой N×M матрицы логических ячеек и сниженная тактовая частота, связанная с задержками срабатывания элементов в длинной приоритетной цепи и цепи переноса сумматора аккумулятора.

Технический результат изобретения - снижение сложности спецпроцессора и повышение тактовой частоты при решении задачи о выполнимости булевых функций.

Технический результат достигается упрощением структуры спецпроцессора за счет того, что часть функций, выполнявшихся в прототипе логической матрицей, заменены кодированием информации, записываемой в стандартной памяти, и последующим раскодированием логикой спецпроцессора. Для кодирования формулы, имеющей N переменных и до М=2^K дизъюнктов в удобной для спецпроцессора форме, используется M(3N+2K) бит внешней для спецпроцессора памяти. Для считывания информации из памяти спецпроцессор формирует K-разрядный адрес. Организованный в спецпроцессоре перебор вариантов назначений переменных, при их конфликте с дизъюнктами формулы, позволяет отбрасывать значительное число неперспективных вариантов назначений. Для обеспечения возможности повышения тактовой частоты и для упрощения спецпроцессора изменение записанного в N-разрядном регистре текущего назначения переменных осуществляется посредством сумматора по модулю два.

Технический результат достигается тем, что предлагаемый спецпроцессор содержит N-разрядный регистр, вход сброса которого является первым входом (сброса) спецпроцессора, вход синхронизации является вторым входом (синхронизации) спецпроцессора; выход N-разрядного регистра является первым выходом спецпроцессора, а его информационный вход подключен к выходу N-разрядного сумматора по модулю два, первый вход которого подключен к выходу регистра; второй вход сумматора соединен с выходом первого мультиплексора; младшие N-1 разряды первого информационного входа первого мультиплексора подключены к выходу N-1 разрядного сдвигового регистра, при этом старший разряд упомянутого входа данных подключен к логическому нулю, второй вход данных мультиплексора является третьим N-разрядным входом спецпроцессора, к младшим N-1 разрядам которого подключен вход данных сдвигового регистра; разряды выхода первого мультиплексора соединены с первыми входами элементов И первой группы, вторые входы элементов этой группы подключены к соответствующим разрядам выхода регистра, а выходы элементов И указанной группы соединены с входами первого элемента ИЛИ, выход которого соединен с инверсным входом сброса первого RS-триггера, а также с первыми входами первого и второго элементов И, в свою очередь, второй вход второго элемента И подключен к младшему разряду выхода сдвигового регистра, а его выход является вторым выходом спецпроцессора; первый вход первой схемы сравнения является четвертым N-разрядным входом спецпроцессора, выход «равенство» упомянутой схемы сравнения соединен с первым адресным входом дешифратора; выход второго RS-триггера соединен с первым входом третьего элемента И, выход которого соединен с первым входом второго элемента ИЛИ, выход которого соединен с входом сброса третьего RS-триггера, инверсный выход которого соединен с первым входом четвертого элемента И и первым входом третьего элемента ИЛИ, второй вход которого подключен к второму выходу дешифратора, а выход соединен с входом разрешения счета первого счетчика, K-разрядный выход которого является третьим выходом спецпроцессора; второй вход первой схемы сравнения подключен к выходам элементов И второй группы, первые входы элементов И упомянутой группы подключены к разрядам выхода регистра, а вторые входы этих элементов И являются пятым N-разрядным входом спецпроцессора; первые входы элементов И третьей группы подключены к разрядам третьего входа спецпроцессора, вторые входы этих элементов подключены к разрядам пятого входа спецпроцессора, а выходы элементов И этой группы соединены с входами четвертого элемента ИЛИ, выход которого соединен с вторым адресным входом дешифратора, вторым входом третьего элемента И, инверсным входом установки второго RS-триггера и с инверсным входом пятого элемента ИЛИ, выход которого соединен с вторым входом четвертого элемента И, выход которого соединен с первым входом шестого элемента ИЛИ, выход которого соединен с входом разрешения загрузки первого K-разрядного счетчика, информационный вход упомянутого счетчика подключен к выходу второго мультиплексора, первый и второй информационные входы которого являются шестым и седьмым K-разрядными входами спецпроцессора, адресный вход второго мультиплексора вместе с вторыми входами второго, шестого и первым входом седьмого элементов ИЛИ подключен к третьему выходу дешифратора; четвертый выход дешифратора соединен с установочными входами первого и четвертого RS-триггеров и с первыми входами восьмого и девятого элементов ИЛИ, при этом вторые входы восьмого элемента ИЛИ и первого элемента И подключены к выходу первого RS-триггера; выход четвертого RS-триггера соединен с входом пятого элемента И и входом разрешения выходов второй схемы сравнения, а инверсный выход триггера соединен с информационным входом дешифратора, адресным входом первого мультиплексора и входом разрешения записи сдвигового регистра; выход пятого элемента И соединен с входом разрешения загрузки второго счетчика и входом пятого элемента ИЛИ, выход которого соединен с вторым входом четвертого элемента И; вход данных второго счетчика подключен к выходу схемы вычитания, выход второго счетчика соединен с входом уменьшаемого схемы вычитания и с первым информационным входом второй схемы сравнения, второй информационный вход упомянутой схемы сравнения, как и вход вычитаемого схемы вычитания, подключен к седьмому входу спецпроцессора; выход восьмого элемента ИЛИ соединен с входом разрешения сдвига сдвигового регистра и вторым входом седьмого элемента ИЛИ, выход которого соединен входом разрешения записи регистра; выход девятого элемента ИЛИ соединен с входом разрешения счета второго счетчика, а также с инверсными входами пятого элемента И и десятого элемента ИЛИ выход последнего соединен с входом сброса четвертого RS-триггера; выход «равенство» второй схемы сравнения соединен с входом десятого элемента ИЛИ, другой вход которого вместе с входом сброса второго RS-триггера, входом сброса второго счетчика и входом установки третьего RS-триггера подключен к выходу «меньше» второй схемы сравнения; вход сброса первого счетчика подключен к первому входу спецпроцессора; кроме того, входы синхронизации всех триггеров регистров и счетчиков подключены к входу синхронизации спецпроцессора.

На фиг. 1 представлена схема спецпроцессора.

На фиг. 2 приведена схема взаимодействия спецпроцессора с внешними блоками.

На фиг. 3 приведена кодировка невыполнимой булевой функции, на примере которой иллюстрируется работа спецпроцессора.

На фиг. 4 представлена таблица, содержащая 17 булевых формул с выполняющими эти формулы наборами.

На фиг. 5 приведена таблица, иллюстрирующая последовательность изменения набора назначений переменных.

Предлагаемый спецпроцессор для задачи выполнимости булевых формул содержит N-разрядный регистр 1, вход сброса которого является первым 2 входом (сброса) спецпроцессора, вход синхронизации является вторым 3 входом (синхронизации) спецпроцессора; выход N-разрядного регистра 1 является первым 4 выходом спецпроцессора, а его информационный вход подключен к выходу N-разрядного сумматора 5 по модулю два, первый вход которого подключен к выходу регистра 1; второй вход сумматора 5 соединен с выходом первого 6 мультиплексора; младшие N-1 разряды первого информационного входа первого 6 мультиплексора подключены к выходу N-1 разрядного сдвигового регистра 7, при этом старший разряд упомянутого входа данных подключен к логическому нулю, второй вход данных мультиплексора 6 является третьим 8 N-разрядным входом спецпроцессора, к младшим N-1 разрядам которого подключен вход данных сдвигового регистра 7; разряды выхода первого 6 мультиплексора соединены с первыми входами элементов И первой 9 группы, вторые входы элементов этой группы подключены к соответствующим разрядам выхода регистра 1, а выходы элементов И указанной группы соединены с входами первого 10 элемента ИЛИ, выход которого соединен с инверсным входом сброса первого 11 RS-триггера, а также с первыми входами первого 12 и второго 13 элементов И, в свою очередь, второй вход второго 13 элемента И подключен к младшему разряду выхода сдвигового регистра 7, а его выход является вторым 14 выходом спецпроцессора; первый вход первой схемы сравнения 15 является четвертым 16 N-разрядным входом спецпроцессора, выход «равенство» упомянутой схемы сравнения соединен с первым адресным входом дешифратора 17; выход второго 18 RS-триггера соединен с первым входом третьего 19 элемента И, выход которого соединен с первым входом второго 20 элемента ИЛИ, выход которого соединен с входом сброса третьего 21 RS-триггера, инверсный выход которого соединен с первым входом четвертого 22 элемента И и первым входом третьего 23 элемента ИЛИ, второй вход которого подключен к второму выходу дешифратора 17, а выход соединен с входом разрешения счета первого 24 счетчика, K-разрядный выход которого является третьим 25 выходом спецпроцессора; второй вход первой 15 схемы сравнения подключен к выходам элементов И второй 26 группы, первые входы элементов И упомянутой группы подключены к разрядам выхода регистра 1, а вторые входы этих элементов И являются пятым 27 N-разрядным входом спецпроцессора; первые входы элементов И третьей 28 группы подключены к разрядам третьего 8 входа спецпроцессора, вторые входы этих элементов подключены к разрядам пятого 27 входа спецпроцессора, а выходы элементов И этой группы соединены с входами четвертого 29 элемента ИЛИ, выход которого соединен с вторым адресным входом дешифратора 17, вторым входом третьего 19 элемента И, инверсным входом установки второго 18 RS-триггера и с инверсным входом пятого 30 элемента ИЛИ, выход которого соединен с вторым входом четвертого 22 элемента И, выход которого соединен с первым входом шестого 31 элемента ИЛИ, выход которого соединен с входом разрешения загрузки первого 24 K-разрядного счетчика, информационный вход упомянутого счетчика подключен к выходу второго мультиплексора 32, первый и второй информационные входы которого являются шестым 33 и седьмым 34 K-разрядными входами спецпроцессора, адресный вход второго 32 мультиплексора вместе с вторыми входами второго 20, шестого 31 и первым входом седьмого 35 элементов ИЛИ подключен к третьему выходу дешифратора 17; четвертый выход дешифратора 17 соединен с установочными входами первого 11 и четвертого 36 RS-тригтеров и с первыми входами восьмого 37 и девятого 38 элементов ИЛИ, при этом вторые входы восьмого 37 элемента ИЛИ и первого 12 элемента И подключены к выходу первого 11 RS-триггера; выход четвертого 36 RS-триггера соединен с входом пятого 39 элемента И и входом разрешения выходов второй 40 схемы сравнения, а инверсный выход триггера соединен с информационным входом дешифратора 17, адресным входом первого 6 мультиплексора и входом разрешения записи сдвигового регистра 7; выход пятого 39 элемента И соединен с входом разрешения загрузки второго счетчика 41 и входом пятого 21 элемента ИЛИ, выход которого соединен с вторым входом четвертого 22 элемента И; вход данных второго 41 счетчика подключен к выходу схемы вычитания 42, выход второго 41 счетчика соединен с входом уменьшаемого схемы вычитания 42 и с первым информационным входом второй 40 схемы сравнения, второй информационный вход упомянутой схемы сравнения, как и вход вычитаемого схемы 42 вычитания, подключен к седьмому 34 входу спецпроцессора; выход восьмого 37 элемента ИЛИ соединен с входом разрешения сдвига сдвигового регистра 7 и вторым входом седьмого 35 элемента ИЛИ, выход которого соединен входом разрешения записи регистра 1; выход девятого 38 элемента ИЛИ соединен с входом разрешения счета второго 41 счетчика, а также с инверсными входами пятого 39 элемента И и десятого 43 элемента ИЛИ, выход последнего соединен с входом сброса четвертого 36 RS-триггера; выход «равенство» второй 40 схемы сравнения соединен с входом десятого 43 элемента ИЛИ, другой вход которого вместе с входом сброса второго 18 RS-тригтера, входом сброса второго 41 счетчика и входом установки третьего 21 RS-триггера подключен к выходу «меньше» второй 40 схемы сравнения; вход сброса первого 24 счетчика подключен к первому 2 входу спецпроцессора; кроме того, входы синхронизации всех триггеров регистров и счетчиков подключены к входу 3 синхронизации спецпроцессора.

Работу спецпроцессора рассмотрим совместно с внешней памятью, дешифратором максимального адреса и счетчиком в варианте, представленном на фиг. 2.

При записи литералов булевой переменной x_i удобно использовать верхний индекс: x_i=X_i⁰, ¬x_i=X_i¹. Дизъюнкт x_i v¬x_j v x_k обозначается как C(X_i⁰,X_j¹,X_k⁰).

Работу спецпроцессора проиллюстрируем на примере формул, составленных из семнадцати дизъюнктов от восьми булевых переменных x₀, x₁, x₂, x₃, x₄, x₅, x₆, x₇: С₀(Х₀⁰,X₁⁰,X₂⁰), С₁(Х₀¹,X₁⁰,X₂⁰), С₂(Х₀⁰,X₁¹,X₂⁰), С₃(Х₀⁰,X₁¹,X₂¹), С₄(Х₀¹,X₁⁰,X₂¹), С₅(Х₀⁰,X₁¹,X₂¹), С₆(Х₀¹,X₁¹,X₂¹), С₇(Х₀⁰,X₃¹,X₄⁰), С₈(Х₂¹,X₃⁰,X₄¹), С₉(Х₁⁰,X₄¹,X₅⁰), С₁₀(Х₁⁰,X₄⁰,X₅¹), С₁₁(Х₂¹,X₅¹,X₆⁰), С₁₂(Х₀⁰,X₅⁰,X₆¹), С₁₃(Х₁⁰,X₆¹,X₇⁰), С₁₄(Х₀⁰,X₃⁰,X₇⁰), С₁₅(Х₁⁰,X₆⁰,X₇¹), С₁₆(Х₀⁰,X₃¹,X₇¹).

Формула F_N, являющаяся конъюнкцией всех семнадцати дизъюнктов

F_N=C₀⋅C₁⋅C₂⋅C₃⋅C₄⋅C₅⋅C₆⋅C₇⋅C₈⋅C₉⋅C₁₀⋅C₁₁⋅C₁₂⋅C₁₃⋅C₁₄⋅C₁₅⋅C₁₆,

невыполнима.

Для кодирования формулы, имеющей N переменных и до М=2^K дизъюнктов в удобной для спецпроцессора форме, используется M(3N+2K) бит внешней для спецпроцессора памяти. В рассматриваемом примере N=S, М=17, K=5. В таблице 1 на фиг. 3 приведена кодировка формулы, используемая спецпроцессором.

В первом столбце (справочно) указан номер дизъюнкта.

Во втором столбце единицами отмечены переменные, присутствующие в дизъюнкте в инвертированной форме. Жирным шрифтом выделены позиции переменных, представленных в дизъюнкте.

В третьем столбце единицами отмечены переменные, литералы которых входят в состав дизъюнкта.

В четвертом столбце единицей отмечена старшая по номеру переменная дизъюнкта. Дизъюнкты упорядочены так, что дизъюнкт, содержащий литерал переменной с большим номером, в свою очередь, имеет больший номер. Если старшие переменные дизъюнктов одинаковы и в первый дизъюнкт переменная входит без инверсии, а во второй с инверсией - второй дизъюнкт имеет больший номер.

Поле в пятом столбце таблицы трактуется в зависимости от того, является ли старшая переменная дизъюнкта инвертированной. Если старшая переменная входит в дизъюнкт без инверсии, поле содержит номер следующего дизъюнкта в случае отсутствия противоречия между дизъюнктом и текущим назначением переменных в регистре 1. Если старшая переменная дизъюнкта инвертирована, это поле задает номер следующего дизъюнкта при конфликте дизъюнкта с текущим назначением переменных. В первом случае это номер следующего дизъюнкта с неинвертированной старшей переменной. Во втором случае это номер первого дизъюнкта, имеющего инвертированную старшую переменную с ближайшим меньшим номером.

Поле в шестом столбце тоже зависит от инверсии старшей переменной. Если старшая переменная входит в дизъюнкт без инверсии, поле содержит номер следующего дизъюнкта при конфликте с текущим назначением переменных. Это поле содержит номер дизъюнкта, имеющего ту же старшую переменную в инверсии либо следующую по старшинству переменную без инверсии. Если старшая переменная дизъюнкта инвертирована, поле содержит отличное от нуля число, указывающее на параметр сдвига поля четвертого столбца вправо для достижения совпадения с соответствующим полем предшествующих дизъюнктов (для младших дизъюнктов, старшей переменной в которых является x₂, параметром сдвига полагается 3).

После снятия сигнала сброса первый счетчик 24, формирующий адрес обращения к памяти, и регистр 1, содержимое которого является начальным назначением переменных, обнулены. При этом на N-разрядные входы 16, 27 и 8 спецпроцессора поступает информация, соответствующая первому (DIS), второму (MASK) и третьему (INCR) полям строки с нулевым адресом таблицы 1 на фиг.3. На выходе первой 15 схемы сравнения формируется признак равенства выделенных полем MASK разрядов регистра 1 с выделенными разрядами поля DIS. На выходе четвертого 29 элемента ИЛИ формируется признак того, что старшая переменная дизъюнкта инвертирована. В случае дизъюнкта C₀(X₀⁰,X₁⁰,X₂⁰), активный сигнал формируется на втором выходе дешифратора 17. Это приводит к записи информации поля А1, поступающей с входа 34 через второй мультиплексор на информационный вход первого 24 счетчика. В результате на выходе первого 24 счетчика формируется адрес «4». Одновременно в регистр 1 записывается побитная сумма по модулю два содержимого регистра 1 и поля INCR. Эта операция выполняется посредством первого 6 мультиплексора и N-разрядной схемы 5 сложения по модулю два. При этом на выходе регистра 1 формируется новый код назначения переменных {00000100}.

При выборке следующих дизъюнктов по адресам «4», «5», «6», «7», «9», «10», «11», «13» конфликта дизъюнкта с текущим назначением переменных не возникает.

Следующим «действующим» дизъюнктом, конфликтующим с текущим назначением переменных, является дизъюнкт С₁₄(Х₀⁰,Х₃⁰,Х₇⁰) по адресу Этот конфликт порождает новое назначение переменных - {10000100}. Процесс преобразования регистра 1 проиллюстрирован в таблице 3 на фиг. 5.

Следующим является дизъюнкт С₁₅(Х₁⁰,Х₆⁰,Х₇¹) по адресу Этот дизъюнкт конфликтует с текущим назначением переменных. Особенностью конфликта является то, что он вызывает перенос, распространяемый в сторону младших разрядов назначения переменных, требующий дополнительных тактов работы спецпроцессора. На время этих дополнительных тактов активный четвертый выход дешифратора 17 устанавливает первый 11 и четвертый 36 RS-триггеры. Установка четвертого 36 RS-триггера приводит к инкременту содержимого второго 41 счетчика и переводит первый 6 мультиплексор в режим передачи на вход схемы 5 сложения по модулю два информации с выхода сдвигового регистра 7. В сдвиговом регистре 7 сдвигается код INCR, ранее загруженный с входа 8 спецпроцессора. Операция подсчета числа позиций переноса во втором 41 счетчике продолжается, пока на выходе первого 10 элемента ИЛИ присутствует единичный сигнал.

Затем запускается процесс поиска номера дизъюнкта для корректного продолжения процесса преобразования содержимого регистра 1. По адресу, заданному первым 24 счетчиком, выбирается следующий адрес, записываемый с K-разрядного входа 33 в упомянутый счетчик. Информация, поступающая на K-разрядный вход 34 спецпроцессора, используется как вычитаемое из содержимого второго 41 счетчика. Этот процесс заканчивается, когда вырабатывается активный сигнал на выходе «равно» или выходе «меньше» второй 40 схемы сравнения.

Особенность в формировании последующих адресов возникает при активном сигнале «меньше» на выходе второй 40 схемы сравнения. Этот сигнал устанавливает третий RS-триггер, который сбрасывается либо при конфликте с текущим назначением переменных дизъюнкта, имеющего неинвертированную старшую переменную, либо когда после дизъюнкта с неинвертированной старшей переменной (фиксируется вторым 18 RS-триггером) следует дизъюнкт с инвертированной старшей переменной.

Для рассматриваемой булевой формулы дальнейшая последовательность формируемых адресов выглядит следующим образом: «4», «5», «6», «7», «8», «10», «12», «12», «10», «8», «4», «0», «1», «4», «6», «7», «8», «9», «10», «11», «13»,«14», «17», «0», «0», «1», «2», «4», «5»,

Нижним подчеркиванием выделены номера дизъюнктов, вступающих в конфликт с текущим назначением переменных.

При наличии единицы в младшем разряде сдвигового регистра 7 и активного уровня на выходе первого 10 элемента ИЛИ на выходе 14 второго 13 элемента И устанавливается активный уровень сигнала, свидетельствующий о невыполнимости булевой формулы. Невыполнимость рассматриваемой формулы устанавливается за 68 тактов работы спецпроцессора.

Выполнимость формулы фиксируется при появлении на выходе 25 первого 24 счетчика адреса, превышающего число дизъюнктов формулы. Выполняющий формулу набор значений переменных считывается с N-разрядного выхода 4 регистра 1.

В таблице 2 на фиг. 4 приведены семнадцать выполнимых формул, каждая их которых получена удалением из невыполнимой формулы F_N одного из дизъюнктов. Формула F_k получается из F_N удалением дизъюнкта C_k.

Для каждой из таких формул приведен выполняющий набор, начиная со старших переменных (х₇, x₆, х₅, х₄, х₃, х₂, x₁, х₀).