Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний

Описывается подход к проверке противоречивости множества дизъюнктов в исчислении высказываний методом резолюций, основанный на модифицированном TSS-методе решения систем линейных однородных диофантовых уравнений. Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний An a...

Повний опис

Збережено в:

Бібліографічні деталі
Дата:	2008
Автори:	Крывый, С.Л., Волошин, С.В., Маркова, Н.С.
Формат:	Стаття
Мова:	Російська
Опубліковано:	Інститут програмних систем НАН України 2008
Теми:	Теоретичні та методологічні основи програмування
Онлайн доступ:	https://nasplib.isofts.kiev.ua/handle/123456789/645
Теги:	Додати тег Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:	Digital Library of Periodicals of National Academy of Sciences of Ukraine
Цитувати:	Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний / С.Л. Крывый, С.В. Волошин, Н.С. Маркова // Пробл. програмув. — 2008. — N 2-3. — С. 25-30. — Бібліогр.: 4 назв. — рус.

Репозитарії

Digital Library of Periodicals of National Academy of Sciences of Ukraine

_version_	1859686901478326272
author	Крывый, С.Л. Волошин, С.В. Маркова, Н.С.
author_facet	Крывый, С.Л. Волошин, С.В. Маркова, Н.С.
citation_txt	Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний / С.Л. Крывый, С.В. Волошин, Н.С. Маркова // Пробл. програмув. — 2008. — N 2-3. — С. 25-30. — Бібліогр.: 4 назв. — рус.
collection	DSpace DC
description	Описывается подход к проверке противоречивости множества дизъюнктов в исчислении высказываний методом резолюций, основанный на модифицированном TSS-методе решения систем линейных однородных диофантовых уравнений. Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний An approach to checking of satisfaction problem of propositional disjunction set by using resolution method is described. This algorithm is used TSS-method for solution of homogeneous systems of linear Diophantine equations. An algorithm for checking of satisfaction problem for propositional disjunction set
first_indexed	2025-11-30T22:57:30Z
format	Article
fulltext	Теоретичні та методологічні основи програмування © С.Л. Крывый, С.В. Волошин, Н.С. Маркова, 2008 ISSN 1727-4907. Проблеми програмування. 2008. № 2-3. Спеціальний випуск 25 УДК 51.681.3 АЛГОРИТМ ПРОВЕРКИ ПРОТИВОРЕЧИВОСТИ МНОЖЕСТВА ДИЗЪЮНКТОВ В ИСЧИСЛЕНИИ ВЫСКАЗЫВАНИЙ С.Л. Крывый, С.В. Волошин, Н.С. Маркова Институт кибернетики им. В.М. Глушкова НАН Украины, Киев, проспект Академика Глушкова, 40. Тел: (044) 526 2128, е-mail: svoloshyn@gmail.com Описывается подход к проверке противоречивости множества дизъюнктов в исчислении высказываний методом резолюций, основанный на модифицированном TSS-методе решения систем линейных однородных диофантовых уравнений. Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний An approach to checking of satisfaction problem of propositional disjunction set by using resolution method is described. This algorithm is used TSS-method for solution of homogeneous systems of linear Diophantine equations. An algorithm for checking of satisfaction problem for propositional disjunction set Введение Проверка противоречивости множества дизъюнктов является одной из основных задач при проектировании и верификации программного и технического обеспечения современных ЭВМ, а также в теории и практике логического вывода. Одним из наиболее практичных методов определения противоречивости множества дизъюнктов в исчислении высказываний является метод резолюций, о котором и пойдет речь в данной работе. При этом множество дизъюнктов, представляющих некоторую формулу исчисления высказываний или булеву функцию, преобразуется в систему линейных однородных диофантовых уравнений с коэффициентами из множества {0, 1, –1}. Идея предлагаемого метода представлена в [1] и данная работа является её развитием. 1. Необходимые сведения Литерой в исчислении высказываний (ИВ) называется атомарная формула или отрицание атомарной формулы. Дизъюнктом называется дизъюнкция конечного числа литер, а однолитерным дизъюнктом называется дизъюнкт, являющийся литерой. Однолитерный дизъюнкт называется негативным, если он является отрицанием атомарной формулы, в противном случае он называется позитивным. Однолитерный дизъюнкт также называется единичным. Литеры p и p¬ называются контрарными. Правило резолюций для ИВ имеет вид: rqrpqp ∨∨¬∨ a, , где p – литера, а q , r – произвольные дизъюнкты. Дизъюнкт, полученный в результате применения правила резолюций к дизъюнктам C и C′ , называется резольвентой данных дизъюнктов. Известно, что произвольную формулу ИВ можно представить в конъюнктивной нормальной форме (КНФ), т. е. в виде конъюнкции множества дизъюнктов. Обычно формулу представляют в виде множества ее дизъюнктов, а каждому такому множеству можно однозначно сопоставить матрицу из коэффициентов –1, 0 и 1. Эта матрица строится так: дизъюнктам соответствуют строки, а столбцы соответствуют атомарным формулам, входящим в дизъюнкты. При этом на пересечении i -й строки и j -го столбца, соответствующего атомарной формуле p , стоит –1, если i -й дизъюнкт содержит литеру p¬ ; 1, если i -й дизъюнкт содержит литеру p ; 0, если i -й дизъюнкт не содержит ни литеры p ни литеры p¬ . Следовательно, размерность матрицы, построенной таким образом, равна mS × , где S – количество дизъюнктов в множестве S , а m – количество атомарных формул, входящих в дизъюнкты множества S . Пример 1. Для множества дизъюнктов S , атомарные формулы которого расположены в порядке srqp ,,, , ,,, srqprqprqp ∨∨∨∨∨∨∨ ,,, sqpsrpsrq ∨∨∨∨∨∨ где x означает отрицание формулы x , соответствующая матрица имеет вид Теоретичні та методологічні основи програмування 26 . 1011 1101 1110 1111 0111 0111                     −− −− −− − − =sA 2. Оптимизация исходных данных Проверка противоречивости множества дизъюнктов S может быть выполнена с помощью анализа матрицы T SA , транспонированной к матрице SA . Действительно, получение пустого дизъюнкта с помощью правила резолюций, как будет показано далее, равносильно поиску линейной зависимости между столбцами матрицы T SA . Данный поиск затрудняется тем, что при сложении двух столбцов матрицы T SA (а это соответствует построению резольвенты двух дизъюнктов, соответствующих этим столбцам) могут порождаться тавтологичные дизъюнкты. Следовательно, допустимыми будут не все возможные комбинации столбцов, а только те, которые не порождают тавтологий. Комбинации двух дизъюнктов будет допустимой, если эти дизъюнкты содержат только одну контрарную пару формул. Например, рассмотрим второй и пятый дизъюнкты из множества S , приведенного в примере 1. Эти дизъюнкты можно комбинировать, так как они порождают резольвенту srq ∨∨ (т. е. новый столбец ( )T1,1,1,0 ), А первый и второй дизъюнкты из S при применении к ним правила резолюций порождают тавтологию 11 =∨=∨∨ rrqq . Полученные таким способом тавтологии бесполезны для дальнейшей проверки противоречивости и появления таких резольвент необходимо избегать. Чтобы избежать появления тавтологичных резольвент в процессе поиска допустимых комбинаций, выполняется проверка наличия других контрарных пар в комбинируемых дизъюнктах. Если такие пары существуют, то резольвента этих столбцов не строится, в противном случае выполняется покомпонентная дизъюнкция соответствующих столбцов. Анализируя матрицу T SA и используя свойства правила резолюций, можно выполнить некоторые её оптимизирующие преобразования, позволяющие упростить как саму матрицу, так и процесс резолюционного вывода. Первое оптимизирующее преобразование связано с наличием в множестве S единичных дизъюнктов. Если в множестве дизъюнктов имеется однолитерный дизъюнкт, то с его помощью удаляются все контрарные ему литеры в остальных дизъюнктах. После этого сам дизъюнкт и все дизъюнкты, его содержащие, удаляются из текущего множества дизъюнктов. Это преобразование позволяет уменьшить размеры матрицы T SA и более эффективно выполнять вычисления. Пример 2. Пусть множество S включает такие дизъюнкты: ssrsrqrqpp ,,,, ∨∨∨∨∨ . Тогда матрица T SA имеет вид        − − − − = 11100 01110 00110 00011 T SA . Редукция T SA с помощью первого оптимизирующего преобразования в конце концов приводит к пустому дизъюнкту. Действительно,               ⇒               − ⇒               − − ⇒               − − − ⇒               − − − − 0 0 0 0 00 00 11 00 000 111 011 000 1110 0111 0011 0000 11100 01110 00110 00011 , а это значит, что множество S противоречиво. Теоретичні та методологічні основи програмування 27 Второе оптимизирующее преобразование. Если в матрице T SA имеется строка, содержащая только лишь негативные (позитивные) литеры, то из T SA удаляются все столбцы, которым принадлежат ненулевые значения данной строки. Например, если T SA имеет вид        − −− −− = 00010 00101 10011 01011 T SA , то очевидно, что второй столбец не будет принимать участия в получении пустого дизъюнкта, поскольку атомарной формуле, которой соответствует данная строка, нет контрарной пары. Поэтому проверять противоречивость S можно исходя из матрицы        − − − = 0000 0011 1001 0101 T SA . Третье оптимизирующее преобразование. Это преобразование традиционное в методе резолюций – удаление наддизъюнктов в текущем множестве дизъюнктов. Поиск и удаление наддизъюнктов сводится к конъюнкции столбцов. При этом, если T n T n T n xxxyyyxxx ),,,(),,,(),,,( 212121 KKK =∧ , то второй дизъюнкт- столбец наддизъюнкт первого дизъюнкта-столбца. 3. Применение модифицированного TSS–алгоритма Рассмотрим одну из модификаций TSS-алгоритма [3] для решения задачи проверки противоречивости множества дизъюнктов в исчислении высказываний. Эта модификация хороша тем, что ее применение позволяет не только проверять противоречивость, но и определять минимальные подмножества дизъюнктов, являющиеся противоречивыми. Построим по множеству дизъюнктов S систему однородных линейных диофантовых уравнений (СЛОДУ) 0=xAT S . Тогда определение противоречивости множества дизъюнктов S сводится к определению совместности СЛОДУ 0=xAT S согласно следующему алгоритму. АПП-TSS ( S ) Вход: Множество дизъюнктов S . Выход: ВЫПОЛНИМО или ПРОТИВОРЕЧИВО. Метод: начало 1) построить T SA для S ; 2) оптимизировать T SA ; 3) 1:=i ; 4) вычислить TSS для ( ) 0=xLi ; 5) для всех 1+= ij до p выполнить (Для всех TSSe ∈ найти значения ( )eL j ); Построить матрицу ( ) pj LLSA K=′ ) (столбцы, обозначенные pj LL K в матрице ( )SA′ , означают столбцы значений уравнений ( ) ( )xLxL pj K на векторах TSSe ∈ ) кц; 6) удалить те TSSe ∈ , которые порождают тавтологии; (т. е. те вектора, для которых значения ( ) 0=eL j , причем ненулевые координаты e не попадают на нулевые коэффициенты ( )xL j при вычислении значений ( )eL j ); 7) если ∅=TSS , то (ВЫПОЛНИМО; на 9); 8) 1: += ii ; Если pi ≤ то (Построить TSS , используя значения ( )xLi для матрицы ( )SA′ ; ij =: ; на 5) иначе если ∅=TSS то ВЫПОЛНИМО Теоретичні та методологічні основи програмування 28 иначе ПРОТИВОРЕЧИВО; 9) СТОП; конец Обоснованием данного алгоритма служит такая теорема. Теорема. Множество дизъюнктов S противоречиво тогда и только тогда, когда СЛОДУ 0=xAT S имеет непустое множество решений, сгенерированное алгоритмом АПП-TSS. Доказательство. ( )→ Если СЛОДУ 0=xAT S имеет хотя бы одно ненулевое решение, то в силу построения алгоритмом АПП-TSS, очевидно, что дизъюнкты, соответствующие ненулевым координатам решения, составляют минимальное противоречивое подмножество дизъюнктов. А это значит что и все множество S тоже будет противоречивым. ( )← Пусть S противоречивое множество дизъюнктов, по которому вышеописанным способом построена СЛОДУ 0=xAT S . Рассмотрим первое из уравнений этой СЛОДУ и найдем базис его множества решений с помощью АПП–TSS. Это уравнение должно иметь хотя бы одно решение, поскольку в противном случае это противоречит тому, что S противоречиво. Пусть ( )nxxxx ,,, 21 K= – решение этого уравнения. Если x имеет две ненулевые координаты ix и jx , то это значит, что x соответствует резольвенте дизъюнктов iC и jC . А если x имеет одну ненулевую координату kx , то соответствующий дизъюнкт не резольвируется ни с каким дизъюнктом из S . Отсюда следует, что все решения первого уравнения соответствуют всем возможным резольвентам по одной из переменных. Но тогда дизъюнкты, содержащие данную переменную с отрицанием (или без), можно удалить, так как они в дальнейшем не будут принимать участия в резолюционном выводе. Повторяя аналогичную процедуру со вторым, третьим и т. д. p-м уравнением СЛОДУ, получаем решения СЛОДУ и такое решение должно существовать в силу противоречивости множества S . Теорема доказана. 4. Иллюстрирующие примеры Рассмотрим применение этого алгоритма к множеству дизъюнктов, приведенному в примере 1 и которому соответствует СЛОДУ из примера 2. Построение TSS для первого уравнения дает такое множество решений (во 2, 3 и 4 столбцах показаны значения соответственно 2, 3 и 4 уравнений, если подставить решения первого уравнения в эти уравнения): TSS 2L 3L 4L 000100 –1 –1 1 110000 0 – – 011000 2 0 – 010010 1 2 1 100001 0 – – 001001 2 –1 –2 000011 1 1 0 После чистки получаем векторы TSS 2L 3L 4L 000100 –1 –1 1 010010 1 2 1 001001 2 –1 –2 Комбинирование по значениям второго столбца порождает такие векторы TSS 3L 4L 010110 1 2 001201 –3 0 После чистки получаем единственный вектор TSS 3L 4L 010110 1 2 Дальнейшее комбинирование невозможно выполнить, поскольку комбинировать не с кем. Следовательно, исходная СЛОДУ не имеет решений (несовместна) и множество дизъюнктов S непротиворечиво. Рассмотрим еще один пример, который взят из учебника по операционным системам и который можно найти в [4]. Являются ли формулы BP ¬∧ и NI ¬∧ следствиями нижеприведенных формул Теоретичні та методологічні основи програмування 29 PA → , ( ) DBP →¬∧ , ( )HMSD ∧∧→ , RNH →∧ , IRH →¬∧ , RBA ¬∧¬∧ ? Преобразуем данные формулы к КНФ PA∨¬ , DBP ∨∨¬ , SD ∨¬ , MD ∨¬ , HD ∨¬ , RNH ∨¬∨¬ , IRH ∨∨¬ , A , B¬ , R¬ . Добавляем к имеющимся дизъюнктам отрицания формул BP ¬∧ и NI ¬∧ , которые после приведения к КНФ принимают вид: BP ∨¬ , NI ∨¬ . Полученному множеству дизъюнктов соответствует СЛОДУ (строки, которые соответствуют переменным обозначены слева этими переменными) . 0100000100000 0100001000000 0001001100000 0000001110000 0000000001000 0000000000100 0000000011110 0010100000010 0010000000011 0000010000001                                 =− =− =− =−− = = =−−− =− =−− =− =⋅ N I R H M S D B P A xAT S Применяя алгоритм АПП-TSS к полученному множеству дизъюнктов, получаем два решения ( )01,0,1,1,0,0,0,0,0,,0,11 =x , которому соответствует такое минимальное противоречивое подмножество дизъюнктов PA∨¬ , A , B¬ , BP ∨¬ , второе решение ( )10,1,1,1,1,1,1,0,0,1,1,2 =x , которому соответствует такое минимальное противоречивое подмножество дизъюнктов: PA∨¬ , A , B¬ , DBP ∨∨¬ , HD ∨¬ , RNH ∨¬∨¬ , IRH ∨∨¬ , R¬ , NI ∨¬ . В правильности этого решения можно убедиться непосредственной проверкой. Следовательно, поскольку отрицания первой и второй из проверяемых формул входят в соответствующие противоречивые подмножества, то сами формулы являются логическими следствиями данного множества дизъюнктов. 5. Результаты экспериментов Приведены результаты экспериментов на множествах дизъюнктов, которые встречаются в процессе проектирования реальных систем. В целях экономии приведены только лишь наиболее существенные множества дизъюнктов и результаты их проверки на противоречивость. Эксперименты проводились на компьютере IBM PC с RAM 256 Мб, процессор: AMD Athlon XP 1800+: 1) Матрица ( )20301 ×TA : 1 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 1 0 0 -1 0 1 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 -1 0 0 1 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 -1 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 1 0 -1 0 1 0 0 0 0 0 0 0 -1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 -1 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 1 0 0 -1 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 -1 0 -1 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 -1 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 -1 0 0 -1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 -1 0 0 0 -1 0 0 0 -1 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 1 0 0 0 -1 0 0 0 0 1 0 0 0 0 0 0 0 2) Матрица ( )36302 ×TA : -1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 -1 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 -1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 -1 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 -1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 -1 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 -1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 -1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 -1 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 1 Теоретичні та методологічні основи програмування 30 3) Матрица ( )40353 ×TA : 1 0 0 0 0 -1 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 -1 0 0 0 0 1 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 -1 0 1 0 0 -1 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 1 -1 0 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 1 0 0 1 0 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 1 1 0 0 -1 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 0 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 0 0 0 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 0 0 0 0 -1 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 0 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 0 0 -1 0 -1 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 -1 -1 0 -1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 -1 0 -1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 1 0 0 0 1 0 0 0 0 0 -1 1 1 0 -1 0 1 0 1 0 0 0 -1 0 -1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 1 0 0 0 0 0 0 -1 0 1 1 0 -1 0 0 0 0 0 1 0 1 0 0 0 -1 0 -1 0 0 1 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1 0 0 0 -1 -1 0 1 0 0 0 1 0 1 0 0 0 -1 0 -1 0 0 1 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 -1 0 -1 0 0 0 0 0 0 0 0 1 0 0 0 0 0 -1 0 0 -1 -1 1 1 0 0 0 0 0 1 0 0 1 0 0 1 0 1 0 0 0 -1 0 -1 -1 0 0 0 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 1 0 1 0 0 0 -1 0 0 -1 0 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 1 1 0 0 0 0 0 1 0 0 0 0 0 0 1 0 1 0 0 0 -1 -1 0 -1 0 1 0 -1 0 0 0 1 0 0 1 0 0 -1 0 0 0 1 0 0 0 0 1 0 0 0 0 0 1 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 0 -1 0 1 0 0 0 -1 -1 0 -1 0 0 0 1 0 0 0 1 0 0 0 0 0 1 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 0 -1 0 0 0 1 0 0 0 -1 0 0 0 1 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 0 0 0 1 0 0 0 -1 0 0 0 0 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 0 -1 0 0 0 0 -1 0 0 0 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 1 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 1 0 0 0 -1 0 0 -1 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 1 0 0 -1 0 0 1 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 -1 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 -1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 -1 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 0 0 0 0 0 -1 Общее время вычисления Система Количество решений Без оптимизации С оптимизацией Для множества дизъюнктов, соответствующих матрице TA1 0 313 мс 47мс Для множества дизъюнктов, соответствующих матрице TA2 6 438 мс 546 мс Для множества дизъюнктов, соответствующих матрице TA3 0 3,5 мин. 94 мс Заключение Отметим, что описанный метод применялся при проверке выполнимости булевых функций, представленных в КНФ. Хорошо известно, что проблема проверки выполнимости булевой функции, зависящей не менее чем от трех переменных, имеет экспоненциальную оценку временной сложности. Данный алгоритм в худшем случае тоже имеет экспоненциальную оценку временной сложности. Однако, в среднем сложность данного алгоритма лучше, чем сложность классических методов проверки выполнимости булевых функций [2]. 1. Кривой С.Л., Хайдер М., Багрий Р.А. Приложения алгоритмов решения систем линейных констрейнтов. Материалы междун. конф. “Алгебра, логика и кибернетика”. – Иркутск, 25–28 августа 2004 – С. 165–166. 2. Васильев Ю.Л., Ветухновский Ф.Я., Глаголев В.В. и др. Дискретная математика и математические вопросы кибернетики. – М: Наука, 1974. – 311 с. 3. Кривой С.Л. Алгоритмы решения систем линейных ограничений в целочисленных областях. // Кибернетика и системный анализ. – 2006. – № 2. – С. 3 – 17. 4. Кривий С.Л. Дискретна математика: вибранi питання. – К.: Видавничий дім “Києво-Могилянська академiя”, 2007. – 570 с.
id	nasplib_isofts_kiev_ua-123456789-645
institution	Digital Library of Periodicals of National Academy of Sciences of Ukraine
issn	1727-4907
language	Russian
last_indexed	2025-11-30T22:57:30Z
publishDate	2008
publisher	Інститут програмних систем НАН України
record_format	dspace
spelling	Крывый, С.Л. Волошин, С.В. Маркова, Н.С. 2008-05-30T14:13:37Z 2008-05-30T14:13:37Z 2008 Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний / С.Л. Крывый, С.В. Волошин, Н.С. Маркова // Пробл. програмув. — 2008. — N 2-3. — С. 25-30. — Бібліогр.: 4 назв. — рус. 1727-4907 https://nasplib.isofts.kiev.ua/handle/123456789/645 51.681.3 Описывается подход к проверке противоречивости множества дизъюнктов в исчислении высказываний методом резолюций, основанный на модифицированном TSS-методе решения систем линейных однородных диофантовых уравнений. Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний An approach to checking of satisfaction problem of propositional disjunction set by using resolution method is described. This algorithm is used TSS-method for solution of homogeneous systems of linear Diophantine equations. An algorithm for checking of satisfaction problem for propositional disjunction set ru Інститут програмних систем НАН України Теоретичні та методологічні основи програмування Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний An algorithm for checking of satisfaction problem for propositional disjunction set Article published earlier
spellingShingle	Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний Крывый, С.Л. Волошин, С.В. Маркова, Н.С. Теоретичні та методологічні основи програмування
title	Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний
title_alt	An algorithm for checking of satisfaction problem for propositional disjunction set
title_full	Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний
title_fullStr	Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний
title_full_unstemmed	Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний
title_short	Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний
title_sort	алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний
topic	Теоретичні та методологічні основи програмування
topic_facet	Теоретичні та методологічні основи програмування
url	https://nasplib.isofts.kiev.ua/handle/123456789/645
work_keys_str_mv	AT kryvyisl algoritmproverkiprotivorečivostimnožestvadizʺûnktovvisčisleniivyskazyvanii AT vološinsv algoritmproverkiprotivorečivostimnožestvadizʺûnktovvisčisleniivyskazyvanii AT markovans algoritmproverkiprotivorečivostimnožestvadizʺûnktovvisčisleniivyskazyvanii AT kryvyisl analgorithmforcheckingofsatisfactionproblemforpropositionaldisjunctionset AT vološinsv analgorithmforcheckingofsatisfactionproblemforpropositionaldisjunctionset AT markovans analgorithmforcheckingofsatisfactionproblemforpropositionaldisjunctionset

Алгоритм проверки противоречивости множества дизъюнктов в исчислении высказываний

Репозитарії

Схожі ресурси