Метод решения k-SAT-задачи сведением ее к задаче о покрытии
Предложен алгоритм решения k-SAT-задачи в среднем за полиномиальное время и 3-SATзадачи за полиномиальное время. Предлагаемый метод позволяет существенно сократить время решения SAT-задач. Запропоновано алгоритм розв’язку k-SAT-задачі в середньому за поліноміальний час і 3-SAT-задачі за поліноміальн...
Збережено в:
| Опубліковано в: : | Электронное моделирование |
|---|---|
| Дата: | 2015 |
| Автори: | , |
| Формат: | Стаття |
| Мова: | Російська |
| Опубліковано: |
Інститут проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України
2015
|
| Теми: | |
| Онлайн доступ: | https://nasplib.isofts.kiev.ua/handle/123456789/101162 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Цитувати: | Метод решения k-SAT-задачи сведением ее к задаче о покрытии / С.В. Листровой, А.В. Сидоренко // Электронное моделирование. — 2015. — Т. 37, № 5. — С. 17-34. — Бібліогр.: 4 назв. — рос. |
Репозитарії
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860212760477958144 |
|---|---|
| author | Листровой, С.В. Сидоренко, А.В. |
| author_facet | Листровой, С.В. Сидоренко, А.В. |
| citation_txt | Метод решения k-SAT-задачи сведением ее к задаче о покрытии / С.В. Листровой, А.В. Сидоренко // Электронное моделирование. — 2015. — Т. 37, № 5. — С. 17-34. — Бібліогр.: 4 назв. — рос. |
| collection | DSpace DC |
| container_title | Электронное моделирование |
| description | Предложен алгоритм решения k-SAT-задачи в среднем за полиномиальное время и 3-SATзадачи за полиномиальное время. Предлагаемый метод позволяет существенно сократить время решения SAT-задач.
Запропоновано алгоритм розв’язку k-SAT-задачі в середньому за поліноміальний час і 3-SAT-задачі за поліноміальний час. Запропонований метод дозволяє істотно скоротити час розв’язку SAT-задач .
An algorithm for solving the k-SAT-problem for the average polynomial time and 3-SAT-problem for the polynomial time. The proposed method can significantly reduce the time to solve SAT-problems.
|
| first_indexed | 2025-12-07T18:14:53Z |
| format | Article |
| fulltext |
ÓÄÊ 519.682.1
Ñ.Â. Ëèñòðîâîé, ä-ð òåõí. íàóê
Óêðàèíñêèé ãîñóäàðñòâåííûé óíèâåðñèòåò
æåëåçíîäîðîæíîãî òðàíñïîðòà
(Óêðàèíà, 61050, Õàðüêîâ, ïë. Ôåéðáàõà, 7,
òåë. (050) 9355042, å-mail: om1@ yandex.ru),
À.Â. Ñèäîðåíêî
Íàó÷íî-ïðîèçâîäñòâåííîå ïðåäïðèÿòèå «Ñòàëüýíåðãî»
(Óêðàèíà, 61105, Õàðüêîâ, óë. Ôåäîðåíêî 9,
òåë. (050) 9800852, å-mail: cdandrey@gmail.com)
Ìåòîä ðåøåíèÿ k-SAT-çàäà÷è
ñâåäåíèåì åå ê çàäà÷å î ïîêðûòèè
Ïðåäëîæåí àëãîðèòì ðåøåíèÿ k-SAT-çàäà÷è â ñðåäíåì çà ïîëèíîìèàëüíîå âðåìÿ è 3-SAT-
çàäà÷è çà ïîëèíîìèàëüíîå âðåìÿ. Ïðåäëàãàåìûé ìåòîä ïîçâîëÿåò ñóùåñòâåííî ñîêðàòèòü
âðåìÿ ðåøåíèÿ SAT-çàäà÷.
Çàïðîïîíîâàíî àëãîðèòì ðîçâ’ÿçêó k-SAT-çàäà÷³ â ñåðåäíüîìó çà ïîë³íîì³àëüíèé ÷àñ ³
3-SAT-çàäà÷³ çà ïîë³íîì³àëüíèé ÷àñ. Çàïðîïîíîâàíèé ìåòîä äîçâîëÿº ³ñòîòíî ñêîðîòèòè ÷àñ
ðîçâ’ÿçêó SAT-çàäà÷ .
Ê ë þ ÷ å â û å ñ ë î â à : SAT-çàäà÷à, ïîëèíîìèàëüíàÿ ñâîäèìîñòü.
Ðåøåíèå SAT-çàäà÷ âåñüìà àêòóàëüíî â ñèñòåìàõ àâòîìàòè÷åñêîé ïðî-
âåðêè äîêàçàòåëüñòâ, ãäå ôîðìóëîé íàçûâàþò íàáîð êëîçîâ, ïîä êîòîðû-
ìè ïîíèìàþò äèçúþíêöèþ íåêîòîðîãî êîëè÷åñòâà ëèòåðàëîâ — ïåðåìå-
ðåííûõ Õ è X . Áîëüøîå çíà÷åíèå ýòè çàäà÷è èìåþò ïðè âûÿñíåíèè âû-
ïîëíèìîñòè ñõåì CIRCUIT-SAT è ðàñïîçíàâàíèè îáðàçîâ. Âàæíîå ìåñòî â
èññëåäîâàíèè SAT-çàäà÷ çàíèìàåò ðàçðàáîòêà ïðîãðàìì äëÿ èõ ðåøåíèÿ, íà-
çûâàåìûõ SAT-ñîëâåðàìè. Ñîâðåìåííûå SAT-ñîëâåðû ñïîñîáíû áûñòðî ðå-
øàòü ìíîãèå çàäà÷è, ñ÷èòàâøèåñÿ íåðåøàåìûìè íåñêîëüêî ëåò íàçàä.
Èçâåñòíî ìíîãî ýêñïîíåíöèàëüíûõ àëãîðèòìîâ ðåøåíèÿ SAT-çàäà÷è è
ýâðèñòè÷åñêèõ ïîäõîäîâ ïîëèíîìèàëüíîé ñëîæíîñòè ê åå ðåøåíèþ. Íà-
ïðèìåð, â àëãîðèòìå Ìîíèåíà è Øïèêåðìàéåðà äëÿ çàäà÷è 3-SAT èñïîëüçîâàí
ïðîñòîé ïåðåáîð: âìåñòî êàæäîé ïåðåìåííîé ïîî÷åðåäíî âûïîëíÿåòñÿ ïîäñòà-
íîâêà åäèíèöû èëè íóëÿ è çàòåì ðåêóðñèâíî ðåøàåòñÿ çàäà÷à ìåíüøåãî ðàçìå-
ðà. Ýòîò àëãîðèòì èìååò âðåìåííóþ ñëîæíîñòü Î (1,84n). Àëãîðèòì ðåøåíèÿ
çàäà÷è ïðîïîçèöèîíàëüíîé âûïîëíèìîñòè ôîðìóë â êîíúþíêòèâíîé íîð-
ìàëüíîé ôîðìå [1] èìååò âðåìåííóþ ñëîæíîñòü Î (1,074n) .
ISSN 0204–3572. Ýëåêòðîí. ìîäåëèðîâàíèå. 2015. Ò. 37. ¹ 5 17
� Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî, 2015
 îáùåì ñëó÷àå ìîæíî âûäåëèòü äâà îñíîâíûõ òèïà àëãîðèòìîâ äëÿ
