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

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

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

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