Hardprob/Maximum Renamable Horn Subformula — различия между версиями

Материал из DISCOPAL
Перейти к: навигация, поиск
(Массовая правка: замена \cup на ∪)
Строка 1: Строка 1:
 
<!-- start --><!-- {{svg-image-for-hard-problem|{{PAGENAME}}}} -->
 
<!-- start --><!-- {{svg-image-for-hard-problem|{{PAGENAME}}}} -->
 
* Набор булевых переменных <em>U</em>, коллекция <em>C</em> скобок-конъюнкций не больше чем из трех литералов.
 
* Набор булевых переменных <em>U</em>, коллекция <em>C</em> скобок-конъюнкций не больше чем из трех литералов.
* Найти [https://en.wikipedia.org/wiki/Horn-satisfiability переименовываемую хорнову подформулу] <em>C'</em> от <em>C</em>, т.е. подмножество <em>C'⊆ C</em>, т.к. здесь существует подмножество <em>S ⊆ U</em>, таких переменных, что перестановка литералов в <m>S \cup \bar{S}</m> делает <em>C'</em> хорновой булевой формулы, где <m>\bar{S} = \{\bar{u} \mid u \in S\}</m>.
+
* Найти [https://en.wikipedia.org/wiki/Horn-satisfiability переименовываемую хорнову подформулу] <em>C'</em> от <em>C</em>, т.е. подмножество <em>C'⊆ C</em>, т.к. здесь существует подмножество <em>S ⊆ U</em>, таких переменных, что перестановка литералов в <m>S \bar{S}</m> делает <em>C'</em> хорновой булевой формулы, где <m>\bar{S} = \{\bar{u} \mid u \in S\}</m>.
 
* Максимизировать размер подформулы, т.е. <em>|C'|</em>.
 
* Максимизировать размер подформулы, т.е. <em>|C'|</em>.
  

Версия 11:39, 17 апреля 2023

  • Набор булевых переменных U, коллекция C скобок-конъюнкций не больше чем из трех литералов.
  • Найти переименовываемую хорнову подформулу C' от C, т.е. подмножество C'⊆ C, т.к. здесь существует подмножество S ⊆ U, таких переменных, что перестановка литералов в делает C' хорновой булевой формулы, где .
  • Максимизировать размер подформулы, т.е. |C'|.

Задача в лаб22 (рид-онли просмотр)