ðåøåíèÿ SAT-çàäà÷:
1) àëãîðèòìû ëîêàëüíîãî ïîèñêà, êîòîðûå íà÷èíàþòñÿ ñ êàêîãî-ëèáî
íàáîðà çíà÷åíèé (íå âûïîëíÿþùèå âñþ ôîðìóëó); çàòåì èõ ìîäèôèöè-
ðóþò, ïûòàÿñü ïîñëåäîâàòåëüíî ïðèáëèçèòüñÿ ê âûïîëíÿþùåìó íàáîðó.
2) òàê íàçûâàåìûå DPLL-àëãîðèòìû (ñîîòâåòñòâåííî èìåíàì ñîçäàòå-
ëåé: Davis, Putnam, Logemann, Loveland (1968 ã.)), îáõîäÿùèå äåðåâî âñå-
âîçìîæíûõ íàáîðîâ è âûïîëíÿþùèå ïîèñê â ãëóáèíó.
Ïðåäëàãàåòñÿ ýôôåêòèâíûé àëãîðèòì ðåøåíèÿ 3-SAT-çàäà÷è è ïðîèç-
âîëüíîé k-SAT-çàäà÷è ïîëèíîìèàëüíîé ñëîæíîñòè.
Ôîðìàëèçàöèÿ SAT-çàäà÷è è åå ðåøåíèå. Ðàññìîòðèì áóëåâó ôóíê-
öèþ F x x xn( , , ..., )1 2 â êîíúþíêòèâíîé ôîðìå çàïèñè:
F x x x x x x xn n
n m( , , ..., ) ( ... ) ... (1 2 1 2 1
11 12 1 1� � � � � �� � � � � � �x xm mn
n2
2� �... ),
ãäå
x
x
x
i
i
i
�
�
�
�
�
�
�
�
, ,
, ;
1
0
� è � — áóëåâû îïåðàöèè, ìîäåëèðóþùèå ïðîñòåéøèå ëîãè÷åñêèå âûñêà-
çûâàíèÿ «ÈËÈ» è «È». Äëÿ ëþáîãî äâîè÷íîãî íàáîðà x x x xn� ( , , ..., )1 2
ôóíêöèÿ ïðèíèìàåò îäíî èç äâóõ âîçìîæíûõ çíà÷åíèé: 1 èëè 0. Çàäà÷à «âû-
ïîëíèìîñòü» çàêëþ÷àåòñÿ â îòâåòå íà âîïðîñ: ñóùåñòâóåò ëè íàáîð çíà÷åíèé
ïåðåìåííûõ x x x xn� ( , , ..., )1 2 , îáðàùàþùèé ôóíêöèþ F â åäèíèöó.
Êàê ïîêàçàíî â [2], SAT-çàäà÷ó ìîæíî ðàññìàòðèâàòü êàê çàäà÷ó î
ïîêðûòèè. Äëÿ ýòîãî ïî áóëåâîé ôóíêöèè ïîñòðîèì áóëåâó ìàòðèöó Â, â
êîòîðîé ñòîëáöàì ñîîòâåòñòâóþò ïåðåìåííûå ( , , ..., )X X X n1 2 è ( , ,...X X1 2
..., )X n , à ñòðîêàì — äèçúþíêòû áóëåâîé ôóíêöèè.  îáùåì ñëó÷àå ÷èñëî
ñòîëáöîâ â ìàòðèöå  ðàâíî 2n, à ÷èñëî ñòðîê — ÷èñëó äèçúþíêòîâ m â
áóëåâîé ôóíêöèè. Íàïðèìåð,
F X X X X X X X X X X X X� � � � � � � �( ) ( ) ( ) ( ) ( )1 2 3 1 2 3 1 3 3 1 1 2 . (1)
Ïåðåíóìåðóåì äèçúþíêòû áóëåâîé ôóíêöèè:
Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî
18 ISSN 0204–3572. Electronic Modeling. 2015. V. 37. ¹ 5
1 ( )X X X1 2 3� � 2 ( )X X X1 2 3� �
3 ( )X X1 3� 4 ( )X X3 1� 5 ( )X X1 2�
.
Òîãäà ìàòðèöà Â ïðèìåò âèä
B
X X X X X X
�
1
2
3
4
5
1 1 1 0 0 0
0 0 0 1 1 1
1 0 0 0 0 1
0 0 1 1 0 0
1 0 0 0 1 0
1 2 3 1 2 3
.
Ñòîëáöû, ñîîòâåòñòâóþùèå ïåðåìåííûì X j è X i â ìàòðèöå Â, áóäåì
íàçûâàòü èíâåðñíûìè. Åñëè â ìàòðèöå Â ñóùåñòâóåò ïîêðûòèå ñòðîê
åäèíèöàìè, ïðèíàäëåæàùåå íåèíâåðñíûì ñòîëáöàì, òî ýòî çíà÷èò, ÷òî
ôóíêöèÿ F âûïîëíèìà, åñëè òàêîãî ïîêðûòèÿ íå ñóùåñòâóåò, òî îíà íå-
âûïîëíèìà. Îáîçíà÷èì ïåðåìåííûå X j ÷åðåç Z j . Òîãäà ìàòðèöà  äëÿ
áóëåâîé ôóíêöèè (1) ïðèìåò ñëåäóþùèé âèä:
B
X X X Z Z Z
�
1
2
3
4
5
1 1 1 0 0 0
0 0 0 1 1 1
1 0 0 0 0 1
0 0 1 1 0 0
1 0 0 0 1 0
1 2 3 1 2 3
, (2)
ãäå Z j = 0, åñëè X j = 1, è Z j = 1, åñëè X j = 0.
Êàê ïîêàçàíî â [2], çàäà÷ó î ìèíèìàëüíîì ïîêðûòèè äëÿ ïðîèçâîëüíîé
ìàòðèöû Â, çàäàâàåìîé íåêîòîðîé áóëåâîé ôóíêöèåé
F X X X X X X X X Xl b k s r t q d h� � � � � � � � � �( ... ) ( ... ) ( ... ),
ìîæíî ðàññìàòðèâàòü êàê çàäà÷ó íàõîæäåíèÿ ìèíèìàëüíîãî íàáîðà ïåðå-
ìåííûõ {Xi = 1}, ïðè êîòîðûõ áóëåâà ôóíêöèÿ (1) âûïîëíèìà. Ýòó çàäà÷ó
ìîæíî çàïèñàòü â âèäå min{ }
j jX �1 ïðè âûïîëíåíèè îãðàíè÷åíèé
( ... ) ( ... ) ( ... )X X X X X X X X Xl b k s r t q d h� � � � � � � � � �1.
Ïåðåõîäÿ ê äâîéñòâåííîé áóëåâîé ôóíêöèè (â äèçúþíêòèâíîé íîðìàëü-
íîé ôîðìå (ÄÍÔ)), ïîëó÷àåì min { }
j jX �0 ïðè
X X X X X X X X Xl b k s r t q d h... ... ... ...� � � �0, (3)
Ìåòîä ðåøåíèÿ k-SAT-çàäà÷è ñâåäåíèåì åå ê çàäà÷å î ïîêðûòèè
ISSN 0204–3572. Ýëåêòðîí. ìîäåëèðîâàíèå. 2015. Ò. 37. ¹ 5 19
îòêóäà ñëåäóåò, ÷òî çàäà÷ó î íàèìåíüøåì ïîêðûòèè ìîæíî ðàññìàòðèâàòü
êàê çàäà÷ó íåëèíåéíîãî áóëåâîãî ïðîãðàììèðîâàíèÿ, êîòîðàÿ çàêëþ÷àåò-
ñÿ â íàõîæäåíèè íàèìåíüøåãî ÷èñëà ïåðåìåííûõ{ }X j � 0 , îáðàùàþùèõ â
íóëü ëåâóþ ÷àñòü îãðàíè÷åíèÿ (3). Åñëè ñóùåñòâóåò õîòÿ áû îäíî ïîêðû-
òèå, òî íåîáõîäèìî âûÿñíèòü, ñóùåñòâóåò ëè õîòÿ áû îäèí íàáîð ïåðå-
ìåííûõ { }X j � 0 , îáðàùàþùèõ â íóëü ëåâóþ ÷àñòü îãðàíè÷åíèÿ (3). Äëÿ
ìàòðèöû (2) óñëîâèå ñóùåñòâîâàíèÿ õîòÿ áû îäíîãî ïîêðûòèÿ èìååò âèä
X Z X X Z X X Z Zl b k s r t q d h... ... ... ...� � � �0 (4)
ïðè âûïîëíåíèè ñëåäóþùèõ óñëîâèé:
åñëè X j �1, òî Z j �0 ,
åñëè X j �0, òî Z j �1.
(5)
Òàêèì îáðàçîì, äëÿ óñòàíîâëåíèÿ âûïîëíèìîñòè áóëåâîé ôóíêöèè
òðåáóåòñÿ óñòàíîâèòü íàëè÷èå õîòÿ áû îäíîãî ïîêðûòèÿ ñòðîê åäèíèöàìè
â ìàòðèöå Â (2), óäîâëåòâîðÿþùåå óñëîâèþ (5). Äëÿ ýòîãî íåîáõîäèìî
ðåøèòü íåëèíåéíîå áóëåâî óðàâíåíèå (4), è ðåøåíèå ýòîãî óðàâíåíèÿ
äîëæíî óäîâëåòâîðÿòü óñëîâèþ (5). Îáîçíà÷èâ ïðîèçâîëüíûé äèçúþíêò
â (4) ÷åðåç S i , à ÷èñëî äèçúþíêòîâ — ÷åðåç m, çàäà÷ó (4), (5) ìîæíî
çàïèñàòü â âèäå
i
m
iS
�
�
1
0 . (6)
Äëÿ ðåøåíèÿ çàäà÷è (5), (6) ïåðåìåííûå áóëåâîé ôóíêöèè
x
x
z
j
j
j
�
�
�
�
�
�
�
�
, ,
, ,
1
0
ïðèíèìàþùèå çíà÷åíèÿ X j , Z j , áóäåì õàðàêòåðèçîâàòü âåñîâûìè õàðàê-
òåðèñòèêàìè h j , îïðåäåëÿþùèìè ÷àñòîòó ïîÿâëåíèÿ ïåðåìåííûõ X j è Z j
â ñëàãàåìûõ óðàâíåíèÿ (6). Ïðè ýòîì êàæäûé äèçúþíêò S i òàêæå áóäåì
õàðàêòåðèçîâàòü âåñîâîé õàðàêòåðèñòèêîé pi, ðàâíîé ñóììå ÷àñòîò ïåðå-
ìåííûõ hj, îáðàçóþùèõ äàííîå ñëàãàåìîå. Ïîä ïðåîáðàçîâàíèåì íåêîòî-
ðîé áóëåâîé ôóíêöèè Fr â Fr�1 áóäåì ïîäðàçóìåâàòü èçìåíåíèå ôóíêöèè
Fr â ðåçóëüòàòå ïîäñòàíîâêè â íåå ïàð X j �1, Z j �0 èëè X j �0, Z j �1.
Ïîñêîëüêó â ôóíêöèè Fr â ðåçóëüòàòå ïîäñòàíîâêè X j �1èëè Z j �1 ïîÿâ-
ëÿþòñÿ äèçúþíêòû ñ ìåíüøèì ÷èñëîì ïåðåìåííûõ, áóäåì âûïîëíÿòü
îïåðàöèþ ïîãëîùåíèÿ âèäà XZ X X� � . Åñëè â ðåçóëüòàòå ïîäñòàíîâêè â
íåå ïàð X j �1, Z j �0 èëè X j �0, Z j �1âûòåêàåò íåîáõîäèìîñòü âûïîëíå-
íèÿ ðàâåíñòâà X j � Z j �0 (ò.å. (6) ïðèíèìàåò âèä 1 = 0), òî áóäåì c÷èòàòü,
÷òî âîçíèêëî ïðîòèâîðå÷èå è ôóíêöèÿ Fr íåâûïîëíèìà. Åñëè â ïðîöåññå
Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî
20 ISSN 0204–3572. Electronic Modeling. 2015. V. 37. ¹ 5
ïðåîáðàçîâàíèÿ ïîÿâëÿþòñÿ äèçúþíêòû, ñîñòîÿùèå èç îäíîé ïåðåìåííîé,
òî ýòè ïåðåìåííûå ïîëàãàåì ðàâíûìè íóëþ è çàíîñèì èõ â ðåøåíèå.
Îñíîâíàÿ èäåÿ ðåøåíèÿ óðàâíåíèÿ (6) — âûáîð íåêîòîðîãî äèçúþíê-
òà â èñõîäíîé áóëåâîé ôóíêöèè F è ïðîâåðêà âîçìîæíîñòè îáíóëåíèÿ
âñåõ îñòàëüíûõ ñëàãàåìûõ ïðè îáíóëåíèè ïîî÷åðåäíî ïåðåìåííûõ, ïðè-
íàäëåæàùèõ âûáðàííîìó äèçúþíêòó. Ïðè ýòîì îáðàçóþòñÿ íåêîòîðûå
ïðîìåæóòî÷íûå ôóíêöèè Fr , â êîòîðûõ òàêæå âûäåëÿåì äèçúþíêòû è
ïûòàåìñÿ îáíóëèòü âñå ñëàãàåìûå íà îñíîâå âûáîðà îäíîãî äèçúþíêòà â
ýòèõ ôóíêöèÿõ, ïîëàãàÿ ïåðåìåííûå â âûáðàííûõ äèçúþíêòàõ ïîî÷åðåäíî
ðàâíûìè íóëþ. Ýòà ïðîöåäóðà ïðîäîëæàåòñÿ äî òåõ ïîð, ïîêà íå ïîëó÷èì
òîæäåñòâî 0 = 0 èëè ïðåéäåì ê ïðîòèâîðå÷èþ 1 = 0.  ïåðâîì ñëó÷àå èñ-
ñëåäóåìàÿ ôóíêöèÿ âûïîëíèìà, à âî âòîðîì — íåâûïîëíèìà. Â îáùåì
ñëó÷àå ìíîæåñòâî òàêèõ ôóíêöèé Fr , ñôîðìèðîâàííûõ íà îñíîâå îäíîãî
äèçúþíêòà, âûáðàííîãî â èñõîäíîé áóëåâîé ôóíêöèè F, ìîæíî ïðåäñòàâèòü
â âèäå äåðåâà.
Íà ðèñ. 1 ïðåäñòàâëåíî äåðåâî âñåõ Fr , êîòîðûå ïðèäåòñÿ ïîñòðîèòü
äëÿ ðåøåíèÿ çàäà÷è k-SAT ïðè k = 5. Äëÿ ïîñòðîåíèÿ ïðîöåäóðû ôîðìèðî-
âàíèÿ Fr ïî äåðåâó ââåäåì ñëåäóþùèå îáîçíà÷åíèÿ: S i r( ) — i-é äèçúþíêò
íà r-ì óðîâíå â äåðåâå; j r( ) — íîìåð ïåðåìåííîé â äèçúþíêòå S i r( ) íà r-ì
óðîâíå â äåðåâå; x j r( ) — ïåðåìåííàÿ â äèçúþíêòå S i r( ) ïîä íîìåðîì j r( ). Â
ñîîòâåòñòâèè ñ ïðàâèëàìè ïðåîáðàçîâàíèÿ áóëåâûõ ôóíêöèé Fr ñ ó÷åòîì
ââåäåííûõ îáîçíà÷åíèé ðàññìîòðèì ñëåäóþùóþ ïðîöåäóðó ðåøåíèÿ
óðàâíåíèÿ (6) ïðè âûïîëíåíèè óñëîâèé (5) äëÿ ðåøåíèÿ çàäà÷è k-SAT, ò.å.
çàäà÷è âûïîëíèìîñòè, â êàæäîì äèçúþíêòå êîòîðîé ñîäåðæèòñÿ ïî
k-ïåðåìåííûõ.
Ìåòîä ðåøåíèÿ k-SAT-çàäà÷è ñâåäåíèåì åå ê çàäà÷å î ïîêðûòèè
ISSN 0204–3572. Ýëåêòðîí. ìîäåëèðîâàíèå. 2015. Ò. 37. ¹ 5 21
Äèçúþíêò )(riS ñ ïÿòüþ ïåðåìåííûìè )(rjx
k
k k( 1)�
k k k( 1)( 2)� �
k k k k( 1) ( 2) ( 3)� � �
r = 0
r = 1
r = 2
r = 3
Äèçúþíêòû ñ ÷åòûðüìÿ ïåðåìåííûìè
Äèçúþíêòû ñ òðåìÿ ïåðåìåííûìè
Äèçúþíêòû ñ äâóìÿ ïåðåìåííûìè
×èñëî âåðøèí
äåðåâà íà óðîâíå-r
Ðèñ. 1. Äåðåâî ôîðìèðîâàíèÿ áóëåâûõ ôóíêöèé Fr
Ïðîöåäóðà À.
Ø à ã 1. Âûáèðàåì â (6) äèçúþíêò S i r( ) ñ ìèíèìàëüíûì ÷èñëîì
ïåðåìåííûõ è íàèáîëüøåé ñóììàðíîé âåñîâîé õàðàêòåðèñòèêîé pr ; âûáè-
ðàåì â íåì ïåðåìåííóþ x j r( ) ñ íàèáîëüøèì çíà÷åíèåì ÷àñòîòû h j (÷òî ñîîò-
âåòñòâóåò íóëåâîìó óðîâíþ r = 0) è ïåðåõîäèì ê ñëåäóþùåìó øàãó.
Ø à ã 2. Ïðèñâàèâàåì ïåðåìåííîé x j r( ) äèçúþíêòà S i r( ) íóëåâîå çíà-
÷åíèå è âûïîëíÿåì ïðåîáðàçîâàíèå áóëåâîé ôóíêöèè Fr â Fr�1, ïåðåõîäèì
ê ñëåäóþùåìó øàãó.
Ø à ã 3. Ïðîâåðÿåì ôóíêöèþ Fr�1 íà íåâûïîëíèìîñòü è ïðîâåðÿåì,
åñòü ëè â äèçúþíêòå Si r( ) ïåðåìåííûå, êîòîðûå íå áûëè ïðèðàâíåíû íóëþ,
ò.å. ïðîâåðÿåì, íå âûòåêàåò ëè èç ïðîöåññà ïðåîáðàçîâàíèÿ Fr â Fr�1
ïðîòèâîðå÷èå âèäà X Zi i� �0. Åñëè äà, òî ïåðåõîäèì ê øàãó 2, èíà÷å — ê
ñëåäóþùåìó øàãó.
Ø à ã 4. Ïðîâåðÿåì, âûïîëíèìà èëè íåò ôóíêöèÿ Fr�1 (ò.å. âûïîëíåíèå
òîæäåñòâà 0 = 0 â óðàâíåíèè (6)). Åñëè äà, òî àëãîðèòì çàêàí÷èâàåò ðàáîòó,
èíà÷å — ïåðåõîäèì ê ñëåäóþùåìó øàãó.
Ø à ã 5. Ïðîâåðÿåì ôóíêöèþ Fr�1 íà íåâûïîëíèìîñòü: âîçíèêàåò ïðî-
òèâîðå÷èå âèäà X Zi i� �0 ïðè ïîïûòêå îáðàùåíèÿ Fr�1 â íóëü. Åñëè
ôóíêöèÿ íå îáðàùåíà â íóëü è ïðè ýòîì ïðîòèâîðå÷èÿ íå âîçíèêàëè, òî
ïåðåõîäèì ê ñëåäóþùåìó øàãó, åñëè ïðîòèâîðå÷èå âîçíèêëî (ò.å. îíà
íåâûïîëíèìà), òî ïåðåõîäèì ê øàãó 7.
Ø à ã 6. Ïåðåõîäèì íà ñëåäóþùèé óðîâåíü. Äëÿ ýòîãî íàõîäèì äèçúþíêò
S i r( ) ñ ìèíèìàëüíûì ÷èñëîì ïåðåìåííûõ è íàèáîëüøåé ñóììàðíîé âå-
ñîâîé õàðàêòåðèñòèêîé pr , âûáèðàåì â íåì ïåðåìåííóþ x j r( ) ñ íàèáîëüøèì
çíà÷åíèåì ÷àñòîòû h j â áóëåâîé ôóíêöèè Fr è ïåðåõîäèì ê øàãó 2.
Ø à ã 7. Ïðîâåðÿåì, ïðîâåðåíû ëè íà íóëåâîì óðîâíå (r = 0) âñå ïå-
ðåìåííûå íà âîçìîæíîñòü îáíóëåíèÿ äèçúþíêòîâ â óðàâíåíèè (6). Åñëè
äà, òî àëãîðèòì çàêàí÷èâàåò ðàáîòó, òàê êàê ôóíêöèÿ íåâûïîëíèìà, èíà÷å —
ïåðåõîäèì ê ñëåäóþùåìó øàãó.
Ø à ã 8. Âîçâðàùàåìñÿ íà ïðåäûäóùèé (r – 1)-é óðîâåíü âåòâëåíèÿ è
ïåðåõîäèì ê øàãó 2.
Áëîê-ñõåìà äàííîãî àëãîðèòìà ïðåäñòàâëåíà íà ðèñ. 2. Ïîñëå âûáîðà
äèçúþíêòà Si r( ) â èñõîäíîé áóëåâîé ôóíêöèè F ïðîöåäóðà À àíàëèçèðóåò
íå âñþ èñõîäíóþ áóëåâó ôóíêöèþ F, à ëèøü òó ÷àñòü äèçúþíêòîâ, ñ
êîòîðûìè ïî ïåðåìåííûì ïåðåñåêàåòñÿ âûáðàííûé äèçúþíêò. Ïîñëåäîâà-
òåëüíîñòè äèçúþíêòîâ áóëåâîé ôóíêöèè, êîòîðûå íå ïåðåñåêàþòñÿ ïî
ïåðåìåííûì, âõîäÿùèì â äèçúþíêòû, îáðàçóþùèå ýòè ïîñëåäîâàòåëü-
íîñòè, áóäåì íàçûâàòü, íåçàâèñèìûìè ïîñëåäîâàòåëüíîñòÿìè äèçúþíê-
òîâ. ßñíî, ÷òî åñëè â áóëåâîé ôóíêöèè ÷èñëî ïåðåìåííûõ ðàâíî 2n, à
÷èñëî ïåðåìåííûõ â êàæäîì äèçúþíêòå ðàâíî k, òî ìàêñèìàëüíîå ÷èñëî
Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî
22 ISSN 0204–3572. Electronic Modeling. 2015. V. 37. ¹ 5
Ìåòîä ðåøåíèÿ k-SAT-çàäà÷è ñâåäåíèåì åå ê çàäà÷å î ïîêðûòèè
ISSN 0204–3572. Ýëåêòðîí. ìîäåëèðîâàíèå. 2015. Ò. 37. ¹ 5 23
Íà÷àëî
Êîíåö
Íåò
Íåò
Äà
Äà
Äà
Íåò
Íåò
Äà
6
Ïåðåõîäèì íà ñëåäóþùèé
(r +1)-é óðîâåíü âåòâëåíèÿ ðåøåíèé
8
Íàõîäèì äèçúþíêò ñ ìèíèìàëüSi r( ) íûì
÷èñëîì ïåðåìåííûõ ñ ìàêñèìàëüíîé
÷àñòîòîé âõîæäåíèÿ â Fr
9
r = 0
(ïðîâåðåíû
ïåðåìåííûå -íà íà÷àëü
íîì óðîâíå)
âñå
10
Âîçâðàùàåìñÿ íà ïðåäûäóùèé
(r �1)-é óðîâåíü âåòâëåíèÿ ðåøåíèé
11
Ôóíêöèÿ íåâûïîëíèìà12
Ôóíêöèÿ âûïîëíèìà
13
F Sr+ i1 è â
åùå åñòü íåïðîâåðåííûå
( )ríåâûïîëíèìà
âûïîëíèìà
íåâûïîëíèìà
ïåðåìåííûå
5
Âûïîëíÿåì ïðåîáðàçîâàíèÿ Fr,
ïîëó÷àåì Fr+1
4
3
Íàõîäèì äèçúþíêò ñ ìèíèìàëüSi r( )
÷àñòîòîé âõîæäåíèÿ â ôóíêöèþ
íûì
÷èñëîì ïåðåìåííûõ ñ ìàêñèìàëüíîé
2
Âõîäíûå äàííûå:
ÄÍÔ áóëåâîé ôóíêöèè F
1
7
Ïðèñâàèâàåì é ïåðåìåííîéxj r( )-
äèçúþíêòà íóëåâîå çíà÷åíèåSi r( )
Fr+1
Fr+1
Ðèñ. 2. Áëîê-ñõåìà ðåàëèçàöèè ïðîöåäóðû À
òàêèõ íåçàâèñèìûõ ïîñëåäîâàòåëüíîñòåé íå ìîæåò ïðåâûñèòü âåëè÷èíó
2n k/ , ò.å. â õóäøåì ñëó÷àå íà îñíîâå ïðåäëîæåííîé ïðîöåäóðû â èñõîäíîé
áóëåâîé ôóíêöèè ïðèäåòñÿ îáíóëÿòü íå áîëåå 2n k/ òàêèõ ïîñëåäîâàòåëü-
íîñòåé è, ñëåäîâàòåëüíî, àíàëèçèðîâàòü íå áîëåå 2n k/ äåðåâüåâ.
Îöåíèì ñëîæíîñòü àíàëèçà îäíîãî òàêîãî äåðåâà. Â ñîîòâåòñòâèè ñ
ïîñòðîåííûì äåðåâîì ÷èñëî ôóíêöèé Fr , êîòîðûå ïðèäåòñÿ ïðåîáðàçî-
âûâàòü, ðàâíî ñóììàðíîìó ÷èñëó âåðøèí íà âñåõ óðîâíÿõ àíàëèçèðóåìîãî
äåðåâà. Êàê ñëåäóåò èç ðèñ. 1, ÷èñëî âåðøèí íà íóëåâîì óðîâíå áóäåò ðàâ-
íî k, íà ïåðâîì óðîâíå — k (k � 1), íà òðåòüåì — k k k( ) ( )� �1 2 è òàê äàëåå.
Ñëåäîâàòåëüíî, ÷èñëî âåðøèí íà íóëåâîì óðîâíå ðàâíî k, íà âòîðîì — ÷èñëî
âåðøèí íå ïðåâûñèò k2, íà òðåòüåì — îíî íå ïðåâûñèò k 3 è íà ïîñëåä-
íåì — íå ïðåâûñèò k k �1.
Ðàññìîòðèì ñóììó k k k k k� � � � �2 3 1... . ßñíî, ÷òî îíà íå ìîæåò ïðåâû-
ñèòü âåëè÷èíó k k . Íàïðèìåð, äëÿ çàäà÷è «3-âûïîëíèìîñòü» â äåðåâå ïðè-
äåòñÿ ïðåîáðàçîâàòü â õóäøåì ñëó÷àå k k k k k k� � � � � � �( ) ( ) ( )1 1 2 15
� � � � � � �3 3 3 1 3 3 1 3 2 15( ) ( ) ( ) ôóíêöèé. Ó÷èòûâàÿ, ÷òî ïðè ðåøåíèè k-SAT-
çàäà÷è ïðèäåòñÿ àíàëèçèðîâàòü 2n k/ äåðåâüåâ, â õóäøåì ñëó÷àå ïðèäåòñÿ
ïðåîáðàçîâàòü 2 1k nk � ôóíêöèé Fr .  ñëó÷àå ðåøåíèÿ 3-SAT-çàäà÷è ýòî
÷èñëî íå ïðåâûñèò âåëè÷èíó
15 2
3
10
�
n
n.
Äëÿ àíàëèçà èñõîäíîãî óðàâíåíèÿ è ïðîèçâîëüíîé áóëåâîé ôóíêöèè
Fr â ñîîòâåòñòâèè ñ ïðåäëîæåííîé ïðîöåäóðîé À ïîòðåáóåòñÿ u ðàçëè÷íûõ
îïåðàöèé. ×èñëî u îïðåäåëÿåòñÿ 2mn îïåðàöèÿìè ñðàâíåíèÿ äëÿ îïðåäåëå-
íèÿ ÷àñòîò h j ïîÿâëåíèÿ êàæäîé ïåðåìåííîé â âûáðàííîì ñëàãàåìîì è
îñòàëüíûõ ñëàãàåìûõ ïëþñ mk îïåðàöèÿìè ñëîæåíèÿ äëÿ îïðåäåëåíèÿ
ñóììàðíîãî çíà÷åíèÿ âåñîâîé õàðàêòåðèñòèêè pi êàæäîãî ñëàãàåìîãî â
óðàâíåíèè (6) è ïëþñ m mlog2 îïåðàöèÿìè ñðàâíåíèÿ âûáîðà ìàêñèìàëü-
íîãî ýëåìåíòà â ìàññèâå èç m ýëåìåíòîâ, ò.å. u mn mk m m� � �2 2log . Â
õóäøåì ñëó÷àå íà êàæäîì øàãå ïðîöåäóðû À áóäåò îáíóëÿòñÿ òîëüêî îäíî
ñëàãàåìîå, ò.å. â óðàâíåíèè (6) ïîñëå ïåðâîãî øàãà îñòàíåòñÿ m – 1 ñëà-
ãàåìîå, äàëåå m – 2, m – 3, ..., 1 ñëàãàåìûõ, ò.å. îáíóëåíèå âñåõ ñëàãàåìûõ
ïðîöåäóðû À â õóäøåì ñëó÷àå ïîòðåáóåò âûïîëíåíèÿ
m m
u
( )�1
2
îïåðàöèé.
Òàêèì îáðàçîì, îáùåå ÷èñëî ýëåìåíòàðíûõ îïåðàöèé ïðè ðåøåíèè
k-SAT- çàäà÷è â õóäøåì ñëó÷àå íå ìîæåò ïðåâûñèòü âåëè÷èíó
O
k nm m
u O k mn m mn mk m
k
k2 1
2
1 2
1
1
2
�
���
�
��
�
�
�� � � � �
( )
( ( ) ( log m)) �
Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî
24 ISSN 0204–3572. Electronic Modeling. 2015. V. 37. ¹ 5
� �
��
�
�
�
�
�
�
�
�
�
�
�
�O m n k
k m
n
k2 1
2
3 2 1 2log
. (7)
Ïðè ðåøåíèè 3-SAT-çàäà÷è ÷èñëî ýëåìåíòàðíûõ îïåðàöèé â õóäøåì
ñëó÷àå íå ìîæåò ïðåâûñèòü âåëè÷èíó
O m m n
m
n
O m n10 1 1
3
2
10 1
32 2 2 3 2( )
log log
� �
��
�
�
�
�
�
�
�
�
�
�
� � �
� 2
2
m
n
�
�
�
�
�
�
�
�
�
�
�
� . (8)
Èçâåñòíî, ÷òî k-SAT-çàäà÷à ìîæåò áûòü ñâåäåíà ê 3-SAT-çàäà÷å çà
ïîëèíîìèàëüíîå âðåìÿ.  ÷àñòíîñòè, åñëè äèçúþíêò S i ñîäåðæèò áîëåå
òðåõ ëèòåðàëîâ, íàïðèìåð S i k� � � �( ... )� � �1 2 , k �3, òî ìîæíî çàìåíèòü
S i íà k – 2 äèçúþíêòîâ [3] :
S x x x x x xi k k� � � � � � �
� �� �( ) ( ) ( ) ... (� � � � � �1 2 1 1 3 2 2 4 3 3 1 k ), (9)
ãäå x xk1 3,..., � — íîâûå ïåðåìåííûå. Íàáîð ýòèõ íîâûõ äèçúþíêòîâ âû-
ïîëíèì òîãäà è òîëüêî òîãäà, êîãäà âûïîëíèì äèçúþíêò S i . Òàêèì
îáðàçîì, ïðè ïåðåõîäå îò k-SAT-çàäà÷è ê çàäà÷å 3-SAT êàæäûé äèçúþíêò
k-SAT-çàäà÷è óâåëè÷èâàåò ÷èñëî ïåðåìåííûõ â áóëåâîé ôóíêöèè íà (k – 3), à
÷èñëî äèçúþíêòîâ — íà k – 2 äèçúþíêòà. Ñëåäîâàòåëüíî, ïîñëå ñâåäåíèÿ
÷èñëî ïåðåìåííûõ è ÷èñëî äèçúþíêòîâ â íîâîé çàäà÷å áóäóò ñîîòâåòñò-
âåííî � � � �n n m k( ( ))3 è � � �m k m( )2 . Ïîäñòàâëÿÿ â (8) �n è �m â êà÷åñòâå
íîâûõ çíà÷åíèé n è m, ïîëó÷àåì îöåíêó ñëîæíîñòè ðåøåíèÿ k-SAT-çàäà÷è
ñ ïîìîùüþ ïðîöåäóðû À:
O k m n m k
k m
n m k
10 2 3 1
3 2
2 3
3 3 2 2 2( ) ( ( ))
log ( ) log
( (
� � � �
� � �
� � ))
�
�
�
�
�
�
�
�
�
�
�
� . (10)
Ïðåäëîæåííàÿ ïðîöåäóðà À ðåøåíèÿ k-SAT-çàäà÷è ïðåäñòàâëÿåò ñî-
áîé ôîðìàëüíî ïîëèíîìèàëüíûé àëãîðèòì, íî ñ âûñîêîé ñòåïåíüþ ïîëè-
íîìà (7), è, ñëåäîâàòåëüíî, ðåàëèçóåòñÿ çà ýêñïîíåíöèàëüíîå âðåìÿ, ïðè
ýòîì ðåøåíèå 3-SAT-çàäà÷è ïðîöåäóðà À îñóùåñòâëÿåò çà ïîëèíîìèàëü-
íîå âðåìÿ. Ñëåäîâàòåëüíî, ïðåîáðàçîâàíèå k-SAT-çàäà÷è çà ïîëèíîìèàëü-
íîå âðåìÿ â 3-SAT-çàäà÷ó ïðèâîäèò ê àëãîðèòìó ïîëèíîìèàëüíîé ñëîæ-
íîñòè. Ïðè ðåøåíèè k-SAT-çàäà÷è ñ ïîìîùüþ ïðîöåäóðû À áåç ñâåäåíèÿ
åå ê 3-SAT-çàäà÷å àëãîðèòì ïðåîáðàçîâàíèÿ èìååò ýêñïîíåíöèàëüíóþ
ñëîæíîñòü. Ïðè ýòîì âûáîð íà êàæäîì øàãå ïðîöåäóðû À äèçúþíêòà S i r( )
ñ ìèíèìàëüíûì ÷èñëîì ïåðåìåííûõ è íàèáîëüøåé ñóììàðíîé âåñîâîé
õàðàêòåðèñòèêîé pr ïîçâîëÿþò ñóùåñòâåííî ñîêðàòèòü ñðåäíåå âðåìÿ ðåà-
ëèçàöèè àëãîðèòìà ïîñðåäñòâîì îáíóëåíèÿ ìàêñèìàëüíî âîçìîæíîãî ÷èñ-
ëà ñëàãàåìûõ íà êàæäîì øàãå ïðîöåäóðû.
Òàêèì îáðàçîì, ïðîöåäóðà À ïðåäñòàâëÿåò ñîáîé ïîëíûé ïåðåáîð
âàðèàíòîâ âîçìîæíîãî îáíóëåíèÿ äèçúþíêòîâ.  ñëó÷àå âûïîëíèìîñòè
Ìåòîä ðåøåíèÿ k-SAT-çàäà÷è ñâåäåíèåì åå ê çàäà÷å î ïîêðûòèè
ISSN 0204–3572. Ýëåêòðîí. ìîäåëèðîâàíèå. 2015. Ò. 37. ¹ 5 25
ôóíêöèè îáíóëåíèå ïðîèñõîäèò çà ïîëèíîìèàëüíîå âðåìÿ, à â ñëó÷àå åå
íåâûïîëíèìîñòè ïîñëå ïåðâîé ïîïûòêè îáíóëåíèÿ ëèáî ïåðâîãî ëèáî
m-ãî äèçúþíêòà âûÿñíÿåòñÿ íåâîçìîæíîñòü åãî îáíóëåíèÿ è â äåðåâå
ïðîèñõîäèò áûñòðûé îòáîð ôóíêöèé, êîòîðûå íåîáõîäèìî àíàëèçèðîâàòü.
 ñâÿçè ñ ýòèì ïðîöåäóðà À ïîçâîëÿåò ðåøèòü k-SAT-çàäà÷ó â ñðåäíåì çà
ïîëèíîìèàëüíîå âðåìÿ.  ñëó÷àå ïðåîáðàçîâàíèÿ k-SAT-çàäà÷è â 3-SAT-
çàäà÷ó îíà ðåøàåòñÿ ñ ïîìîùüþ ïðîöåäóðû À çà ïîëèíîìèàëüíîå âðåìÿ,
îïðåäåëÿåìîå ñîîòíîøåíèåì (10).
Ðàññìîòðèì ïðèìåðû ðàáîòû ïðîöåäóðû À ïðè îïðåäåëåíèè âûïîë-
íèìîñòè áóëåâûõ ôóíêöèé. Ïóñòü òðåáóåòñÿ îïðåäåëèòü âûïîëíèìîñòü
ñëåäóþùåé áóëåâîé ôóíêöèè ñ ÷åòûðüìÿ ïåðåìåííûìè è òðèíàäöàòüþ
äèçúþíêòàìè:
F x x x x x x x x x x x x( ) ( ) ( ) ( ) (� � � � � � � � �� � � � � � � �
1 0 3 1 0 2 0 3 2 3 2 x
1
)�
� � � � � � � � �� � � � � �( ) ( ) ( ) ( ) (x x x x x x x x x x x x x1 0 3 1 0 2 3 0 2 1 2 0 0 � � �x x
3 2
)
� � � � � � � � �� � � � � �( ) ( ) ( ) ( )x x x x x x x x x x x x2 1 0 0 3 1 3 1 2 0 2 3
, (11)
ãäå ïîëàãàåì, ÷òî çíàê ïëþñ — ýòî çíàê ëîãè÷åñêîãî ñëîæåíèÿ. Çàïèøåì
èñõîäíîå óðàâíåíèå :
Fr�0 = Z1Z0Z3 + x1x0x2 + Z0Z3Z2 + Z3Z2x1 + x1x0x3 + Z1Z0x2+ Z3x0x2 +
+ Z1Z2x0 + Z0x3x2 + Z2x1x0 + Z0Z3x1 + Z3x1x2 + Z0Z2x3 = 0. (12)
Îïðåäåëÿåì ÷àñòîòû h j ïîÿâëåíèÿ ïåðåìåííûõ â êàæäîì ñëàãàåìîì:
Âûáèðàåì äèçúþíêò Z0Z3x1 ñ ìàêñèìàëüíûì çíà÷åíèåì ñóììû ÷àñòîò h j
6 + 6 + 5 = 17, ïîëàãàåì Z0 = 0, x0 = 1 è îñóùåñòâëÿåì ïðåîáðàçîâàíèå Fr�0 â
Fr�1. Â ðåçóëüòàòå èñõîäíîå óðàâíåíèå (12) ïðèíèìàåò âèä
x1x2 + Z3Z2x1 + x1x3 + Z3x2 + Z1Z2 + Z2x1 + Z3x1x2 = 0. (13)
Ïðîâîäèì îïåðàöèþ ïîãëîùåíèÿ: çäåñü x1x2 ïîãëîùàåò ñëàãàåìîå Z3x1x2, à
ñëàãàåìûå Z2x1 è Z3x2 ïîãëîùàþò ñîîòâåòñòâåííî ñëàãàåìûå Z3Z2x1 è Z3x1x2.
Ïîñëå ýòîãî óðàâíåíèå (13) áóäåò èìåòü âèä
Fr�1 = x1x2 + x1x3 + Z3x2 + Z1Z2 + Z2x1 = 0 . (14)
Ïðîâåðÿåì, îáðàùåíà ëè â íóëü ôóíêöèÿ Fr�1 , ò.å. âûïîëíèìà èëè íåò. Â
äàííîì ñëó÷àå ôóíêöèÿ Fr�1 íå îáðàùåíà â íóëü è â ïðîöåññå ïðåîáðà-
Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî
26 ISSN 0204–3572. Electronic Modeling. 2015. V. 37. ¹ 5
x j r( ) x0 x1 x2 x3 Z0 Z1 Z2 Z3
h j 5 5 5 3 6 3 5 6
.
çîâàíèÿ ôóíêöèè Fr�0 â Fr�1 ïðîòèâîðå÷èÿ íå âîçíèêëî. Ñëåäîâàòåëüíî,
ïåðåõîäèì íà ñëåäóþùèé r + 1 óðîâåíü. Ñíîâà îïðåäåëÿåì ÷àñòîòû h j ïîÿâ-
ëåíèÿ ïåðåìåííûõ â êàæäîì ñëàãàåìîì:
(15)
Äàëåå, ñðåäè äèçúþíêòîâ, ñîäåðæàùèõ ìèíèìàëüíîå ÷èñëî ïåðåìåí-
íûõ, à òàêèìè ÿâëÿþòñÿ äèçúþíêòû x1x2, x1x3, Z3x2, Z1Z2, Z2x1, âûáèðàåì
äèçúþíêò ñ íàèáîëüøèì çíà÷åíèåì âåñîâîé õàðàêòåðèñòèêè ðj. Ñîãëàñíî
(15) âåñîâûå õàðàêòåðèñòèêè ýòèõ ñëàãàåìûõ ðàâíû ñîîòâåòñòâåííî 4, 4, 2,
3, 5, ïîýòîìó âûáèðàåì äèçúþíêò Z2 x1. Â íåì ïåðåìåííîé ñ íàèáîëüøåé
÷àñòîòîé, ðàâíîé òðåì, ÿâëÿåòñÿ ïåðåìåííàÿ x1, ïîýòîìó ïîëàãàåì x1 = 0,
Z1 = 1. Òîãäà óðàâíåíèå (14) ïðèíèìàåò âèä
Fr�2 = Z3x2 + Z2 = 0. (16)
 (16) íåëüçÿ ñäåëàòü ïîãëîùåíèé, íî â íåì ïîÿâèëîñü ñëàãàåìîå ñ
îäíîé ïåðåìåííîé, ïîýòîìó ïîëàãàåì Z2 = 0, x2 = 1 è, ñëåäîâàòåëüíî, çàïè-
ñûâàåì (16) â âèäå Z3 = 0. Òàêèì îáðàçîì, íàáîð èç ïåðåìåííûõ Z0 = 0, x1= 0,
Z2 = 0, Z3 = 0 èëè x0
�x
1
x2
�x3
� îáðàùàåò óðàâíåíèå (12) â òîæäåñòâî è, ñëå-
äîâàòåëüíî, ÿâëÿåòñÿ âûïîëíÿþùèì íàáîðîì ïåðåìåííûõ äëÿ áóëåâîé
ôóíêöèè (11).
Ðàññìîòðèì ïðîöåññ ðàáîòû ïðîöåäóðû À â ñëó÷àå, êîãäà áóëåâà ôóíê-
öèÿ íåâûïîëíèìà. Ïóñòü çàäàíà ôóíêöèÿ
F x x x x x x x x x x x x x( ) ( ) ( ) ( ) (� � � � � � � � �� � � � � �
0 1 2 3 0 2 0 3 2 1 2 0 )�
� � � � � � � � �� � � � � �( ) ( ) ( ) ( ) (x x x x x x x x x x x x x0 1 2 3 1 0 3 0 2 0 2 1 3
� � �x x
0 2
)
� � � � � � � � �� � � � � � �( ) ( ) ( ) ( )x x x x x x x x x x x x
3 0 1 3 2 0 2 3 1 1 2 3 . (17)
Çàïèñûâàåì èñõîäíîå óðàâíåíèå:
Fr�1 = x0x1Z2 + Z3Z0x2 + x0Z3x2 + x1Z2Z0 + Z0Z1x2 + x3x1Z0 + x3x0Z2 +
+ x0Z2Z1 + x3x0x2 + x3x0x1 + x3Z2Z0 + Z2Z3Z1 + x1Z2Z3 = 0. (18)
Îïðåäåëÿåì ÷àñòîòó h j ïîÿâëåíèÿ ïåðåìåííûõ â êàæäîì ñëàãàåìîì (18):
Ìåòîä ðåøåíèÿ k-SAT-çàäà÷è ñâåäåíèåì åå ê çàäà÷å î ïîêðûòèè
ISSN 0204–3572. Ýëåêòðîí. ìîäåëèðîâàíèå. 2015. Ò. 37. ¹ 5 27
x j r( ) x1 x2 x3 Z1 Z2 Z3
h j 3 1 1 1 2 1
.
x j r( ) x0 x1 x2 x3 Z0 Z1 Z2 Z3
h j 6 5 4 4 5 3 6 4
.
Âûáèðàåì äèçúþíêò x0x1Z2 ñ ìàêñèìàëüíûì çíà÷åíèåì ñóììû ÷àñòîò h j
6 + 5 + 6 = 17. Âûáèðàåì â íåì ïåðåìåííóþ x0 ñ ìàêñèìàëüíûì çíà÷åíèåì
h j è ïîëàãàåì x0 = 0, Z0 = 1. Òîãäà èñõîäíîå óðàâíåíèå (18) çàïèñûâàåì â
âèäå
Z3x2 + x1Z2 + Z1x2 + x3x1 + x3Z2 + Z2Z3Z1 + x1Z2Z3 = 0. (19)
 (19) ñëàãàåìîå x1Z2 ïîãëîùàåò ñëàãàåìîå x1Z2Z3 è óðàâíåíèå (19) ïðè-
íèìàåò âèä
Fr�1 = Z3x2 + x1Z2 + Z1x2 + x3x1 + x3Z2 + Z2Z3Z1 = 0. (20)
Ïîñêîëüêó ôóíêöèÿ Fr�1 íå îáðàùàåòñÿ â íóëü è ïðè ýòîì ïðîòèâîðå÷èÿ íå
âîçíèêàåò, îïðåäåëÿåì ÷àñòîòy h j ïîÿâëåíèÿ ïåðåìåííûõ â êàæäîì
äèçúþíêòå (20):
 (20) äèçúþíêòàìè ñ ìàêñèìàëüíûì ñóììàðíûì âåñîì, ðàâíûì ïÿòè,
ÿâëÿþòñÿ äèçúþíêòû x1Z2 è x3Z2. Ïîýòîìó äëÿ äàëüíåéøåãî àíàëèçà
âûáèðàåì, íàïðèìåð, äèçúþíêò S1 = x1Z2 è â íåì âûáèðàåì ïåðåìåííóþ Z2
ñ ìàêñèìàëüíîé ÷àñòîòîé ïîÿâëåíèÿ â äèçúþíêòàõ ôóíêöèè (20), ðàâíîé
òðåì. Äàëåå, ïîëàãàÿ Z2 = 0, x2 = 1, ïðåîáðàçóåì (20) ê âèäó
Fr�2 = Z3 + Z1 + x3x1 = 0 . (21)
Ïîñêîëüêó â (21) ïîãëîùåíèé ñäåëàòü íåëüçÿ è ïîÿâèëèñü ñëàãàåìûå,
ñîäåðæàùèå ïî îäíîé ïåðåìåííîé, ïîëàãàåì Z3 = 0, x3 = 1 è Z1 = 0, x1 = 1, â
ðåçóëüòàòå ÷åãî ïîëó÷àåì 1 = 0, ò.å. âîçíèêàåò ïðîòèâîðå÷èå. Ïîýòîìó âîçâ-
ðàùàåìñÿ íà ïðåäûäóùèé óðîâåíü Fr�1 è ïåðåõîäèì ê ïîïûòêå îáíóëåíèÿ
äèçúþíêòà x1Z2 íà îñíîâå ïåðåìåííîé x1. Äëÿ ýòîãî â (21) ïîëàãàåì x1 = 0,
Z1 = 1 è ïîëó÷àåì
Fr�2 = Z3x2 + x2 + x3Z2 + Z2Z3 = 0. (22)
 (22) x2 ïîãëîùàåò ñëàãàåìîå Z3x2. Òîãäà ïîëó÷àåì ñëåäóþùåå óðàâíåíèå:
Fr�3 = x2 + x1Z2 + Z2Z1 + x1Z2 = 0. (23)
Ïîñêîëüêó â (23) ïîÿâèëèñü ñëàãàåìûå, ñîäåðæàùèå ïî îäíîé ïåðå-
ìåííîé, ïîëàãàåì x2 = 0, Z2 = 1 è ïîëó÷àåì x1 + Z1 = 0, ò.å. âîçíèêëî ïðî-
òèâîðå÷èå. Ñëåäîâàòåëüíî, îáíóëèòü äèçúþíêò S1 = x1Z2, èñïîëüçóÿ ïåðå-
Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî
28 ISSN 0204–3572. Electronic Modeling. 2015. V. 37. ¹ 5
x j r( ) x1 x2 x3 Z1 Z2 Z3
h j 2 2 2 2 3 2
.
ìåííûå x1 è Z2, áåç âîçíèêíîâåíèÿ ïðîòèâîðå÷èÿ íåâîçìîæíî. Ïîýòîìó
âîçâðàùàåìñÿ íà íóëåâîé óðîâåíü è ïðîâåðÿåì, âñå ëè ïåðåìåííûå
ïðîâåðåíû íà âîçìîæíîñòü îáíóëåíèÿ äèçúþíêòà x0x1Z2.  äàííîì ñëó÷àå
íåïðîâåðåííûìè îñòàëèñü ïåðåìåííûå x1 è Z2. Ïðè ýòîì ïåðåìåííàÿ Z2
èìååò áîëüøóþ ÷àñòîòó ïîÿâëåíèÿ â äèçúþíêòàõ, ÷åì x1. Ïîýòîìó, ïîëàãàÿ
Z2 = 0, x2 = 1, ïðèâîäèì óðàâíåíèå (18) ê âèäó
Fr�1 = Z3Z0 + x0Z3 + Z0Z1 + x3x1Z0 + x3x0 + x3x0x1 = 0 . (24)
 (24) ñëàãàåìîå x3x0 ïîãëîùàåò ñëàãàåìîå x3x0x1. Òîãäà ïîëó÷àåì
Fr�2 = Z3Z0 + x0Z3 + Z0Z1 + x3x1Z0 + x3x0 = 0. (25)
Ôóíêöèÿ Fr�2 íå îáðàùàåòñÿ â íóëü, è ïðè ýòîì ïðîòèâîðå÷èÿ íå
âîçíèêàåò. Ïîýòîìó îïðåäåëÿåì ÷àñòîòy h j ïîÿâëåíèÿ ïåðåìåííûõ â êàæ-
äîì äèçúþíêòå (25):
Ñðåäè äèçúþíêòîâ ñ äâóìÿ ïåðåìåííûìè âûáèðàåì äèçúþíêò ñ ìàêñè-
ìàëüíîé ñóììàðíîé ÷àñòîòîé. Òàêèì ÿâëÿåòñÿ ñëàãàåìîå Z3Z0 ñ âåñîâîé
õàðàêòåðèñòèêîé, ðàâíîé ïÿòè. Âûáèðàåì â íåì ïåðåìåííóþ Z0 ñ íàè-
áîëüøèì âåñîì, ðàâíûì ÷åòûðåì, è ïîëàãàåì x0 = 1 è Z0 = 0. Òîãäà (25)
ïðèíèìàåò âèä Z3 + x3 = 0, ò.å. âîçíèêëî ïðîòèâîðå÷èå. Ïîýòîìó âîçâðà-
ùàåìñÿ íà ïðåäûäóùèé óðîâåíü äëÿ îáíóëåíèÿ äèçúþíêòà Z3Z0 íà îñíîâå
ïåðåìåííîé Z3. Äëÿ ýòîãî â (25) ïîëàãàåì x3 = 1, Z3 = 0 è ïîëó÷àåì
Fr�1 =Z0Z1 + x1Z0 + x0 = 0. (26)
 (26) âîçíèêëî ñëàãàåìîå, ñîñòîÿùåå èç îäíîé ïåðåìåííîé. Ïîýòîìó
ïîëàãàåì x0 = 0, Z0 = 1 è ïîëó÷àåì Z1 + x1 = 0, ò.å. âîçíèêëî ïðîòèâîðå÷èå.
Äàëåå, ïðîâåðÿåì, âñå ëè ïåðåìåííûå x j r( ) íà íóëåâîì óðîâíå áûëè èñ-
ïîëüçîâàíû äëÿ îáíóëåíèÿ äèçúþíêòà x0x1Z2 .  äàííîì ñëó÷àå îñòàëàñü
íåïðîâåðåííîé òîëüêî îäíà ïåðåìåííàÿ x1, ïîýòîìó ïîëàãàåì x1 = 0, Z1 = 1.
Òîãäà óðàâíåíèå (18) ïðèíèìàåò âèä
Fr�1 = Z3Z0x2 + x0Z3x2 + Z0x2 + x3x0Z2 + x0Z2 + x3x0x2 + x3Z2Z0 + Z2Z3 = 0.
Ïîñëå ïîãëîùåíèÿ ñëàãàåìûì x0Z2 ñëàãàåìûõ Z3Z0x2 è x3x0Z2 ïîëó÷àåì
Fr�1 = x0Z3x2 + Z0x2 + x0Z2 + x3x0x2 + x3Z2Z0 + Z2Z3 = 0. (27)
Ìåòîä ðåøåíèÿ k-SAT-çàäà÷è ñâåäåíèåì åå ê çàäà÷å î ïîêðûòèè
ISSN 0204–3572. Ýëåêòðîí. ìîäåëèðîâàíèå. 2015. Ò. 37. ¹ 5 29
x j r( ) x0 x1 x3 Z0 Z1 Z3
h j 2 1 2 3 1 2
.
Ôóíêöèÿ Fr�1 íå îáðàùàåòñÿ â íóëü, è ïðè ýòîì ïðîòèâîðå÷èÿ íå âîç-
íèêàåò. Ïîýòîìó îïðåäåëÿåì ÷àñòîòy h j ïîÿâëåíèÿ ïåðåìåííûõ â êàæäîì
äèçúþíêòå (27):
Ñðåäè äèçúþíêòîâ ñ äâóìÿ ïåðåìåííûìè â (27) âûáèðàåì äèçúþíêò ñ
ìàêñèìàëüíîé ñóììàðíîé ÷àñòîòîé. Òàêèì ÿâëÿåòñÿ ñëàãàåìîå x0Z2 ñ âåñî-
âîé õàðàêòåðèñòèêîé, ðàâíîé øåñòè. Âûáèðàåì â íåì ïåðåìåííóþ x0 ñ ÷àñ-
òîòîé ïîÿâëåíèÿ â äðóãèõ äèçúþíêòàõ (27), ðàâíîé òðåì, è ïîëàãàåì x0 = 0
è Z0 = 1. Òîãäà (27) ïðèíèìàåò âèä
Z3x2 + x2 + x3Z2 + Z2Z3 = 0. (28)
 (28) x2 ïîãëîùàåò Z3x2 , ïîýòîìó ïîëó÷àåì
Fr�2 = x2 + x3Z2 + Z2Z3 = 0. (29)
 (29) ïîÿâèëîñü ñëàãàåìîå ñ îäíîé ïåðåìåííîé x2 . Ïîýòîìó ïîëàãàåì
x2 = 0, Z2 = 1 è ïîëó÷àåì x3 + Z3 = 0, ò.å. âîçíèêëî ïðîòèâîðå÷èå. Ïîýòîìó
âîçâðàùàåìñÿ íà óðîâåíü r – 1, ò.å. ïåðåõîäèì ê ôóíêöèè (27) è ïðåäïðè-
íèìàåì ïîïûòêó îáíóëåíèÿ äèçúþíêòà x0Z2 íà îñíîâå ïåðåìåííîé Z2. Äëÿ
ýòîãî, ïîëàãàÿ â (27) Z2 = 0, x2 = 1, ïîëó÷àåì Z3Z0 + x0Z3 + Z0 + x3x0 = 0. Ïðî-
âåäÿ ïîãëîùåíèå, ïîëó÷àåì x0Z3 + Z0 + x3x0 = 0, ãäå ïîÿâèëîñü ñëàãàåìîå ñ
îäíîé ïåðåìåííîé Z0. Ïîýòîìó ïîëàãàåì Z0 = 0, x0 = 1 è ïîëó÷àåì Z3 + x3 = 0,
ò.å. îáðàçîâàëîñü ïðîòèâîðå÷èå. Ïîýòîìó âîçâðàùàåìñÿ íà r – 1 óðîâåíü (â
äàííîì ñëó÷àå íóëåâîé) è ïðîâåðÿåì, âñå ëè ïåðåìåííûå èñïîëüçîâàíû
äëÿ îáíóëåíèÿ äèçúþíêòà x0x1Z2.  äàííîì ñëó÷àå ýòî — ïîñëåäíÿÿ ïå-
ðåìåííàÿ. Ñëåäîâàòåëüíî, ïðîöåäóðà çàêàí÷èâàåò ðàáîòó, òàê êàê ïðè ðà-
âåíñòâå íóëþ ïåðåìåííûõ â äèçúþíêòå x0x1Z2 îáðàòèòü óðàâíåíèå (18) â
òîæäåñòâî íåâîçìîæíî, çíà÷èò ôóíêöèÿ (17) íåâûïîëíèìà.
Ñëåäóåò çàìåòèòü, ÷òî â íàèõóäøåì ñëó÷àå îöåíêà ñâåðõó âðåìåííîé
ñëîæíîñòè ïðîöåäóðû À ÿâëÿåòñÿ äîñòàòî÷íî ãðóáîé, òàê êàê ïðåäïî-
ëàãàëîñü, ÷òî ïðè ïðèñâîåíèè X j � 0 è Z j �1 íà êàæäîì øàãå îáíóëÿåòñÿ
òîëüêî îäíî ñëàãàåìîå, õîòÿ íà ñàìîì äåëå îáíóëÿåòñÿ h j ñëàãàåìûõ.
Ïîýòîìó ïðåäñòàâëÿåò èíòåðåñ ïîëó÷èòü ñðåäíþþ âåëè÷èíó îöåíêè âðå-
ìåííîé ñëîæíîñòè ïðîöåäóðû À.
Ïðè ïðîâåäåíèè ýêñïåðèìåíòà 2n ïåðåìåííûõ X j �1 è Z j ðàçìåùà-
ëèñü ïî äèçúþíêòàì ïî ðàâíîìåðíîìó çàêîíó ðàñïðåäåëåíèÿ. Ðåçóëüòàòû
ýêñïåðèìåíòàëüíûõ èññëåäîâàíèé ïîëó÷åíû ñ äîâåðèòåëüíîé âåðîÿò-
Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî
30 ISSN 0204–3572. Electronic Modeling. 2015. V. 37. ¹ 5
x j r( ) x0 x2 x3 Z0 Z2 Z3
h j 3 2 2 2 3 2
.
íîñòüþ 0,95. Äëÿ ïîëó÷åíèÿ ñðåäíåãî çíà÷åíèÿ ÷èñëà ýëåìåíòàðíûõ îïåðà-
öèé (ÝÎ), âûïîëíÿåìûõ ïðîöåäóðîé À, íà êàæäóþ òî÷êó ãåíåðèðîâàëîñü îò
50 äî 70 áóëåâûõ ôóíêöèé èññëåäóåìîé ðàçìåðíîñòè. ×èñëî äèçúþíêòîâ m
ìåíÿëîñü îò 100 äî 10000, à ÷èñëî ïåðåìåííûõ n — îò 90 äî 2400. Ðåçóëüòàòû
ýêñïåðèìåíòàëüíûõ èññëåäîâàíèé ïðèâåäåíû â òàáë. 1—3.
Èç òàáë. 1—3 âèäíî, ÷òî íàèáîëüøåå ÷èñëî îïåðàöèé ïðîöåäóðà âû-
ïîëíÿåò ïðè çíà÷åíèÿõ � � n m/ , áëèçêèõ ê 0,24. Ïðè ðàâíîìåðíîì çàêîíå
ðàñïðåäåëåíèÿ ïåðåìåííûõ X i è X i ïî äèçúþíêòàì ïðè � < 0,24 áóëåâû
ôóíêöèè, êàê ïðàâèëî, ÿâëÿþòñÿ íåâûïîëíèìûìè, à ïðè � > 0,24 —
Ìåòîä ðåøåíèÿ k-SAT-çàäà÷è ñâåäåíèåì åå ê çàäà÷å î ïîêðûòèè
ISSN 0204–3572. Ýëåêòðîí. ìîäåëèðîâàíèå. 2015. Ò. 37. ¹ 5 31
n ×èñëî ÝÎ � = n/m Âûïîëíèìîñòü
áóëåâîé ôóíêöèè
Âðåìÿ ðåøåíèÿ, ìñ
ìèíèìàëüíîå ìàêñèìàëüíîå
m = 500; k = 3
100 1,06
108 0,2 – 5,06 793 934
110 7,2
108 0,22 – 5,06 793 934
120 8,6
109 0,24 – 5,06 793 934
130 4,2
108 0,26 + 5,06 793 934
140 63 209 0,28 + 5,06 793 934
150 52 096 0,3 + 5,06 793 934
400 286 987 1,25 – 36,5 849
800 106 0,625 – 36,5 849
1200 2,24
106 0,416 – 36,5 849
1600 4
106 0,313 + 36,5 849
2000 6,2
106 0,25 + 36,5 849
2400 8,9
106 0,208 + 36,5 849
m =10000; k = 3
100 324 459 0,2 – 44 819 261
200 1,25
106 0,22 – 44 819 261
300 4,89
106 0,24 – 44 819 261
400 9,5
107 0,26 + 44 819 261
500 2,36
109 0,28 + 44 819 261
5000 6,1
107 0,3 + 44 819 261
Ïðèìå÷àíèå: çíàê ìèíóñ îçíà÷àåò íåâûïîëíèìîñòü áóëåâîé ôóíêöèè, à çíàê ïëþñ — åå
âûïîëíèìîñòü.
Òàáëèöà 1
âûïîëíèìûìè. Ïðè çíà÷åíèè �, áëèçêîì ê 0,24, âåðîÿòíîñòü ïîÿâëåíèÿ
âûïîëíèìûõ è íåâûïîëíèìûõ áóëåâûõ ôóíêöèé ñòàíîâèòñÿ îäèíàêîâîé è
âîçðàñòàåò ÷èñëî îïåðàöèé, âûïîëíÿåìûõ ïðîöåäóðîé À. Ñ óâåëè÷åíèåì
çíà÷åíèÿ k (ñì. òàáë. 2), êîãäà ñëàãàåìîå
k m
n
� log2
2
â (10) çíà÷èòåëüíî ìåíü-
øå åäèíèöû, íàáëþäàåòñÿ óìåíüøåíèå âðåìåííîé ñëîæíîñòè ðàáîòû
ïðîöåäóðû, ÷òî îáóñëîâëåíî âîçðàñòàíèåì ÷èñëà îáíóëÿåìûõ ñëàãàåìûõ
íà êàæäîì øàãå åå ðàáîòû. Îäíàêî, êîãäà óêàçàííîå â (10) ñëàãàåìîå
ñòàíîâèòñÿ ñóùåñòâåííî áîëüøå åäèíèöû, íàáëþäàåòñÿ äàëüíåéøåå âîç-
ðàñòàíèå ÷èñëà ýëåìåíòàðíûõ îïåðàöèé, âûïîëíÿåìûõ ïðîöåäóðîé À.
Äëÿ òåñòèðîâàíèÿ ðàçðàáîòàííîãî àëãîðèòìà èñïîëüçîâàíî 900 òåñòîâ
ñïåöèàëèçèðîâàííîé áèáëèîòåêè SAT Live [4], êàæäûé èç êîòîðûõ ñîäåð-
Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî
32 ISSN 0204–3572. Electronic Modeling. 2015. V. 37. ¹ 5
m ×èñëî ÝÎ � = n/m Âûïîëíèìîñòü
áóëåâîé ôóíêöèè
Âðåìÿ ðåøåíèÿ, ìñ
ìèíèìàëüíîå ìàêñèìàëüíîå
n =90; k = 3
100 16 029 0,9 + 2,15 38 910
200 26 994 0,4 + 2,15 38 910
300 37 413 0,3 + 2,15 38 910
400 4,39
107 0,23 + 2,15 38 910
500 2,42
107 0,18 – 2,15 38 910
600 1,86
107 0,15 – 2,15 38 910
Òàáëèöà 2
k ×èñëî ÝÎ
Âûïîëíèìîñòü
áóëåâîé ôóíêöèè
Âðåìÿ ðåøåíèÿ, ìñ
ìèíèìàëüíîå ìàêñèìàëüíîå
m =500; n =90; � = 18
3 2,42
107 � 7,57 160
10 60 807 + 7,57 160
20 48 555 + 7,57 160
30 55 488 + 7,57 160
40 64 268 + 7,57 160
50 74 508 + 7,57 160
Òàáëèöà 3
æèò 403 äèçúþíêòà è 100 ïåðåìåííûõ ñ ïàðàìåòðîì � = 0,248. Òåñòû
ñôîðìèðîâàíû ïîñðåäñòâîì ïñåâäî-ñëó÷àéíîãî çàïîëíåíèÿ äèçúþíêòîâ.
Òåñòèðîâàíèå îñóùåñòâëÿëîñü íà êîìïüþòåðå ASER c Intel Pentium pro-
cessor T4400, 2,2 Ghz, 3 GB Memory. Ðåçóëüòàòû òåñòèðîâàíèÿ ïðèâåäåíû
â òàáë. 4.
Åñëè â ïðîöåññå ðàáîòû ïðîöåäóðû À âûáðàííûé äèçúþíêò íåâîç-
ìîæíî îáíóëèòü áåç âîçíèêíîâåíèÿ ïðîòèâîðå÷èÿ, òî, çíà÷èò, ôóíêöèÿ
íåâûïîëíèìà, è ïðîâîäèòü ïðîâåðêó âîçìîæíîñòè îáíóëåíèÿ îñòàëüíûõ
ñëàãàåìûõ â (10) íå èìååò ñìûñëà. Ïîýòîìó, êàê ñâèäåòåëüñòâóþò ðåçóëü-
òàòû ýêñïåðèìåíòàëüíîãî èññëåäîâàíèÿ, äëÿ âûÿñíåíèÿ ôàêòà íåâûïîëíè-
ìîñòè áóëåâûõ ôóíêöèé ïðîöåäóðîé À òðåáóåòñÿ ñóùåñòâåííî ìåíüøå
âðåìåíè, ÷åì çàòðà÷èâàåòñÿ íà ðåøåíèå çàäà÷è, êîãäà ôóíêöèÿ âûïîëíè-
ìà. Ýòî õîðîøî âèäíî ïðè ðàâíîìåðíîì ðàñïðåäåëåíèè ïåðåìåííûõ X i è
X i ïî äèçúþíêòàì áóëåâîé ôóíêöèè äëÿ çíà÷åíèé ïàðàìåòðà �, çíà÷è-
òåëüíî ìåíüøèõ 0,24. Òàêæå áûñòðî îñóùåñòâëÿåòñÿ ðåøåíèå è äëÿ âûïîë-
íèìûõ ôóíêöèé ïðè çíà÷åíèÿõ ïàðàìåòðà �, ñóùåñòâåííî ïðåâûøàþùèõ
0,24. Íàèõóäøèé ñëó÷àé äëÿ ðàáîòû ïðîöåäóðû, — êîãäà ïàðàìåòð �
ïðèíèìàåò çíà÷åíèå, áëèçêîå ê 0,24.  ýòîì ñëó÷àå ÷èñëî ýëåìåíòàðíûõ
îïåðàöèé, âûïîëíÿåìûõ ïðîöåäóðîé À, íàèáîëåå áëèçêî ê âåðõíåé îöåíêå,
îïðåäåëÿåìîé ñîîòíîøåíèÿìè (7), (8).
Âûâîäû
Ïðåäëîæåííàÿ ïðîöåäóðà À ïîçâîëÿåò ðåøàòü 3-SAT-çàäà÷ó è k-SAT-çàäà÷ó çà
ïîëèíîìèàëüíîå âðåìÿ. Ðàçðàáîòàííûé ìåòîä ðåøåíèÿ SAT-çàäà÷ ïîç-
âîëèò ñîçäàòü áûñòðîäåéñòâóþùèå ïðîãðàììû — SAT-ñîëâåðû, ñïîñîá-
íûå ðåøàòü ìíîãèå çàäà÷è äèñêðåòíîé îïòèìèçàöèè áîëüøîé ðàçìåðíîñòè
â ìàñøòàáå ðåàëüíîãî âðåìåíè, ðàíåå ñ÷èòàâøèåñÿ íåðåøàåìûìè.
Ìåòîä ðåøåíèÿ k-SAT-çàäà÷è ñâåäåíèåì åå ê çàäà÷å î ïîêðûòèè
ISSN 0204–3572. Ýëåêòðîí. ìîäåëèðîâàíèå. 2015. Ò. 37. ¹ 5 33
Òåñò
×èñëî
ïåðå-
ìåííûõ
×èñëî
äèçúþíê-
òîâ
Ñðåäíåå ÷èñëî
âûïîëíåííûõ
îïåðàöèé ïðè
ðåøåíèè
Âðåìÿ ðåøåíèÿ, ìñ
ñðåäíåå
ìèíè-
ìàëüíîå
ìàêñè-
ìàëüíîå
CBS_k3_n100_m403_b0 100 400
. . . . . . . . . . . . . . . . . . . . 51
106 4578 2,28 77843
CBS_k3_n100_m403_b900 100 400
Òàáëèöà 4
ÑÏÈÑÎÊ ËÈÒÅÐÀÒÓÐÛ
1. Hirsch E.A. New Worst-Case Upper Bounds for SAT // Journal of Automated Reasoning. —
2000. — Vol. 24, No 4. — P. 397—420.
2. Ëèñòðîâîé Ñ.Â., Ìèíóõèí Ñ.Â. Ìåòîä ðåøåíèÿ çàäà÷ î ìèíèìàëüíîì âåðøèííîì
ïîêðûòèè â ïðîèçâîëüíîì ãðàôå è çàäà÷è î íàèìåíüøåì ïîêðûòèè // Ýëåêòðîí.
ìîäåëèðîâàíèå. — 2012. — 34, ¹1.— Ñ. 29—43.
3. Ïàïàäèìèòðèó Õ., Ñòàéãëèö Ê. Êîìáèíàòîðíàÿ îïòèìèçàöèÿ. Àëãîðèòìû è ñëîæ-
íîñòü. — Ì.: Ìèð, 1985. — 509ñ.
4. SAT Live [Ýëåêòðîííûé ðåñóðñ]. — Ðåæèì äîñòóïà: www.satlive.org, ñâîáîäíûé.
S.V. Listrovoy, À.V. Sidorenko
METHODS OF SOLUTION TO THE k-SAT-PROBLEM IS BASED
ON ITS REDUCTION TO THE PROBLEM OF COVERING
An algorithm for solving the k-SAT-problem for the average polynomial time and 3-SAT-problem
for the polynomial time. The proposed method can significantly reduce the time to solve
SAT-problems.
K e y w o r d s: SAT-problem, polynomial reducibility.
REFERENCES
1. Hirsch, E.A. (2000), “New Worst-Case Upper Bounds for SAT”, Journal of Automated Rea-
soning, Vol. 24, no. 4, pp. 397-420.
2. Listrovoy, S.V. and Minuchin, S.V. (2012), “The method of solving the problems of the min-
imum vertex cover in an arbitrary graph and the problem of the lowest coverage”, Elekt-
ronnoe modelirovanie, Vol. 34, no. 1, pp. 29-43.
3. Papadimitriou, H. and Stayglits, K. (1985), Kombinatornaya optimizatsiya. Algoritmy i
slozhnost [Combinatorial optimization. Algorithms and complexity], Mir, Moscow, Russia.
4. SAT Live, available at: http: // www.satlive.org.
Ïîñòóïèëà 27.06.14
ïîñëå äîðàáîòêè 03.07.15
ËÈÑÒÐÎÂÎÉ Ñåðãåé Âëàäèìèðîâè÷, ä-ð òåõí. íàóê, ïðîôåññîð, ïðîôåññîð êàôåäðû ñïåöèà-
ëèçèðîâàííûõ êîìïüþòåðíûõ ñèñòåì Óêðàèíñêîãî ãîñóäàðñòâåííîãî óíèâåðñèòåòà æåëåçíî-
äîðîæíîãî òðàíñïîðòà.  1972 ã. îêîí÷èë Õàðüêîâñêîå âûñøåå âîåííîå êîìàíäíî-èíæåíåðíîå
ó÷èëèùå. Îáëàñòü íàó÷íûõ èññëåäîâàíèé — çàäà÷è äèñêðåòíîé îïòèìèçàöèè è òåîðèè ãðàôîâ
è èõ ïðèëîæåíèå ê àíàëèçó âû÷èñëèòåëüíûõ ñèñòåì è ñåòåé.
ÑÈÄÎÐÅÍÊÎ Àíäðåé Âëàäèìèðîâè÷, âåä. èíæåíåð-ïðîãðàììèñò Íàó÷íîãî ïðîèçâîäñòâåí-
íîãî ïðåäïðèÿòèÿ «Ñòàëüýíåðãî» (ã. Õàðüêîâ).  2001 ã. îêîí÷èë Õàðüêîâñêèé âîåííûé óíè-
âåðñèòåò. Îáëàñòü íàó÷íûõ èññëåäîâàíèé — çàäà÷è äèñêðåòíîé îïòèìèçàöèè è òåîðèè ãðà-
ôîâ è èõ ïðèëîæåíèÿ ê àíàëèçó âû÷èñëèòåëüíûõ ñèñòåì è ñåòåé.
Ñ.Â. Ëèñòðîâîé, À.Â. Ñèäîðåíêî
34 ISSN 0204–3572. Electronic Modeling. 2015. V. 37. ¹ 5
|
| id | nasplib_isofts_kiev_ua-123456789-101162 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 0204-3572 |
| language | Russian |
| last_indexed | 2025-12-07T18:14:53Z |
| publishDate | 2015 |
| publisher | Інститут проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України |
| record_format | dspace |
| spelling | Листровой, С.В. Сидоренко, А.В. 2016-05-31T17:54:50Z 2016-05-31T17:54:50Z 2015 Метод решения k-SAT-задачи сведением ее к задаче о покрытии / С.В. Листровой, А.В. Сидоренко // Электронное моделирование. — 2015. — Т. 37, № 5. — С. 17-34. — Бібліогр.: 4 назв. — рос. 0204-3572 https://nasplib.isofts.kiev.ua/handle/123456789/101162 519.682.1 Предложен алгоритм решения k-SAT-задачи в среднем за полиномиальное время и 3-SATзадачи за полиномиальное время. Предлагаемый метод позволяет существенно сократить время решения SAT-задач. Запропоновано алгоритм розв’язку k-SAT-задачі в середньому за поліноміальний час і 3-SAT-задачі за поліноміальний час. Запропонований метод дозволяє істотно скоротити час розв’язку SAT-задач . An algorithm for solving the k-SAT-problem for the average polynomial time and 3-SAT-problem for the polynomial time. The proposed method can significantly reduce the time to solve SAT-problems. ru Інститут проблем моделювання в енергетиці ім. Г.Є. Пухова НАН України Электронное моделирование Математическое моделирование и вычислительные методы Метод решения k-SAT-задачи сведением ее к задаче о покрытии Methods of solution to the k-SAT-problem is based on its reduction to the problem of covering Article published earlier |
| spellingShingle | Метод решения k-SAT-задачи сведением ее к задаче о покрытии Листровой, С.В. Сидоренко, А.В. Математическое моделирование и вычислительные методы |
| title | Метод решения k-SAT-задачи сведением ее к задаче о покрытии |
| title_alt | Methods of solution to the k-SAT-problem is based on its reduction to the problem of covering |
| title_full | Метод решения k-SAT-задачи сведением ее к задаче о покрытии |
| title_fullStr | Метод решения k-SAT-задачи сведением ее к задаче о покрытии |
| title_full_unstemmed | Метод решения k-SAT-задачи сведением ее к задаче о покрытии |
| title_short | Метод решения k-SAT-задачи сведением ее к задаче о покрытии |
| title_sort | метод решения k-sat-задачи сведением ее к задаче о покрытии |
| topic | Математическое моделирование и вычислительные методы |
| topic_facet | Математическое моделирование и вычислительные методы |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/101162 |
| work_keys_str_mv | AT listrovoisv metodrešeniâksatzadačisvedeniemeekzadačeopokrytii AT sidorenkoav metodrešeniâksatzadačisvedeniemeekzadačeopokrytii AT listrovoisv methodsofsolutiontotheksatproblemisbasedonitsreductiontotheproblemofcovering AT sidorenkoav methodsofsolutiontotheksatproblemisbasedonitsreductiontotheproblemofcovering |