\documentclass[11pt,reqno]{amsart}
\usepackage[cp1251]{inputenc}
\usepackage[english,russian]{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{graphicx}
\usepackage{xcolor}
\usepackage[colorlinks]{hyperref}


\usepackage{titlesec}
\titlespacing{\section}{0pt}{2.5ex}{1.5ex}
\titlespacing{\subsection}{0pt}{1.5ex}{1ex}
\titlespacing{\subsubsection}{0pt}{1.5ex}{1ex}
\titleformat{\section}{\large\bfseries\centering}{\thesection}{1em}{}
\titleformat{\subsection}[runin]{\bfseries}{\thesubsection.}{0.5em}{}[.\mbox{\ }]
\titleformat{\subsubsection}[runin]{\bfseries}{\thesubsubsection.}{0.4em}{}[.\mbox{\ }]



%%%%%---------- ORCiD
\newcommand\orcidicon[1]{\href{https://orcid.org/#1}{\includegraphics[scale=0.02]{orcid.pdf}}}

\def\udcs{510.52} %Здесь автор определяет УДК своей работы
\def\mscs{68Q17} %Здесь автор определяет классификаторы AMS своей работы
\setcounter{page}{1}

\newtheorem{lemma}{Лемма}
\newtheorem{theorem}{Теорема}
\newtheorem{definition}{Определение}
\newtheorem{corollary}{Следствие}
\newtheorem{proposition}{Предложение}


\definecolor{myblue}{rgb}{0.03, 0.27, 0.79}

\hypersetup{linkcolor=blue,filecolor=black,urlcolor=blue, citecolor=blue}

\def\logo{\textcolor{blue}{{\bf\Huge S\raisebox{0.2ex}{\hspace{0.55ex}\raisebox{0.05ex}e\hspace{-1.65ex}$\bigcirc$}MR}}}

\def\semrtop
     {
  \vbox{
     \noindent\logo \hspace{-3mm}  \parbox{12cm}{     \begin{center}
     {\LARGE \textsf{СИБИРСКИЕ ЭЛЕКТРОННЫЕ}} \\[2mm]
     {\LARGE \textsf{МАТЕМАТИЧЕСКИЕ ИЗВЕСТИЯ}} \\[2mm]
     {\Large \textsf{Siberian Electronic Mathematical Reports}} \\[1mm]
     {\Large\tt{\textcolor{blue}{http://semr.math.nsc.ru}}}\\[1mm]
     \raisebox{1ex}{ISSN 1813-3304 }
     \vspace*{-3mm}
%     {\small Институт математики им. С.Л.Соболева СО РАН}\\[-1mm]
%     {\small Sobolev Institute of Mathematics SB RAS}
     \end{center}
}
     \vspace{-1mm}
     \noindent
      \begin{tabular}{c}
     \hphantom{aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa!} \\
     \hline\hline
     \end{tabular}

     \vspace{3mm}
     {\flushleft\it Том 20, № 2, стр. 144--145 (2023) \hspace{\fill}{\rm\small УДК \udcs \hspace{-4mm}}}
     \newline
     	{\rm\small \textcolor{blue}{https://doi.org/10.33048/semi.2023.20.???}}\hphantom{aaaaaaaaaaaaaaaaaaaaaaaa\;}{\rm\small MSC\ \ \mscs }
  }%\vbox
}



\begin{document}
\renewcommand{\refname}{References}


\thispagestyle{empty}

\title[\sc Дизъюнктивно-связные варианты выполнимости]{\large Дизъюнктивно-связные варианты проблемы выполнимости}
\author[В.Ю. ПОПОВ]{{\bf \large \textsc{В.Ю. Попов}}\protect\orcidicon{0000-0001-9671-681X}\\ \\
%\textit{Представлено} \textsc{П.П. Петровым}
%\textit{(заполняется редактором)}
}%
\address{Vladimir Yurievich Popov  % Контактные данные всех авторов и место работы указываются только на английском языке
\newline\hphantom{iii} Ural Federal University,
\newline\hphantom{iii} Lenin st., 51,
\newline\hphantom{iii} 620083, Ekaterinburg, Russia}%
\email{\textcolor{blue}{popovvvv@gmail.com}}%

\thanks{\sc Popov, V.Yu.,
Clause-connected versions of the satisfiability problem}
\thanks{\copyright \ 2023 Попов В.Ю}
%\thanks{\rm Работа поддержана РФФИ (грант 03-01-11111)}
\thanks{\it Поступила 1 января 2023 г., опубликована 31 декабря 2023 г.}%


\semrtop \vspace{1cm}
\maketitle {\small
\begin{quote}
\noindent{\bf Abstract:} The satisfiability problem is one of the most famous computationally hard algorithmic problems.
It is well known that the satisfiability problem remains hard even in the restricted version in which Boolean formulas
in conjunctive normal form with exactly three distinct literals per clause. However, the problem can be solved in polynomial time
for Boolean formulas with exactly two distinct literals per clause.
Narrowing the gap between the problems is of fundamental interest.
Therefore, it is natural to analyze the complexity of some restricted versions of the satisfiability problem.
In this paper, we prove hardness of some clause-connected versions of the satisfiability problem.\medskip

\noindent{\bf Keywords:} satisfiability problem, computational complexity, {\bf NP}-complete.
 \end{quote}
}

\bigskip

\section*{Введение}
Проблема выполнимости булевой функции ({\sc SAT}) является одной из наиболее известных вычислительно трудных алгоритмических проблем.
Обычно проблема {\sc SAT} рассматривается для булевых функций в конъюнктивной нормальной форме.
При этом хорошо известно, что проблема {\sc 3SAT}, в которой допускается в дизъюнкциях ровно по три литерала, остается {\bf NP}-полной, а проблема {\sc 2SAT}, в которой допускается в дизъюнкциях ровно по два литерала, разрешима за полиномиальное время.
Сужение зазора между {\sc 3SAT} и {\sc 2SAT} представляет фундаментальный интерес и вызывает большое внимание у исследователей
(см., например, \cite{Berman__Karpinski__2007,Darmann__Docker__2021,Misra__Narayanaswamy__2010}).
Для рассмотрения ограниченных версий проблемы {\sc 3SAT} имеется большое количество дополнительных важных причин.

Проблема {\sc 3SAT} использовалась для получения многочисленных результатов по вычислительной трудности. Поэтому
доказательство трудности для ограниченного варианта {\sc 3SAT} во многих случаях позволяет получить важные следствия для
других проблем.


Рассмотрим произвольную булеву функцию $f(x_1,x_2, \dots , x_n)$ в конъюнктивной нормальной форме.
Без ограничения общности мы можем полагать, что функция $f(x_1,x_2, \dots , x_n)$ имеет вид
\begin{equation}\label{f0}
\wedge_{i=1}^m C_i,
\end{equation}
где для любого $i$, $1 \leq i \leq m$, функция $C_i$ является дизъюнкцией литералов,
т.е.
\begin{equation}\label{f1}
C_i=\vee_{j=1}^{p_i} u_{i,j},
\end{equation}
$$u_{i,j} \in \{ x_1, x_2, \dots , x_n, \neg x_1, \neg x_2, \dots , \neg x_n \}.$$
Сведение различных вычислительно трудных проблем к проблема выполнимости и решение их при помощи
специально разработанных для {\sc SAT} программ уже давно рассматривается как эффективный метод решения задач.
Однако стандартная процедура приведения произвольной булевой функции к виду (\ref{f0}) является, вообще говоря,
экспоненциальной.
Даже использование эффективных алгоритмов
(см., например, \cite{Tseitin__1983})
для приведения к виду (\ref{f0}) накладывает значительную дополнительную вычислительную нагрузку
на программу-решатель.
Конкретный вид выражений (\ref{f1}) тоже имеет важное значение, поскольку упрощение выражения
(\ref{f1}) может оказать существенное влияние на количество переменных, количество и структуру решений.
Поэтому при построении сведений прикладных задач к проблеме выполнимости важно заботиться о
конкретном виде получаемых булевых функций. При этом, накладывая ограничения на вид булевых функций,
необходимо знать, сохраняет ли ограниченный вариант проблемы {\sc SAT} выразительные способности {\sc SAT}.
С другой стороны при построении сведений задач робототехники
(см., например, \cite{Curtis__Tenenbaum__2022,Ablad__Spensieri__2023,Meli__Nakawala__2023}),
планирования для автономных транспортных средств
(см., например, \cite{Matlekovic__Schneider-Kamp__2023,Wang__Ma__Wang__2021}),
майнинга криптовалюты \cite{Abed__Ashkanan__2020}, криптоанализа
(см., например, \cite{Trimoska__Ionica__2020,Utsumi__Sakamoto__2023}),
моделирования квантовых вычислительных процессов
(см., например, \cite{Huang__Newman__2020,Schneider__Burgholzer__2023})
и многих других часто булевы функции специального вида возникают естественным образом.
Даже если выявление дополнительной структуры не ведет к нахождению полиномиального алгоритма,
во многих случаях появляется возможность для создания более эффективной программы-решателя.
В последние годы при разработке программ-решателей все большее внимание уделяется не стандартным формулировкам {\sc SAT} и {\sc 3SAT}, а упрощенным вариантам {\sc 3SAT}
(см., например, \cite{Bliznets__Sagunov__2022}).
Во многих случаях известные специализированные варианты проблемы {\sc 3SAT} недостаточно хорошо отражают
специфику прикладной задачи, что требует введения сложных дополнительных структур и приводит к совместному решению нескольких
задач
(см., например, \cite{Lin__Althoff__2022}).
Исследование различных прикладных задач приводит к рассмотрению новых вариантов проблемы {\sc 3SAT}.
При этом существенное внимание уделяется исследованию дополнительных ограничений на проблему {\sc 3SAT},
обеспечивающих некоторую связность между переменными в различных дизъюнкциях
(см., например, \cite{Caballero__Gomez__2023,Demaine__Eisenstat__2011}).
Характерным примером является исследование, представленное в работе \cite{Imeson__Smith__2019},
где вариант проблемы {\sc 3SAT} с дополнительным условием на связность переменных
решается совместно с другой оптимизационной задачей.

Программы-решатели для вариантов проблемы выполнимости демонстрируют высокую эффективность
при решении многих прикладных задач. Однако часто их использование сопряжено с трудностями, обусловленными недостаточным количеством
тестовых данных \cite{Giraldez__Levy__2016}, что вызывает потребность генерации булевых функций специального вида
(см., например,
\cite{Amendola__Ricca__2020,Barak-Pelleg__Berend__2022,Heradio__Fernandez__2022}).
Активное использование методов машинного обучения для программ-решателей
(см., например,
\cite{Ebert__Weyrich__2021,Guo__Zhen__Li__2023,Sun__Gerault__2020})
требует учета специфики не только прикладной области, но и самих методов машинного обучения.
Хорошо известно, что интеллектуальные системы обычно медленно обучаются на разреженных данных.
С другой стороны данные высокой плотности часто вызывают быстрое переобучение.
Кроме того, специфика исходных данных вызывает определенные трудности в применении программ-решателей для криптоанализа
(см., например,
\cite{Leventi__Peetz__2019,Mosca__Verschoor__2022}).


Многие современные криптографические алгоритмы работают с разреженными или плотными
данными
(см., например,
\cite{Branco__Mateus__2020,Egger__Xhemrishi__2023,Perez_Pacheco__Caballero_Gil__2023}).
Соответственно разрабатываются методы криптоанализа, которые ориентируются на поиск специфических закономерностей, связанных с разреженными и плотными данными \cite{Afzal__Yousaf__2020,Baldi__Deneuville__2021}.
Принципиальная возможность нахождения подобных закономерностей основывается на наличии фазового перехода, который
характерен не только для алгоритмических проблем, но и для физических систем в целом
\cite{Hartmann__Weigt__2005,Mezard__Montanari__2009,Moore__Mertens__2011}.
Суть фазового перехода в том, что для исходных данных одного и того же размера
структура решений может значительно отличаться. Соотверственно, трудность проблемы зависит не столько от размера
исходных данных, сколько от некоторых их структурных особенностей.
Исследования этого феномена тесно связаны с пороговой гипотезой, согласно которой
трудность исходных данных зависит от отношения размера исходных данных к количеству переменных,
т.е. от степени их плотности. Для проблемы {\sc 3SAT} это отношение можно рассматривать как отношение
$\frac{m}{n}$
количества дизъюнкций $m$ к количеству переменных $n$
\cite{Mitchell__Selman__1992}.
Многие вычислительно трудные проблемы демонстрируют предсказуемое поведение в зависимости от плотности
исходных данных, что существенно облегчает их решение
(см., например,
\cite{Cheeseman__Kanefsky__1991,Sleegers__Olij__2000}).
Весьма значительное внимание было уделено изучению пороговой гипотезы для проблемы {\sc SAT}
(см., например,
\cite{Mezard__Parisi__2002,Biroli__Cocco__2002}.
Обзор современного состояния исследований по пороговой гипотезе дан в работе
\cite{Perkins__2024}.
В частности, следует отметить, что недавно пороговая гипотеза получила подтверждение как для проблемы выполнимости
\cite{Ding__Sly__2016,Ding__Sly__2022}, так и в общем случае
\cite{Park__Pham__2024}.
Однако исследования, представленные в работе
\cite{Schawe__Bleim__2019}, показывают наличие нетривиальных зависимостей у проблемы выполнимости,
которые не могут быть описаны одним лишь подтверждением пороговой гипотезы.
В частности, у проблемы {\sc 3SAT} наблюдается несколько фазовых переходов.
Тем не менее, нахождение эффективных методов, позволяющих гибко регулировать связность булевых функций,
представляет значительный интерес для разработки методов генерации булевых функций и маскировки для криптографических алгоритмов.
В частности, их можно было бы применять для тех значений плотности, для которых общее поведение
решений проблемы выполнимости сравнительно предсказуемо.
При этом при помощи полиномиальных сведений маскировку на основе булевых функций можно
применять не только для сравнительно непопулярных алгоритмов, основанных непосредственно на {\sc SAT}
\cite{Schmittner__2015,Sun__Peng__Tian__2017,Thomas__Chaudhari__2011},
но и для алгоритмов на целочисленных решетках или схем на основе Classic McEliece.

Пожалуй, наиболее основательно вопрос о требованиях к булевым функциям проработан в области генерации трудных входов
для программ-решателей
(см., например,
\cite{Li__Chen__Guo__2023,Newsham__Ganesh__2014,Slater__2002}).
В частности, в работе
\cite{Li__Chen__Guo__2023}
указывается, что в отличие от случайных булевых функций индустриальные должны демонстрировать
наличие определенной структуры связей. При этом одной из ключевых проблем генерации является
деградация сложности из-за ограниченности инструментов модификации \cite{Li__Chen__Guo__2023}.
В свою очередь, ограниченные возможности модификации обусловлены стремлением сохранить семантику
булевых функций, получаемых из экспериментальных данных.
Таким образом, необходимы эффективные инструменты, позволяющие осуществлять гибкую модификацию структуры
связей в булевой функции, наследуя трудность исходной функции.
С другой стороны, для разработки самих решателей необходимы трудные варианты {\sc 3SAT}, ориентированные не
на случайные входы, а на структурированные.

Основной целью данной статьи является описание простых преобразований для регулирования связности булевых функций,
которые можно использовать как эффективный инструмент при генерации булевых функций и маскировке данных.
На основе этих преобразований мы получим ряд трудных вариантов проблемы выполнимости, которые можно использовать не
только для доказательства {\bf NP}-трудности, но и для исследований за пределами {\bf NP}.

\section{Дизъюнктивно-связные булевы функции}

Будем говорить, что литерал $x$ принадлежит дизъюнкции $C_i$ вида (\ref{f1}) и писать $x \in C_i$,
если существует значение $j$ такое, что $x=u_{i,j}$. Для любого литерала $x$ будем полагать, что $x= \neg \neg x$.
Для булевой функции $f$ вида (\ref{f0})рассмотрим граф $G_f=(V_f,E_f)$, заданный множеством вершин
\begin{equation}\label{f2}
V_f=\{ C_i \mid 1 \leq i \leq m \}
\end{equation}
и множеством ребер
\begin{eqnarray}\label{f3}
&E_f=\{ (C_i,C_j) \mid 1 \leq i \leq m, 1 \leq j \leq m,
\nonumber \\
&\exists x ( (x \in C_i \vee \neg x \in C_i)
\wedge (x \in C_j \vee \neg x \in C_j))\}.
\end{eqnarray}
Следуя \cite{Demaine__Karntikoon__2023}, булеву функцию $f$ вида (\ref{f0}) будем называть дизъюнктивно-связной, если граф $G_f$ является связным.
Рассмотрим граф $D_f=(V_f,P_f)$, заданный множеством вершин
(\ref{f2})
и множеством ребер
\begin{eqnarray}\label{f4}
&P_f=\{ (C_i,C_j) \mid 1 \leq i \leq m, 1 \leq j \leq m,
\nonumber \\
&\exists x ( x \in C_i \wedge x \in C_j )\}.
\end{eqnarray}
Булеву функцию $f$ вида (\ref{f0}) будем называть сильно дизъюнктивно-связной, если граф $D_f$ является связным.
Исходя из ограничений (\ref{f3}) и (\ref{f4}), накладываемых на ребра графа, у дизъюнктивно-связной булевой функции между
дизъюнкциями существует связь тогда и только тогда, когда у них есть общая переменная, а у сильно дизъюнктивно-связной булевой функции между
дизъюнкциями существует связь тогда и только тогда, когда у них есть общий литерал.

\section{Дизъюнктивно-связная {\sc 3SAT}}
Рассмотрим сначала формулировку основной проблемы выполнимости в удобной для нас форме.

{\sc Проблема выполнимости  (SAT).}

{\sc Дано:} {\it Булева функция
$f(x_1,x_2, \dots , x_n) =\wedge_{i=1}^m C_i$, где для любого $i$,
$1\leq i \leq m$, функция $C_i$ является дизъюнкцией литералов.}

{\sc Вопрос:} {\it Существует ли набор значений переменных $x_j$,
$x_j \in \{ 0,1 \}$, $1\leq j \leq m$, такой, что выполняется равенство $f(x_1,x_2, \dots , x_m) =1$?}

Согласно теореме Кука, проблема {\sc SAT} является {\bf NP}-полной. Хотя этого утверждения в явном виде в работе \cite{Cook__1971} нет, из рессуждений, представленных в статье \cite{Cook__1971}, очевидным образом вытекает его справедливость.

Теперь рассмотрим проблему {\sc 3SAT}, предложенную в книге \cite{Garey__Johnson__1979}.
Мы приведем формулировку проблемы {\sc 3SAT} в удобной для нас форме, отличающейся от формулировки из \cite{Garey__Johnson__1979} лишь терминологически.

{\sc Проблема 3-выполнимости  (3SAT).}

{\sc Дано:} {\it Булева функция
$f(x_1,x_2, \dots , x_n) =\wedge_{i=1}^m C_i$, где для любого $i$,
$1\leq i \leq m$, функция $C_i$ является дизъюнкцией ровно трех литералов.}

{\sc Вопрос:} {\it Существует ли набор значений переменных $x_j$,
$x_j \in \{ 0,1 \}$, $1\leq j \leq m$, такой, что выполняется равенство $f(x_1,x_2, \dots , x_m) =1$?}

В книге \cite{Garey__Johnson__1979} проблема {\sc 3SAT} представлена как одна из {\bf NP}-полных проблем
из списка Карпа \cite{Karp__1972}.
В книге \cite{Garey__Johnson__1979} приведена полиномиальная сводимость проблемы {\sc SAT} к {\sc 3SAT}.
Заметим, что в статье Карпа \cite{Karp__1972} в списке {\bf NP}-полных проблем проблемы {\sc 3SAT} нет.
Карп рассматривал следующую проблему.

{\sc Проблема $\leq$3-выполнимости ($\leq$3SAT).}

{\sc Дано:} {\it Булева функция
$f(x_1,x_2, \dots , x_n) =\wedge_{i=1}^m C_i$, где для любого $i$,
$1\leq i \leq m$, функция $C_i$ является дизъюнкцией не более трех литералов.}

{\sc Вопрос:} {\it Существует ли набор значений переменных $x_j$,
$x_j \in \{ 0,1 \}$, $1\leq j \leq m$, такой, что выполняется равенство $f(x_1,x_2, \dots , x_m) =1$?}

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

{\sc Проблема выполнимости дизъюнктивно-связной булевой \\
функции (C-SAT).}

{\sc Дано:} {\it Булева функция
$f(x_1,x_2, \dots , x_n) =\wedge_{i=1}^m C_i$ такая, что граф $G_f$ является связным и для любого $i$,
$1\leq i \leq m$, функция $C_i$ является дизъюнкцией литералов.}

{\sc Вопрос:} {\it Существует ли набор значений переменных $x_j$,
$x_j \in \{ 0,1 \}$, $1\leq j \leq m$, такой, что выполняется равенство $f(x_1,x_2, \dots , x_m) =1$?}

{\sc Проблема 3-выполнимости дизъюнктивно-связной булевой
функции (C-3SAT).}

{\sc Дано:} {\it Булева функция
$f(x_1,x_2, \dots , x_n) =\wedge_{i=1}^m C_i$ такая, что граф $G_f$ является связным и для любого $i$,
$1\leq i \leq m$, функция $C_i$ является дизъюнкцией ровно трех литералов.}

{\sc Вопрос:} {\it Существует ли набор значений переменных $x_j$,
$x_j \in \{ 0,1 \}$, $1\leq j \leq m$, такой, что выполняется равенство $f(x_1,x_2, \dots , x_m) =1$?}

{\sc Проблема $\leq$3-выполнимости дизъюнктивно-связной булевой функции (C-$\leq$3SAT).}

{\sc Дано:} {\it Булева функция
$f(x_1,x_2, \dots , x_n) =\wedge_{i=1}^m C_i$ такая, что граф $G_f$ является связным и для любого $i$,
$1\leq i \leq m$, функция $C_i$ является дизъюнкцией не более трех литералов.}

{\sc Вопрос:} {\it Существует ли набор значений переменных $x_j$,
$x_j \in \{ 0,1 \}$, $1\leq j \leq m$, такой, что выполняется равенство $f(x_1,x_2, \dots , x_m) =1$?}

Заметим, что если булева функция $f(x_1,x_2, \dots , x_n)$
не является дизъ\-юнктив\-но-\-связ\-ной, то найдутся булевы функции
$$g(x_{i_1},x_{i_2}, \dots , x_{i_p}) =C_{j_1} \wedge C_{j_2} \wedge  \dots \wedge C_{j_q},$$
$$h(x_{r_1},x_{r_2}, \dots , x_{r_s}) =C_{l_1} \wedge C_{l_2} \wedge  \dots \wedge C_{l_t}$$
такие, что
$$n=p+s,$$
$$m=q+t,$$
$$\{x_1,x_2, \dots , x_n\} = \{x_{i_1},x_{i_2}, \dots , x_{i_p}\} \cup \{x_{r_1},x_{r_2}, \dots , x_{r_s}\},$$
$$\{x_{i_1},x_{i_2}, \dots , x_{i_p}\} \cap \{x_{r_1},x_{r_2}, \dots , x_{r_s}\} = \emptyset ,$$
$$\{C_{1}, C_{2},  \dots , C_{m}\} =
\{ C_{j_1}, C_{j_2}, \dots , C_{j_q} \} \cup
\{ C_{l_1}, C_{l_2},  \dots , C_{l_t} \},$$
$$\{ C_{j_1}, C_{j_2}, \dots , C_{j_q} \} \cap
\{ C_{l_1}, C_{l_2},  \dots , C_{l_t} \}= \emptyset .$$
В этом случае функция $f$ будет выполняться тогда и только тогда, когда быдет выполнимой каждая из
функций $g$ и $h$.
Соответственно, если у нас есть полиномиальный алгоритм для проверки выполнимости дизъюнктивно-связной
булевой функции, то найдется и полиномиальный алгоритм для проверки выполнимости произвольной
булевой функции, т.е. если проблема {\sc C-3SAT} принадлежит классу {\bf P}, то и
проблема {\sc 3SAT}  принадлежит классу {\bf P}.
Однако, если ${\bf P} \not= {\bf NP}$
из только что рассмотренных рассуждений не следует автоматически, что {\sc 3SAT}
полиномиально сводится к {\sc C-3SAT},
поскольку проверка выполнимости функции $f$ по функциям $g$ и $h$ потребует {\bf NP}-оракула.
При решении задачи на практике функции {\bf NP}-оракула может выполнить программа-решатель.
Однако это не подходит для задач, требующих совместного решения нескольких проблем, и задач, в которых
важна семантическая нагрузка булевой функции.

Для каждой из трех сформулированных проблем доказательство {\bf NP}-полноты можно получить как следствие
{\bf NP}-полноты проблемы {\sc 3SAT}, используя локальное преобразование, предложенное в работе
\cite{Demaine__Karntikoon__2023}.
Очевидно, что если у каждой пары дизъюнкций есть общая переменная, то граф $G_f$ является связным.
Если граф $G_f$ не является связным, то найдутся дизъюнкции литералов
$\vee_{i=1}^p u_i$
и
$\vee_{j=1}^q v_j$,
не имеющие общих переменных.
Возьмем новую переменную $y$ и заменим в функции $f(x_1,x_2, \dots , x_n)$ подформулу
\begin{equation}\label{f5}
(\vee_{i=1}^p u_i ) \wedge (\vee_{j=1}^q v_j )
\end{equation}
на формулу
\begin{equation}\label{f6}
(\vee_{i=1}^{p} u_i ) \wedge (\vee_{j=1}^{q} v_j ) \wedge (u_p \vee v_q \vee y).
\end{equation}
Получим функцию $g(x_1,x_2, \dots , x_n,y)$.
Очевидно, что замена формулы (\ref{f5}) на формулу (\ref{f6})
уменьшает количество пар дизъюнкций, у которых нет общих переменных.
Соответственно функция $g$ содержит на одну пару меньше, чем
функция $f$.
При этом поскольку все дизъюнкции функции $f$ содержатся в функции
$g$, из выполнимости функции $g$ следует выполнимость функции $f$.
Если функция $f$ истинна на некотором наборе
$t_1,t_2, \dots , t_n$,
то $g(t_1,t_2, \dots , t_n,1)=1$.
Следовательно, замена формулы (\ref{f5}) на формулу (\ref{f6}) сохраняет выполнимость.
Легко понять, что последовательное применение замены формулы (\ref{f5}) на формулу (\ref{f6})
позволяет получить полиномиальную сводимость от проблемы {\sc 3SAT} к проблеме
{\sc C-3SAT}.
Учитывая очевидную принадлежность проблемы {\sc C-3SAT} классу {\bf NP},
это доказывает {\bf NP}-полноту проблемы {\sc C-3SAT}.
Поскольку проблема {\sc C-3SAT} является частным случаем проблем
{\sc C-SAT} и {\sc C-$\leq$3SAT},
каждая из них тоже является {\bf NP}-полной.

Заметим, что, осуществляя последовательные замены формул вида (\ref{f5}) на формулы вида (\ref{f6}),
мы можем использовать одну и ту же переменную $y$. Поэтому мы можем получить итоговую функцию,
содержащую единственную дополнительную переменную $y$, отсутствующую в начальном списке переменных.

Хотя использование замены  формул вида (\ref{f5}) на формулы вида (\ref{f6})
обеспечивает простой способ перехода от произвольной булевой функции к дизъюнктивно-связной,
у этого способа есть серьезный недостаток. При таком построении дизъюнктивно-связной
булевой функции не наследуется количество решений, поскольку при определенных условиях
мы, кроме решения вида $t_1,t_2, \dots , t_n,1$, можем получить решение вида $t_1,t_2, \dots , t_n,0$.
Причем не всегда есть очевидный способ для отслеживания, следует ли из того, что
$t_1,t_2, \dots , t_n,1$ является решением, то, что $t_1,t_2, \dots , t_n,0$
тоже будет решением. Заметим, что в общем случае проблема, требующая выяснить по данной
булевой функции $f(x_1,x_2, \dots , x_n)$ и данному решению $t_1,t_2, \dots , t_n$, существует ли еще один набор,
на котором функция $f$ выполняется, является {\bf NP}-полной \cite{Juban__1999}.

Отсутствие сохранения количества решений при сводимости существенно затрудняет дальнейшее использование проблемы
для исследований, связанных с многиги важными классами, находящимися за пределами класса {\bf NP},
что значительно уменьшает полезность преобразования на основе замены  формул вида (\ref{f5}) на формулы вида (\ref{f6})
с теоретической точки зрения.
С практической точки зрения преобразования, которые не сохраняют количество решений, тоже не всегда допустимы.
В частности, их нельзя использовать совместно с \#{\sc SAT}-решателями
\cite{Sundermann__Hess__2023,Sundermann__Thum__2020}.
Во многих случаях недопустимо применять такие преобразования в криптографических целях.
Их нельзя применять при проектировании квантовых вычислительных схем.
Кроме того, исследования показывают, что при генерации случайных булевых функций для программ-решателей
важно учитывать количество решений для этих функций даже в тех случаях, когда перед решателем ставится задача
проверки выполнимости, а не нахождения решений
\cite{Zhao__Liao__Luo__2023}.

\section{Классы количественных алгоритмических проблем}
На сегодняшний день предложено довольно большое количество
сводимостей, которые можно использовать для исследования алгоритмических зависимостей между проблемами
\cite{Downey__Fellows__1999,Flum__Grohe__2004,Ladner__Lynch__1975}.
Для проблем из класса {\bf NP} стандартной является полиномиальная сводимость.

Для произвольного множества $\Sigma$ обозначим через $\Sigma^{\ast}$ множество всевозможных слов над алфавитом $\Sigma$.
Для произвольных языков $L_1$, $L_1 \subseteq \Sigma_1^{\ast}$, и $L_2$, $L_2 \subseteq \Sigma_2^{\ast}$,
следуя \cite{Garey__Johnson__1979}, будем говорить, что язык $L_1$ полиномиально сводится к языку $L_2$,
если существует детерминированная машина Тьюринга, вычисляющая за полиномиальное время функцию
$f : \Sigma_1^{\ast} \rightarrow \Sigma_2^{\ast}$ такую, что
$x \in L_1$ тогда и только тогда, когда $f(x) \in L_2$ для любого $x \in \Sigma_1^{\ast}$.
Если язык $L_1$ полиномиально сводится к языку $L_2$ будем писать
$L_1 \leq_T L_2$.

Язык $L$ называется {\bf NP}-полным, если $L \in {\bf NP}$ и $M \leq_T L$ для любого языка $M$ из {\bf NP}.
Алгоритмическая проблема, предполагающая решение из множества $\{ 0, 1\}$, называется {\bf NP}-полной,
если {\bf NP}-полным является описывающий ее язык. Заметим, что если решение проблемы не обязательно из множества
$\{ 0, 1\}$, то проблема относится к классу функциональных проблем.
В частности, через {\bf FP} мы будем обозначать класс функциональных проблем, разрешимых детерминированной
машиной Тьюринга за полиномиальное время.
Заметим, что машина Тьюринга, устанавливающая полиномиальную сводимость языка $L_1$ к языку $L_2$,
решает некоторую проблему $f$ из класса {\bf FP}.

Следуя \cite{Papadimitriou__1994}, будем говорить, что язык $L_1$ логарифмически сводится к языку $L_2$,
если существует детерминированная машина Тьюринга, вычисляющая функцию
$f : \Sigma_1^{\ast} \rightarrow \Sigma_2^{\ast}$ с использованием памяти $O( \log n)$ такую, что
$x \in L_1$ тогда и только тогда, когда $f(x) \in L_2$ для любого $x \in \Sigma_1^{\ast}$.
Если язык $L_1$ логарифмически сводится к языку $L_2$ будем писать
$L_1 \leq_L L_2$.
Заметим, что если машина Тьюринга обеспечивает логарифмическую сводимость языка $L_1$
к языку $L_2$, то она всегда останавливается через полиномиальное количество шагов (см. \cite{Papadimitriou__1994},
предложение 8.1). Поэтому из $L_1 \leq_L L_2$ следует $L_1 \leq_T L_2$.
Таким образом, требование логарифмической сводимости, вообще говоря, более сильное, чем необходимо
для доказательства {\bf NP}-трудности. Однако логарифмическая сводимость в отличие от полиномиальной позволяет
работать с подклассами класса {\bf P} языков, распознаваемых детерминированной машиной Тьюринга за полиномиальное время.
В частности, логарифмическую сводимость можно использовать для класса {\bf NL} языков, распознаваемых недетерминированной машиной Тьюринга на логарифмической памяти.
Кроме того, использование логарифмической сводимости представляет существенный практический интерес.
В последние годы все большее внимание уделяется таким вопросам как автоматическая генерация тестов \cite{Jayasena__Mishra__2024}; разработка языков программирования для решения задач при помощи решателей \cite{Lin__Zhao__2004,Rubio__Cantarero__2024,Soh__Tamura__Banbara__2013}; аппаратная реализация решателей \cite{Kim__Rahman__2024,Sohanghpurwala__Hassan__2017}; аппаратная реализация решателей
как многоцелевых процессоров \cite{Hu__Zhang__Ardeshiricham__2017,Mahmoud__Shokry__2024}; аппаратная реализация программ, созданных решателями \cite{Su__Kim__Kim__2024}. Все это указывает на постепенно формирующуюся тенденцию перехода от программного
решения прикладных задач при помощи решателей к аппаратному, что требует экономного отношения к памяти при построении сводимостей.
В дальнейшем под полиномиальной сводимостью языка $L_1$ к языку $L_2$ мы будем понимать логарифмическую и писать $L_1 \leq L_2$.

Рассмотрим теперь ряд важных классов, находящихся за пределами {\bf NP}.
Для произвольной алгоритмической проблемы ${\mathcal A}$ через $\#{\mathcal A}$
будем обозначать проблему, требующую по данному входу проблемы ${\mathcal A}$
найти количество решений проблемы ${\mathcal A}$ на этом входе.
Для произвольных исходных данных $x$ и
произвольной недетерминированной машины Тьюринга $T$ через $\#acc_T(x)$ и $\#rej_T(x)$
мы будем обозначать
количество допускающих и отвергающих вход $x$ вычислений, соответственно.
Через {\bf GapP} мы будем обозначать класс всех функций $f$, для которых существует
недетерминированная машина Тьюринга $T$ такая, что равенство
$f(x)=\#acc_T(x)-\#rej_T(x)$ выполняется для всех $x$.
Следуя \cite{Spakowski__Thakur__2005,Ogiwara__Hemachandra__1993},
будем полагать, что
\begin{itemize}
\item {\bf PP}~--- класс языков $L \subseteq \Sigma^{\ast}$, для которых существует функция $f \in {\bf GapP}$ такая, что
$$x \in L \Leftrightarrow f(x)> 0$$
для любого $x \in \Sigma^{\ast}$ \cite{Gill__1977,Simon__1975};
\item {\bf Mod}$_k${\bf P}~--- класс языков $L \subseteq \Sigma^{\ast}$, для которых существует функция $f \in {\bf GapP}$ такая, что
$$x \in L \Leftrightarrow f(x)\not\equiv 0 \mod k$$
для любого $x \in \Sigma^{\ast}$ \cite{Beigel__Gill__1992,Cai__Hemachandra__1990,Hertrampf__1990};
\item $\oplus{\bf P} = {\bf Mod}_k{\bf P}$ \cite{Goldschlager__Parberry__1986,Papadimitriou__Zachos__1983};
\item {\bf SPP}~--- класс языков $L \subseteq \Sigma^{\ast}$, для которых существует функция $f \in {\bf GapP}$ такая, что
$$x \in L \Rightarrow f(x)=1,$$
$$x \notin L \Rightarrow f(x)=0$$
для любого $x \in \Sigma^{\ast}$ \cite{Fenner__Fortnow__1994};
\item {\bf C$_=$P}~--- класс языков $L \subseteq \Sigma^{\ast}$, для которых существует функция $f \in {\bf GapP}$ такая, что
$$x \in L \Leftrightarrow f(x)= 0$$
для любого $x \in \Sigma^{\ast}$  \cite{Simon__1975,Wagner__1986};
\item {\bf WPP}~--- класс языков $L \subseteq \Sigma^{\ast}$, для которых существуют функции $f \in {\bf GapP}$ и
$g \in {\bf FP}$ такие, что для любого $x \in \Sigma^{\ast}$ выполняются соотношения
$$x \in L \Rightarrow f(x)=g(x),$$
$$x \notin L \Rightarrow f(x)=0$$
и  значение функции $g(x)$ отлично от нуля \cite{Fenner__Fortnow__1994}.
\end{itemize}
Заметим, что для этих классов известны следующие соотношения \cite{Spakowski__Thakur__2005,Rao__Rothe__1994}:
$${\bf P} \subseteq {\bf SPP} \subseteq {\bf WPP} \subseteq {\bf C\hbox{$_=$}P} \subseteq {\bf PP},$$
$${\bf SPP} \subseteq \oplus{\bf P} \subseteq {\bf Mod}_k{\bf P},$$
$${\bf co-NP} \subseteq {\bf C\hbox{$_=$}P},$$
$${\bf NP} \subseteq {\bf co-C\hbox{$_=$}P},$$
$${\bf WPP} \subseteq {\bf co-C\hbox{$_=$}P},$$
где класс {\bf co-NP} является дополнением класса {\bf NP}, а {\bf co-C\hbox{$_=$}P} обозначает дополнение
класса {\bf C\hbox{$_=$}P}.

Следуя \cite{Valiant__1979}, подсчитывающей машиной Тьюринга мы будем называть
недетерминированную машину Тьюринга $T$ с дополнительной лентой,
предназначенной для печати в двоичном виде значения функции $\#acc_T(x)$.
Обозначим через $t(n)$ максимальное время допустимого вычисления на входах, размер которых
не превосходит $n$.
Будем предполагать, что подсчитывающая машина Тьюринга в худшем случае имеет
сложность по времени $t(n)$. Соответственно, трудоемкость генерации
значения функции $\#acc_T(x)$ на дополнительной ленте не учитывается.
Обозначим через \#{\bf P} класс, состоящий из всех функций, которые могут быть вычислены
подсчитывающей машиной Тьюринга за полиномиальное время \cite{Valiant__1979}.

Как и для большинства других классов вычислительной сложности, доказательство \#{\bf P}-трудности
некоторой алгоритмической проблемы $A$ обычно заключается в сведении к ней некоторой
\#{\bf P}-полной проблемы $B$.
Однако сводимость должна обеспечивать сохранение количества решений.
Для произвольного входа $I$ алгоритмической проблемы $\Pi$ обозначим через
$\#I$ количество решений проблемы $\Pi$ на входе $I$.

Если существует полиномиально вычислимая функция
$f_R$ такая, что
имеет место равенство
$\# I_1 = f_R(I_1) \# I_2$
для любых входов
$I_1 \in \Pi_1$
и
$I_2 \in \Pi_2$,
удовлетворяющих соотношению
$R(I_1)=I_2$,
то полиномиальную сводимость
$R$ проблемы $\Pi_1$ к проблеме $\Pi_2$ будем называть слабо экономной \cite{Barbanchon__2004}.
Если для любых входов
$I_1 \in \Pi_1$
и
$I_2 \in \Pi_2$
таких, что
$R(I_1)=I_2$,
имеет место равенство
$\# I_1 = \# I_2$,
то полиномиальная сводимость
$R$ проблемы $\Pi_1$ к проблеме $\Pi_2$ называется экономной \cite{Barbanchon__2004}.
Мы будем использовать обозначение $\Pi_1 \leq_P \Pi_2$ для экономной сводимости и $\Pi_1 \leq_W \Pi_2$ для слабо экономной сводимости.

По произвольной функции $\#{\mathcal A} : \Sigma^{\ast} \rightarrow {\Bbb N}$ из класса \#{\bf P}, следуя \cite{Bakali__Chalki__2024},
определим следующие алгоритмические проблемы.
\begin{itemize}
\item $\oplus{\mathcal A}$~--- по произвольному входу $x \in \Sigma^{\ast}$ выяснить, является ли значение $\#{\mathcal A}(x)$ нечетным.
\item ${\bf Mod}_k{\mathcal A}$~--- по произвольному входу $x \in \Sigma^{\ast}$ выяснить, верно ли, что $\#{\mathcal A}(x)\not\equiv 0 \mod k$.
\item ${\bf Diff}{\mathcal A}_{=0}$~--- по произвольному входу $(x,y) \in \Sigma^{\ast} \times \Sigma^{\ast}$ выяснить, верно ли, что $\#{\mathcal A}(x)= \#{\mathcal A}(y)$.
\item ${\bf Diff}{\mathcal A}_{>0}$~--- по произвольному входу $(x,y) \in \Sigma^{\ast} \times \Sigma^{\ast}$ выяснить, верно ли, что $\#{\mathcal A}(x)> \#{\mathcal A}(y)$.
\item ${\bf Diff}{\mathcal A}_{=1}$~--- по произвольному входу $(x,y) \in \Sigma^{\ast} \times \Sigma^{\ast}$ в предположении, что
    $$(x,y) \in I_{yes} \cup I_{no},$$
    где
    $$I_{yes} = \{ (x,y) \mid \#{\mathcal A}(x)= \#{\mathcal A}(y)+1\},$$
    $$I_{no} = \{ (x,y) \mid \#{\mathcal A}(x)= \#{\mathcal A}(y)\},$$
    выяснить, верно ли, что
    $$(x,y) \in I_{yes}.$$
\item ${\bf Diff}{\mathcal A}_{=g}$~--- по произвольному входу $(x,y,k) \in \Sigma^{\ast} \times \Sigma^{\ast} \times {\Bbb N}$ в предположении, что
    $$(x,y,k) \in I_{yes} \cup I_{no},$$
    где
    $$I_{yes} = \{ (x,y,k) \mid \#{\mathcal A}(x)= \#{\mathcal A}(y)+k\},$$
    $$I_{no} = \{ (x,y,k) \mid \#{\mathcal A}(x)= \#{\mathcal A}(y)\},$$
    выяснить, верно ли, что
    $$(x,y,k) \in I_{yes}.$$
\end{itemize}
Согласно \cite{Bakali__Chalki__2024}, если проблема $\#{\mathcal A}$ является \#{\bf P}-полной относительно экономной сводимости, то
проблемы $\oplus{\mathcal A}$, ${\bf Mod}_k{\mathcal A}$, ${\bf Diff}{\mathcal A}_{=0}$, ${\bf Diff}{\mathcal A}_{>0}$,
${\bf Diff}{\mathcal A}_{=1}$,
${\bf Diff}{\mathcal A}_{=g}$ являются полными для классов
$\oplus{\bf P}$, {\bf Mod}$_k${\bf P}, {\bf C$_=$P}, {\bf PP}, {\bf SPP}, {\bf WPP}, соответственно.

\section{Экономная сводимость для {\sc 3SAT}}
Доказательство теоремы Кука \cite{Cook__1971}, которое устанавливает {\bf NP}-труд\-ность проблемы {\sc SAT},
является первым примером непосредственной интерпретации машины Тьюринга при доказательстве
{\bf NP}-полноты алгоритмической проблемы. Такой подход используется весьма редко.
Для большинства алгоритмических проблем доказательство трудности осуществляется
демонстрацией полиномиальной сводимости от {\sc SAT} или от проблемы, для которой сводимость
от {\sc SAT} уже известна. 

Следует отметить, что в работе \cite{Cook__1971} булева функция
$f(x_1,x_2, \dots , x_n) $ строится так, что каждому допустимому вычислению машины Тьюринга
соответствует ровно один набор значений переменных, для которого $f(x_1,x_2, \dots , x_m) =1$.
Следуя рассуждениям Кука, представленным в работе \cite{Cook__1971}, несложно убедиться в том,
что проблема \#{\sc SAT} является \#{\bf P}-полной относительно экономной сводимости.

Легко понять, что в книге \cite{Garey__Johnson__1979} представлена формулировка проблемы 3-выполнимости,
которая более удобна для использования при доказательстве трудности различных проблем.
Проблема {\sc $\leq$3SAT} предполагает, что в функции $f(x_1,x_2, \dots , x_n)$
нет дизъюнкций более трех литералов, а у проблемы {\sc 3SAT} нет и дизъюнкций более трех литералов,
и дизъюнкций менее трех литералов. Однако, полиномиальная сводимость, построенная в \cite{Karp__1972},
является экономной, а полиномиальная сводимость, предложенная в \cite{Garey__Johnson__1979},
экономной не является.
В самом деле, доказательство в \cite{Karp__1972} основано на замене произвольной дизъюнкции литералов
\begin{equation}
\label{e_karp__01}
\sigma_1 \vee \sigma_2 \vee \dots \vee \sigma_m,
\end{equation}
где $m>3$, формулой
\begin{eqnarray}
\label{e_karp__02}
&(\sigma_1 \vee \sigma_2 \vee u_1) \wedge (\sigma_3 \vee \sigma_4 \vee \dots \vee \sigma_m  \vee \neg u_1)
\wedge
\nonumber \\
&(\neg \sigma_3 \vee  u_1) \wedge (\neg \sigma_4 \vee  u_1) \wedge \dots \wedge (\neg \sigma_m \vee  u_1),
\end{eqnarray}
где $u_1$ является новой переменной. Очевидно, что формула (\ref{e_karp__02}) выполняется
тогда и только тогда, когда выполняются все ее конъюнкты.
Если для некоторого
$3 \leq i \leq m$ имеет место равенство $\sigma_i =1$, то для выполнимости
\begin{equation}
\label{e_karp__03}
(\neg \sigma_3 \vee  u_1) \wedge (\neg \sigma_4 \vee  u_1) \wedge \dots \wedge (\neg \sigma_m \vee  u_1),
\end{equation}
необходимо, чтобы $u_1=1$.
Если для любого
$3 \leq i \leq m$ имеет место равенство $\sigma_i =0$, то для выполнимости
\begin{equation}
\label{e_karp__04}
\sigma_3 \vee \sigma_4 \vee \dots \vee \sigma_m  \vee \neg u_1,
\end{equation}
необходимо, чтобы $u_1=0$.
Таким образом, формулы (\ref{e_karp__03}) и (\ref{e_karp__04}) обеспечивают
единственность решения (\ref{e_karp__02}) для каждого решения (\ref{e_karp__01}).
Несложно убедиться в том, что отсюда вытекает, что сводимость, которую в работе \cite{Karp__1972} предложил Карп,
является экономной сводимостью от проблемы {\sc SAT} к проблеме {\sc $\leq$3SAT}.
Соответственно, проблема \#{\sc $\leq$3SAT} является \#{\bf P}-полной относительно экономной сводимости.
С другой стороны, замена дизъюнкции литералов
\begin{equation}
\label{e_karp__05}
\sigma_1 \vee \sigma_2
\end{equation}
формулой
\begin{equation}
\label{e_karp__06}
(\sigma_1 \vee \sigma_2 \vee u_1) \wedge (\sigma_1 \vee \sigma_2 \vee \neg u_1),
\end{equation}
предлагаемая в \cite{Garey__Johnson__1979}, вообще говоря, позволяет для каждого решения (\ref{e_karp__05})
получить два решения (\ref{e_karp__06}). Поэтому сводимость, предложенная в книге \cite{Garey__Johnson__1979},
экономной не является. Во многих случаях это делает сводимость, предложенную в книге \cite{Garey__Johnson__1979},
неудобной для дальнейшего использования. Учитывая то, что проблема {\sc 3SAT} является наиболее популярной при доказательстве
трудности, естественно стремиться получить для нее не только наиболее эффективную сводимость, но и максимально выразительную
формулировку, поскольку во многих случаях свойства, которые могли бы быть сформулированы для проблемы {\sc 3SAT},
приходится многократно воспроизводить при построении сводимостей
(см., например,
\cite{Lichtenstein__1982,Moret__1988}).

В формулировке {\sc $\leq$3SAT} можно предполагать, что в одной и той же
дизъюнкции литерал можно использовать, вообще говоря, несколько раз. Тогда мы легко получим {\sc 3SAT}
и сохраним экономность сводимости.
Например, дизъюнкции $u$ и $u \vee v$
можно заменять на дизъюнкции
$u \vee u \vee u$ и $u \vee v \vee v$,
соответственно.
Однако допущение многократного использования литералов
при доказательстве трудности проблем, например, для графов может привести к появлению кратных вершин и ребер.
Разбор соответствующих случаев может сделать доказательства существенно более громоздкими.
Аналогичные проблемы возникнут и для многих других прикладных задач.

Несложной модификацией доказательства, предложенного в \cite{Garey__Johnson__1979},
можно сохранить экономность сводимости без использования повторяющихся литералов.
В частности, вместо локальной замены, предложенной в \cite{Garey__Johnson__1979},
можно использовать локальную замену следующего вида.
Произвольная дизъюнкция $\sigma_1$ заменяется на
формулу
\begin{eqnarray}
\label{e_karp__07}
&(\sigma_1 \vee u_1 \vee u_2)
\wedge (\neg u_1 \vee \neg u_2 \vee \neg u_3)
\wedge
\nonumber \\
&(u_1 \vee \neg u_2 \vee \neg u_3)
\wedge (\neg u_1 \vee u_2 \vee \neg u_3)
\wedge
\nonumber \\
&(\neg u_1 \vee \neg u_2 \vee u_3)
\wedge (u_1 \vee u_2 \vee \neg u_3)
\wedge
\nonumber \\
&(u_1 \vee \neg u_2 \vee u_3)
\wedge (\neg u_1 \vee u_2 \vee u_3),
\end{eqnarray}
дизъюнкция $\sigma_1 \vee \sigma_2$ заменяется на
формулу
\begin{eqnarray}
\label{e_karp__08}
&(\sigma_1 \vee \sigma_2 \vee u_1)
\wedge (\neg u_1 \vee \neg u_2 \vee \neg u_3)
\wedge
\nonumber \\
&(u_1 \vee \neg u_2 \vee \neg u_3)
\wedge (\neg u_1 \vee u_2 \vee \neg u_3)
\wedge
\nonumber \\
&(\neg u_1 \vee \neg u_2 \vee u_3)
\wedge (u_1 \vee u_2 \vee \neg u_3)
\wedge
\nonumber \\
&(u_1 \vee \neg u_2 \vee u_3)
\wedge (\neg u_1 \vee u_2 \vee u_3),
\end{eqnarray}
дизъюнкция (\ref{e_karp__01}) заменяется на
формулу
\begin{eqnarray}
\label{e_karp__09}
&(\sigma_1 \vee \sigma_2 \vee u_1) \wedge (\sigma_3 \vee \sigma_4 \vee \dots \vee \sigma_m  \vee \neg u_1)
\wedge
\nonumber \\
&\wedge_{i \not= j, m \geq i>2, m \geq j>2}
(\neg \sigma_i \vee  \neg \sigma_j \vee  u_1)
\wedge
\nonumber \\
&\wedge_{i \not= j, m \geq i>2, m \geq j>2}
(\neg \sigma_i \vee  \sigma_j \vee  u_1).
\end{eqnarray}

Заметим, что формула
\begin{eqnarray}
\label{e_karp__10}
&(\neg u_1 \vee \neg u_2 \vee \neg u_3)
\wedge (u_1 \vee \neg u_2 \vee \neg u_3)
\wedge
\nonumber \\
&(\neg u_1 \vee u_2 \vee \neg u_3)
\wedge (\neg u_1 \vee \neg u_2 \vee u_3)
\wedge
\nonumber \\
&(u_1 \vee u_2 \vee \neg u_3)
\wedge (u_1 \vee \neg u_2 \vee u_3)
\wedge
\nonumber \\
&(\neg u_1 \vee u_2 \vee u_3)
\end{eqnarray}
выполняется тогда и только тогда, когда
\begin{equation}
\label{e_karp__11}
u_1=u_2=u_3=0.
\end{equation}
Выполнимость формулы (\ref{e_karp__07}) или (\ref{e_karp__08})
требует выполнимости формулы (\ref{e_karp__10}).
Поэтому выполнимость формулы (\ref{e_karp__07})
равносильна выполнимости дизъюнкции $\sigma_1$ и системы равенств
(\ref{e_karp__11}).
Аналогично выполнимость формулы (\ref{e_karp__08})
равносильна выполнимости дизъюнкции $\sigma_1 \vee \sigma_2$ и системы равенств
(\ref{e_karp__11}).
Поэтому замена дизъюнкций $\sigma_1$ и  $\sigma_1 \vee \sigma_2$ на формулы
(\ref{e_karp__07}) и (\ref{e_karp__08}), соответственно, не влияет на количество решений.
Более того, легко понять, что для всех дизъюнкций вида $\sigma_1$ и  $\sigma_1 \vee \sigma_2$
мы можем использовать единую тройку переменных $u_1$, $u_2$ и $u_3$.
Выполнимость формулы (\ref{e_karp__09}) требует выполнимости
формул (\ref{e_karp__04}) и
\begin{eqnarray}
\label{e_karp__12}
&\wedge_{i \not= j, m \geq i>2, m \geq j>2}
(\neg \sigma_i \vee  \neg \sigma_j \vee  u_1)
\wedge
\nonumber \\
&\wedge_{i \not= j, m \geq i>2, m \geq j>2}
(\neg \sigma_i \vee  \sigma_j \vee  u_1).
\end{eqnarray}
Если для некоторого
$3 \leq i \leq m$ имеет место равенство $\sigma_i =1$, то для выполнимости
формулы (\ref{e_karp__12})
необходимо, чтобы $u_1=1$.
Если для любого
$3 \leq i \leq m$ имеет место равенство $\sigma_i =0$, то для выполнимости
формулы (\ref{e_karp__04})
необходимо, чтобы $u_1=0$.
Таким образом, формулы (\ref{e_karp__04}) и (\ref{e_karp__12}) обеспечивают
единственность решения (\ref{e_karp__09}) для каждого решения (\ref{e_karp__01}).

Таким образом, мы получили экономную сводимость от проблемы {\sc SAT} к проблеме {\sc 3SAT}.
Соответственно, проблема \#{\sc 3SAT} является \#{\bf P}-полной относительно экономной сводимости.
При этом мы можем предполагать, что в каждой дизъюнкции три литерала, соответствующие трем различным
переменным.


\section{Экономная сводимость для {\sc C-3SAT}}
\begin{theorem}
\label{TT_01}
$\hbox{{\sc 3SAT}} \leq_P \hbox{{\sc C-3SAT}}$.
\end{theorem}

\begin{proof}
Если на входе у проблемы {\sc 3SAT} дизъюнктивно-\-связ\-ная булева функция, то ничего делать не нужно.
Поэтому без ограничения общности можно предполагать, что булева функция на входе у проблемы {\sc 3SAT} дизъюнктивно-связной
не является.

Рассмотрим произвольную булеву функцию $f(x_1,x_2, \dots , x_n)$ вида (\ref{f0}), где для любого $i$,
$1\leq i \leq m$, функция $C_i$ имеет вид (\ref{f1}) и является дизъюнкцией ровно трех литералов.
Обозначим через $X$ множество всевозможных пар дизъюнкций $(C_i,C_j)$, $1 \leq i \leq m$, $1 \leq j \leq m$,
не имеющих общих переменных.
В функции $f(x_1,x_2, \dots , x_n)$ произвольную формулу
\begin{eqnarray}
\label{ee_01}
& C_i \wedge C_j,
\end{eqnarray}
где $(C_i,C_j) \in X$,
заменим на формулу
\begin{eqnarray}
\label{ee_02}
& C_i \wedge C_j
\wedge
\nonumber \\
&(y_1 \vee u_{i,3} \vee u_{j,3})
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee y_3)
\wedge (y_1 \vee \neg y_2 \vee \neg y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee \neg y_3)
\wedge (\neg y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee \neg y_3)
\wedge (y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee y_3),
\end{eqnarray}
где $y_1$, $y_2$, $y_3$ являются новыми переменными.
Получим булеву функцию
\begin{eqnarray}
\label{ee_03}
& g(x_1,x_2, \dots , x_n,y_1,y_2,y_3) =
\nonumber \\
& f(x_1,x_2, \dots , x_n)
\wedge
\nonumber \\
&(y_1 \vee u_{i,3} \vee u_{j,3})
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee y_3)
\wedge (y_1 \vee \neg y_2 \vee \neg y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee \neg y_3)
\wedge (\neg y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee \neg y_3)
\wedge (y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee y_3).
\end{eqnarray}

Предположим, что булева функция
$f(x_1,x_2, \dots , x_n)$
выполняется на наборе
$t_1,t_2, \dots , t_n$.
Заметим, что формула
\begin{eqnarray}
\label{ee_04}
&(y_1 \vee y_2 \vee y_3)
\wedge (y_1 \vee \neg y_2 \vee \neg y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee \neg y_3)
\wedge (\neg y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee \neg y_3)
\wedge (y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee y_3)
\end{eqnarray}
выполняется тогда и только тогда, когда
\begin{equation}
\label{ee_05}
y_1=y_2=y_3=1.
\end{equation}
Поэтому выполняется равенство
$$g(t_1,t_2, \dots , t_n,1,1,1) = 1$$
и для любых $a_1$, $a_2$, $a_3$
таких, что
$$a_1 \wedge a_2 \wedge a_3 =0,$$
имеет место равенство
$$g(t_1,t_2, \dots , t_n,a_1,a_2,a_3) = 0.$$
Следовательно, из выполнимости функции $f$ вытекает выполнимость функции $g$.
При этом каждому набору значений переменных
$t_1,t_2, \dots , t_n$,
на котором выполняется функция $f$,
соответствует единственный набор значений переменных
$t_1,t_2, \dots , t_n,1,1,1$,
на котором выполняется функция $g$.

Допустим теперь, что функция $g$ выполняется на
некотором наборе значений переменных
\begin{equation}
\label{ee_06}
t_1,t_2, \dots , t_{n+3}
\end{equation}
Поскольку формула (\ref{ee_04})
выполняется только при условии (\ref{ee_05}),
набор (\ref{ee_06}) должен иметь вид
\begin{equation}
\label{ee_07}
t_1,t_2, \dots , t_{n},1,1,1.
\end{equation}
Подставив набор (\ref{ee_07}) в соотношение (\ref{ee_03}), получим
$$g(t_1,t_2, \dots , t_n,1,1,1) = f(t_1,t_2, \dots , t_n).$$
Следовательно, функция $f$ выполняется на наборе
$t_1,t_2, \dots , t_n$.

Таким образом, замена формулы (\ref{ee_01}) на формулу (\ref{ee_02})
сохраняет выполнимость и количество решений.
Несложно убедиться в том, что, осуществив замену формулы вида (\ref{ee_01}) на формулу вида (\ref{ee_02})
для каждой пары $(C_i,C_j) \in X$, мы сохраним выполнимость и количество решений.
Более того, легко понять, что для всех пар $(C_i,C_j) \in X$ мы можем использовать
одни и те же переменные $y_1$, $y_2$, $y_3$.

Рассмотрим граф $G_g=(V_g,E_g)$.
По определению
$$V_g = V_f \cup \{ (y_1 \vee u_{i,3} \vee u_{j,3}), (y_1 \vee y_2 \vee y_3),$$
$$(y_1 \vee \neg y_2 \vee \neg y_3), (\neg y_1 \vee y_2 \vee \neg y_3),$$
$$(\neg y_1 \vee \neg y_2 \vee y_3), (y_1 \vee y_2 \vee \neg y_3),$$
$$(y_1 \vee \neg y_2 \vee y_3), (\neg y_1 \vee y_2 \vee y_3) \}.$$
Соответственно, каждая замена формулы (\ref{ee_01}) на формулу (\ref{ee_02})
добавляет новые вершины, которые смежны между собой, поскольку каждая из новых
дизъюнкций содержит переменную $y_1$.
После замены формулы вида (\ref{ee_01}) на формулу вида (\ref{ee_02})
для каждой пары $(C_i,C_j) \in X$
все вершины множества $V_f$ попадут в одну компоненту связности,
поскольку для любой пары дизъюнкций $(C_i,C_j)$, $1 \leq i \leq m$, $1 \leq j \leq m$,
либо вершины $C_i$ и $C_j$ являются смежными,
либо существует путь
$$(C_i, (y_1 \vee u_{i,3} \vee u_{j,3}), C_j).$$
Каждая группа новых вершин, соответствующая замене формулы вида (\ref{ee_01}) на формулу вида (\ref{ee_02}),
образует полный подграф, все вершины которого принадлежат той же компоненте связности, что и $V_f$,
благодаря ребрам
$(C_i, (y_1 \vee u_{i,3} \vee u_{j,3}))$
и
$((y_1 \vee u_{i,3} \vee u_{j,3}), C_j)$.
Таким образом, замена формулы вида (\ref{ee_01}) на формулу вида (\ref{ee_02})
для каждой пары $(C_i,C_j) \in X$ позволяет получить дизъюнктивно-связную булеву функцию.
Для завершения доказательства теоремы осталось заметить, что замена формулы вида (\ref{ee_01}) на формулу вида (\ref{ee_02}) добавляет в булеву функцию
только дизъюнкции, состоящие ровно из трех литералов.
\end{proof}

Заметим, что проблема {\sc C-3SAT} является частным случаем проблем
{\sc C-$\leq$3SAT} и {\sc C-SAT}. Поэтому из соотношения $\hbox{{\sc 3SAT}} \leq_P \hbox{{\sc C-3SAT}}$
следуют соотношения $\hbox{{\sc 3SAT}} \leq_P \hbox{{\sc C-SAT}}$ и $\hbox{{\sc 3SAT}} \leq_P \hbox{{\sc C-$\leq$3SAT}}$.
Отсюда вытекает следующее утверждение.

\begin{corollary}
\label{CC_01}
Проблемы \#{\sc C-3SAT}, \#{\sc C-$\leq$3SAT} и \#{\sc C-SAT} являются \#{\bf P}-полными относительно экономной сводимости.
\end{corollary}

Рассмотрим теперь следующую проблему.

{\sc Проблема 3-выполнимости сильно дизъюнктивно-связной булевой функции (SC-3SAT).}

{\sc Дано:} {\it Булева функция
$f(x_1,x_2, \dots , x_n) =\wedge_{i=1}^m C_i$ такая, что граф $D_f$ является связным и для любого $i$,
$1\leq i \leq m$, функция $C_i$ является дизъюнкцией ровно трех литералов.}

{\sc Вопрос:} {\it Существует ли набор значений переменных $x_j$,
$x_j \in \{ 0,1 \}$, $1\leq j \leq m$, такой, что выполняется равенство $f(x_1,x_2, \dots , x_m) =1$?}

\begin{theorem}
\label{TT_02}
$\hbox{{\sc 3SAT}} \leq_P \hbox{{\sc SC-3SAT}}$.
\end{theorem}

\begin{proof}
Если на входе у проблемы {\sc 3SAT} сильно дизъюнктив\-но-связная булева функция, то ничего менять не требуется.
Поэтому мы можем предполагать, что булева функция на входе у проблемы {\sc 3SAT} не является сильно дизъюнктивно-связной.

Для произвольной булевой функции $f(x_1,x_2, \dots , x_n)$ вида (\ref{f0}), где для любого $i$,
$1\leq i \leq m$, функция $C_i$ имеет вид (\ref{f1}) и является дизъюнкцией ровно трех литералов,
рассмотрим  множество $X$ всевозможных пар дизъюнкций $(C_i,C_j)$, $1 \leq i \leq m$, $1 \leq j \leq m$,
не имеющих общих литералов.
При замене формулы вида (\ref{ee_01}) на формулу вида (\ref{ee_02})
из функции $f$ мы получаем функцию $g$ вида (\ref{ee_03}).
Легко понять, что граф $D_g$
содержит пути
$$C_i, (y_1 \vee u_{i,3} \vee u_{j,3}), C_j),$$
$$((y_1 \vee u_{i,3} \vee u_{j,3}), (y_1 \vee y_2 \vee y_3),$$
$$(y_1 \vee \neg y_2 \vee \neg y_3), (\neg y_1 \vee y_2 \vee \neg y_3),$$
$$(\neg y_1 \vee \neg y_2 \vee y_3), (y_1 \vee \neg y_2 \vee y_3),$$
$$(\neg y_1 \vee y_2 \vee y_3), (y_1 \vee y_2 \vee \neg y_3)).$$
Поэтому для произвольной пары $(C_i,C_j)$ из множества $X$ замена формулы (\ref{ee_01}) на формулу (\ref{ee_02})
обеспечит сильную дизъюнктивную связность булевой функции.
Однако замена формулы вида (\ref{ee_01}) на формулу вида (\ref{ee_02})
может привести к появлению дизъюнкции, содержащей литералы, соответствующие одной и той же переменной.
Мы предполагаем, что в функции $f(x_1,x_2, \dots , x_n)$ каждая дизъюнкция содержит литералы, соответствующие трем различным
переменным.
Поэтому для произвольной пары дизъюнкций $(C_i,C_j)$ мы всегда можем выбрать литералы
$u_{i,k}$ и $u_{j,p}$, соответствующие различным переменным.
Соответственно, замена произвольной формулы (\ref{ee_01}) на формулу
\begin{eqnarray}
\label{ee_08}
& C_i \wedge C_j
\wedge
\nonumber \\
&(y_1 \vee u_{i,k} \vee u_{j,p})
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee y_3)
\wedge (y_1 \vee \neg y_2 \vee \neg y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee \neg y_3)
\wedge (\neg y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee \neg y_3)
\wedge (y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee y_3)
\end{eqnarray}
не приведет к появлению дизъюнкции, содержащей литералы, соответствующие одной и той же переменной.
По аналогии с доказательством теоремы \ref{TT_01} мы можем убедиться в том, что
использование замены формулы вида (\ref{ee_01}) на формулу вида (\ref{ee_08}) позволяет обеспечить
требуемую сводимость.
\end{proof}

Непосредственно из теоремы \ref{TT_02} получаем следующее утверждение.

\begin{corollary}
\label{CC_02}
Проблема \#{\sc SC-3SAT} является \#{\bf P}-полной относительно экономной сводимости.
\end{corollary}

Заметим, что при доказательстве теоремы \ref{TT_02} мы пользовались тем, что
каждая дизъюнкция булевой функции проблемы {\sc 3SAT} содержит литералы, соответствующие трем различным
переменным, т.е. вырожденных дизъюнкций нет.
Однако различные прикладные задачи могут допускать использование вырожденных дизъюнкций.
В частности, это может возникать при случайной генерации булевых функций, маскировке криптографических данных,
совместном решении нескольких задач. В некоторых случаях может потребоваться изменить плотность булевой функции,
сохраняя имеющиеся вырожденные дизъюнкции, но не добавляя новых.
В частности, это может представлять интерес при разработке аппаратных вредоносных программ.
В этом случае для некоторой переменной $x$ пара дизъюнкций $(C_i,C_j)$
может принять вид $(x,\neg x)$ (совместная выполнимость такой пары дизъюнкций обеспечивается через провокацию отказа системы
и нарушение целостности данных). Для такой пары мы можем использовать замену на формулу
\begin{eqnarray}
& C_i \wedge C_j
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee x)
\wedge
(y_1 \vee y_2 \vee \neg x)
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee y_3)
\wedge (y_1 \vee \neg y_2 \vee \neg y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee \neg y_3)
\wedge (\neg y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(y_1 \vee y_2 \vee \neg y_3)
\wedge (y_1 \vee \neg y_2 \vee y_3)
\wedge
\nonumber \\
&(\neg y_1 \vee y_2 \vee y_3).
\nonumber
\end{eqnarray}

\section{Планарная дизъюнктивно-связная выполнимость}
В работе \cite{Lichtenstein__1982} было введено понятие планарной булевой функции и доказана {\bf NP}-полнота
планарной проблемы 3-выполнимости.
В последующих исследованиях была доказана вычислительная трудность для многих планарных вариантов проблемы выполнимости
\cite{Barbanchon__2004,Dyer__Frieze__1986,Hunt__Marathe__1998}.
Однако в этих работах использовался подход к построению графа, который отличается от рассматриваемого в данной работе.
В этом разделе мы рассмотрим проблему выполнимости для планарных дизъюнктивно-связных булевых функций.

{\sc Проблема $\leq$3-выполнимости планарной дизъюнктивно-\-связ\-ной булевой функции (PC-$\leq$3SAT).}

{\sc Дано:} {\it Булева функция
$f(x_1,x_2, \dots , x_n) =\wedge_{i=1}^m C_i$ такая, что функция $C_i$, $1\leq i \leq m$,
является дизъюнкцией не более трех литералов и граф $G_f$ является планарным и связным.}

{\sc Вопрос:} {\it Существует ли набор значений переменных $x_j$,
$x_j \in \{ 0,1 \}$, $1\leq j \leq m$, такой, что выполняется равенство $f(x_1,x_2, \dots , x_m) =1$?}

\begin{theorem}
\label{TT_03}
$\hbox{{\sc 3SAT}} \leq_P \hbox{{\sc PC-$\leq$3SAT}}$.
\end{theorem}

\begin{proof}
Доказательство теоремы в существенной мере будет опираться на конструкцию, предложенную в работе \cite{Lichtenstein__1982},
и результаты работы \cite{Hunt__Marathe__1998}.
Рассмотрим булеву функцию
$f(x_1,x_2, \dots , x_n) =\wedge_{i=1}^m C_i$, где для любого $i$,
$1\leq i \leq m$, функция $C_i$ является дизъюнкцией ровно трех литералов.
Определим для функции $f$ граф $G(f)$ в соответствие с подходом, предложенным в работе \cite{Lichtenstein__1982}.
Пусть $G(f)=(V(f),E(f))$~--- граф, заданный множеством вершин $V(f)$ и множеством ребер $E(f)$, где
$$V(f) = \{ C_i \mid 1 \leq i \leq m \} \cup \{ x_j \mid 1 \leq j \leq n \},$$
$$E(f) = E_1 \cup E_2 \cup E_3  \cup E_4,$$
$$E_1 = \{ (C_i , x_j) \mid 1 \leq i \leq m, 1 \leq j \leq n, x_j \in C_i \},$$
$$E_2 = \{ (C_i , x_j) \mid 1 \leq i \leq m, 1 \leq j \leq n, \neg x_j \in C_i \},$$
$$E_3 = \{ (x_j , x_{j+1}) \mid 1 \leq j \leq n-1 \},$$
$$E_4 = \{ (x_n , x_1) \}.$$
Таким образом, все ребра графа $G(f)$, кроме простого цикла, образованного переменными, расположенными в естественном порядке,
соединяют некоторую дизъюнкцию с некоторой переменной.

В работе \cite{Lichtenstein__1982} предложен подход на основе локальной замены к преобразованию булевой
функции $f$ в некоторую булеву функцию $g$, имеющую планарный граф $G(g)$. Первый этап построения сводимости
$\hbox{{\sc 3SAT}} \leq_P \hbox{{\sc PC-$\leq$3SAT}}$
будет основан на этой конструкции.

Предполагается, что цикл, образованный переменными, изображается естественным образом. Вершины графа,
соответствующие дизъюнкциям, располагаются с внешней стороны цикла в произвольном порядке.
В частности, можно предполагать, что переменные и дизъюнкции располагаются на двух параллельных линиях.
Мы будем предполагать, что дизъюнкции соединяются с переменными отрезками прямых линий.
Легко понять, что мы можем предполагать, что пересекаться могут только ребра, каждое из которых смежно с некоторой дизъюнкцией.
При этом если какие-либо ребра пересекаются, то всегда найдется пара ребер
$(C_i,x_s)$ и $(C_j,x_t)$ такая, что
ребра $(C_i,x_s)$ и $(C_j,x_t)$ пересекаются в точке
${\mathcal W}$ и отрезки
$[{\mathcal W},x_s]$ и $[{\mathcal W},x_t]$
не имеют пересечений с ребрами.
На отрезках
$[C_i,{\mathcal W}]$ и $[C_j,{\mathcal W}]$
мы всегда можем расположить точки
${\mathcal U}$ и ${\mathcal V}$, соответственно, так,
что отрезки
$[{\mathcal U},{\mathcal W}]$ и $[{\mathcal V},{\mathcal W}]$
не имеют пересечений с ребрами.
Точки ${\mathcal U}$, ${\mathcal V}$ и ${\mathcal W}$
сделаем вершинами нового графа, полагая
$$G=(V,E),$$
$$V=V(f) \cup \{ {\mathcal U}, {\mathcal V}, {\mathcal W} \},$$
$$E= (E(f) \backslash \{ (C_i,x_s), (C_j,x_t) \} ) \cup$$
$$\{ (C_i,{\mathcal U}), (C_j,{\mathcal V}), ({\mathcal U},{\mathcal W}), ({\mathcal V},{\mathcal W}),
({\mathcal W},x_s), ({\mathcal W},x_t) \}.$$
После этого в конструкции, предложенной в работе \cite{Lichtenstein__1982},
подграф, порожденный множеством вершин
$$\{ x_s, x_t, {\mathcal U}, {\mathcal V}, {\mathcal W} \},$$
заменяется на планарный граф специального вида,
который смежен с оставшейся частью графа по вершинам
$$x_s, x_t, {\mathcal U}, {\mathcal V}.$$
Для того чтобы полученный граф сделать графом некоторой булевой функции,
конструкция, предложенная в работе \cite{Lichtenstein__1982},
предполагает ряд изменений в булевой функции $f$ и ряд переобозначений в самом графе.
Без ограничения общности можно предполагать, что
$C_i=u_{i,1} \vee u_{i,2} \vee u_{i,3}$,
где $u_{i,3} \in \{ x_s, \neg x_s \}$,
$C_j=u_{j,1} \vee u_{j,2} \vee u_{j,3}$,
где $u_{j,3} \in \{ x_t, \neg x_t \}$.
Обозначим вершины ${\mathcal U}$ и ${\mathcal V}$ через
$y_s$ и $y_t$, соответственно.
Если $C_i=u_{i,1} \vee u_{i,2} \vee x_s$, то заменим $C_i$ на
$C_i^{\prime}=u_{i,1} \vee u_{i,2} \vee y_s$.
Если $C_i=u_{i,1} \vee u_{i,2} \vee \neg x_s$, то заменим $C_i$ на
$C_i^{\prime}=u_{i,1} \vee u_{i,2} \vee \neg y_s$.
Если $C_j=u_{j,1} \vee u_{j,2} \vee x_t$, то заменим $C_j$ на
$C_j^{\prime}=u_{j,1} \vee u_{j,2} \vee y_t$.
Если $C_j=u_{j,1} \vee u_{j,2} \vee \neg x_t$, то заменим $C_j$ на
$C_j^{\prime}=u_{j,1} \vee u_{j,2} \vee \neg y_t$.
Объявим вершины $y_s$ и $y_t$ новыми вершинами переменных.
Кроме того, добавим в множество вершин переменных шесть внутренних
вершин планарного подграфа: $u_1, u_2, v_1, v_2, v_3, v_4$.
Модифицируем функцию $f$ при помощи замены подформулы
\begin{eqnarray}
\label{ee_09}
& C_i \wedge C_j
\end{eqnarray}
на подформулу
\begin{eqnarray}
\label{ee_10}
& C_i^{\prime} \wedge C_j^{\prime} \wedge
\nonumber \\
&          (\neg u_1 \vee \neg u_2 \vee v_1) \wedge
           (     u_1 \vee \neg v_1) \wedge
           (     u_2 \vee \neg v_1) \wedge
\nonumber \\
&          (\neg u_1 \vee      y_t \vee v_2) \wedge
           (     u_1 \vee \neg v_2) \wedge
           (\neg y_t \vee \neg v_2) \wedge
\nonumber \\
&          (     y_s \vee      y_t \vee v_3) \wedge
           (\neg y_s \vee \neg v_3) \wedge
           (\neg y_t \vee \neg v_3) \wedge
\nonumber \\
&          (     y_s \vee \neg u_2 \vee v_4) \wedge
           (\neg y_s \vee \neg v_4) \wedge
           (     u_2 \vee \neg v_4) \wedge
\nonumber \\
& (v_1 \vee v_2 \vee v_3 \vee v_4) \wedge
\nonumber \\
& (\neg v_1 \vee \neg v_2) \wedge (\neg v_2 \vee \neg v_3)  \wedge
(\neg v_3 \vee \neg v_4)  \wedge (\neg v_1 \vee \neg v_4) \wedge
\nonumber \\
& ( u_1 \vee \neg x_s) \wedge (\neg u_1 \vee x_s)  \wedge
(u_2 \vee \neg x_t)  \wedge (\neg u_2 \vee x_t).
\end{eqnarray}
Таким образом, замена формулы вида (\ref{ee_09}) на формулу вида (\ref{ee_10})
заключается в замене двух дизъюнкций
$C_i$ и $C_j$
на их модифицированные варианты
$C_i^{\prime}$ и $C_j^{\prime}$
и добавлении 21 новой дизъюнкции.
При этом каждая из новых дизъюнкций соответствует одной из вершин планарного подграфа.
На этом построение планарного графа и соответствующей ему булевой функции для выделенного пересечения ребер полностью
завершается. В дальнейшем на первом этапе построения сводимости добавленный планарный подграф и вершины переменных $x_s$ и $x_t$
модифицироваться не будут. Изменения могут затронуть только вершины дизъюнкций $C_i$ и $C_j$.
Для завершения первого этапа построения сводимости нам необходимо последовательно перебрать все пересечения
ребер, осуществляя для каждого из них только что описанные действия. Корректность этой процедуры
обоснована в работе \cite{Lichtenstein__1982}. Следует отметить, что замена
формулы вида (\ref{ee_09}) на формулу вида (\ref{ee_10}) позволяет получить из функции $f$ некоторую
функцию $g$ такую, что функция $f$ выполняется тогда и только тогда, когда выполняется функция $g$,
причем замена
формулы вида (\ref{ee_09}) на формулу вида (\ref{ee_10}) сохраняет количество решений \cite{Lichtenstein__1982}.

До сих пор в тексте при доказательствах мы не упоминали логарифмическую память, поскольку
выполнимость соответствующих алгоритмов на логарифмической памяти была тривиальной. Теперь же нам следует
сделать ряд существенных замечаний, связанных с реализуемостью данной сводимости в логарифмической памяти.
\begin{itemize}
\item Как обычно, логарифмическая сводимость подразумевает, что у нас есть три области памяти. Одна из них изначально содержит исходные данные и предназначена только для чтения. Вторая изначально является пустой и предназначена только для записи результата. Кроме того, есть область памяти, которая изначально является пустой и доступна как для чтения, так и для записи, но размер этой области логарифмически ограничен размером исходных данных. Поэтому суперпозиция логарифмических
    сводимостей, вообще говоря, логарифмической сводимостью не является. Сводимость $\hbox{{\sc 3SAT}} \leq_P \hbox{{\sc PC-$\leq$3SAT}}$ мы описываем как цепь последовательных преобразований. Формально эта последовательность преобразований
    логарифмической сводимостью не будет, поскольку по завершении каждого этапа преобразований формируется новый граф,
    размер которого сравним с размером исходного графа и не позволяет новому графу полностью разместиться в
    логарифмической памяти. Поэтому, несмотря на последовательное изложение преобразований, мы предполагаем, что все этапы
    преобразования осуществляются одновременно, т.е. выбирается небольшая часть графа (пересечение ребер, вершина, планарный
    подграф, имеющий 31 вершину и т.д.), выбирается соответствующая часть булевой функции (которая тоже должна быть локальна), на выбранной части графа осуществляются все этапы преобразования, параллельно все этапы преобразования осуществляются
    на выбранной части булевой функции, полностью преобразованная часть графа и полностью преобразованная часть булевой
    функции перемещаются в память, предназначенную только для записи, только после этого в логарифмическую
    память загружаются новые локальные части графа и функции.
\item Логарифмическая память не позволяет хранить последовательность всех пересечений ребер в явном виде и отмечать в ней
    те пересечения, которые мы уже обработали. Поэтому мы предполагаем, что алгоритм использует естественную дискретизацию
    плоскости, определяемую начальным списком вершин и ребер графа и, соответственно, не требующую хранения в изменяемой памяти.
    Алгоритм пользуется естественным алгоритмом сканирования дискретизированной части плоскости, на которой размещается граф.
В соответствие с используемой дискретизацией алгоритм в изменяемой памяти хранит только координаты просматриваемого участка дискретизированной части плоскости.
\item В рамках первого этапа построения сводимости мы предполагали модификацию вершин дизъюнкций $C_i$ и $C_j$
для каждого пересечения ребер. Хранить эти изменения в явном виде в логарифмической памяти возможности нет.
Но в этом нет и необходимости, поскольку то, какие переменные входят в дизъюнкцию, полностью определяется тем,
с какими вершинами переменных смежна вершина дизъюнкции.
\item В рамках первого этапа построения сводимости предполагается, что пересечения ребер рассматриваются не все по порядку,
а лишь те, у которых отрезки $[{\mathcal W},x_s]$ и $[{\mathcal W},x_t]$ не имеют пересечений с ребрами. Заметим, что это,
вообще говоря, не создает нагрузку на память, поскольку, как нетрудно убедиться, плоскость можно дискретизировать
так, что все пересечения требуемого вида будут просматриваться первыми, а все остальные пересечения будут преобразованы к
требуемому виду к моменту их просмотра. В частности, для расположения, используемого в работе \cite{Lichtenstein__1982},
подходит прямоугольная дискретизация.
\item В ходе преобразований графа появляются новые вершины переменных. Их необходимо включить в цикл вершин переменных.
Конструкция, предложенная в работе \cite{Lichtenstein__1982}, позволяет изначально запланировать положение всех
вершин переменных в цикле, причем позиции в новом цикле как изначально существовавших вершин переменных, так и новых
вершин переменных не требуется хранить в памяти, поскольку они могут быть вычислены по начальному списку переменных и
дизъюнкций, который расположен в памяти, предназначенной только для чтения (см. \cite{Lichtenstein__1982}, рисунок 6).
\end{itemize}

Перейдем к второму этапу построения сведения. Заметим, что после первого этапа в булевой функции
появились дизъюнкции
\begin{eqnarray}
\label{ee_11}
& v_1 \vee v_2 \vee v_3 \vee v_4,
\end{eqnarray}
состоящие из четырех литералов.
Следуя \cite{Hunt__Marathe__1998},
заменим каждую подформулу вида (\ref{ee_11})
на подформулу
\begin{eqnarray}
\label{ee_12}
& (v_1 \vee v_2 \vee v_5) \wedge (\neg v_5 \vee v_3 \vee v_4).
\end{eqnarray}
Легко понять, что функция (\ref{ee_11}) выполняется тогда и только тогда,
когда выполняется функция (\ref{ee_12}).
Однако, в общем случае замена подформулы (\ref{ee_11}) на подформулу (\ref{ee_12})
не сохраняет количество решений.
В нашем случае каждая подформула вида (\ref{ee_11}) является подформулой соответствующей
формулы (\ref{ee_10}).
Поэтому для каждой формулы вида (\ref{ee_11}) существует соответствующая формула
$$(\neg v_1 \vee \neg v_2) \wedge (\neg v_2 \vee \neg v_3)  \wedge
(\neg v_3 \vee \neg v_4)  \wedge (\neg v_1 \vee \neg v_4),$$
выполнимость которой возможна лишь в том случае, когда
ровно одна из переменных $v_1, v_2, v_3, v_4$
является истинной.
Таким образом, хотя сама по себе замена подформулы (\ref{ee_11}) на подформулу (\ref{ee_12})
не обеспечивает сохранения количества решений, эта замена порождает замену подформулы
\begin{eqnarray}
\label{ee_13}
& (v_1 \vee v_2 \vee v_3 \vee v_4) \wedge
\nonumber \\
& (\neg v_1 \vee \neg v_2) \wedge (\neg v_2 \vee \neg v_3)  \wedge
(\neg v_3 \vee \neg v_4)  \wedge (\neg v_1 \vee \neg v_4)
\end{eqnarray}
на подформулу
\begin{eqnarray}
\label{ee_14}
& (v_1 \vee v_2 \vee v_5) \wedge (\neg v_5 \vee v_3 \vee v_4) \wedge
\nonumber \\
& (\neg v_1 \vee \neg v_2) \wedge (\neg v_2 \vee \neg v_3)  \wedge
(\neg v_3 \vee \neg v_4)  \wedge (\neg v_1 \vee \neg v_4),
\end{eqnarray}
которая гарантирует сохранение количества решений.
Замена подформулы (\ref{ee_13}) на подформулу (\ref{ee_14})
требует соответствуюшей модификации графа.
Необходимо удалить вершину дизъюнкции (\ref{ee_11}), добавить две вершины новых дизъюнкций
$v_1 \vee v_2 \vee v_5$ и $\neg v_5 \vee v_3 \vee v_4$,
вершину новой переменной $v_5$ и соответствующие определению ребра.
Полученный граф сохранит планарность \cite{Lichtenstein__1982}.
По завершении второго этапа построения сводимости
мы получаем некоторую булеву функцию
$h(z_1,z_2, \dots , z_p) =\wedge_{i=1}^q H_i$, где для любого $i$,
$1\leq i \leq q$, функция $H_i$ является дизъюнкцией не более трех литералов.
При этом функция $h$ выполняется тогда и только тогда, когда выполняется функция
$f$, замена $f$ на $h$ сохраняет количество решений, граф $G(h)$ является планарным \cite{Lichtenstein__1982,Hunt__Marathe__1998}.

Перейдем к третьему этапу. Этот этап будет заключительным. Поэтому все данные, прошедшие окончательное преобразование
и не требующиеся для дальнейших вычислений,
можно размещать в памяти, предназначенной только для записи.
Заметим, что для построения сводимости $\hbox{{\sc 3SAT}} \leq_P \hbox{{\sc PC-$\leq$3SAT}}$
нам достаточно по функции $f$ построить функцию $g$ с нужными нам свойствами.
В частности, функция $g$ должна иметь планарный граф $G_g$.
Однако строить сам граф $G_g$ необходимости нет.
Поэтому в память, предназначенную только для записи, мы будем размещать только информацию о функции
$g$. Вся информация о графе $G_g$ будет присутствовать в неявном виде в логарифмической памяти и памяти,
предназначенной только для чтения.

Основная цель третьего этапа~--- удаление из графа всех вершин переменных за счет введения новых вершин дизъюнкций.
Мы будем последовательно рассматривать вершины переменных в соответствие с зафиксированным порядком в цикле
вершин переменных.
Без ограничения общности для некоторого натурального числа $l \in {\Bbb N}$
мы можем обозначать вершины цикла вершин переменных $z_i$, $1 \leq i \leq l$,
предполагая, что сам цикл задается последовательностью
$z_1, z_2, \dots , z_l$. Соответственно, мы можем зафиксировать порядок обхода цикла,
предполагая, что вершины посещаются в порядке возрастания номеров.

Выполнение первых двух этапов построения сведения ведет к преобразованию начальной функции $f$
в некоторую функцию $h$ при помощи локальных замен
подформул вида (\ref{ee_09}) на подформулы вида
\begin{eqnarray}
\label{ee_15}
& C_i^{\prime} \wedge C_j^{\prime} \wedge
\nonumber \\
&          (\neg u_1 \vee \neg u_2 \vee v_1) \wedge
           (     u_1 \vee \neg v_1) \wedge
           (     u_2 \vee \neg v_1) \wedge
\nonumber \\
&          (\neg u_1 \vee      y_t \vee v_2) \wedge
           (     u_1 \vee \neg v_2) \wedge
           (\neg y_t \vee \neg v_2) \wedge
\nonumber \\
&          (     y_s \vee      y_t \vee v_3) \wedge
           (\neg y_s \vee \neg v_3) \wedge
           (\neg y_t \vee \neg v_3) \wedge
\nonumber \\
&          (     y_s \vee \neg u_2 \vee v_4) \wedge
           (\neg y_s \vee \neg v_4) \wedge
           (     u_2 \vee \neg v_4) \wedge
\nonumber \\
& (v_1 \vee v_2 \vee v_5) \wedge (\neg v_5 \vee v_3 \vee v_4) \wedge
\nonumber \\
& (\neg v_1 \vee \neg v_2) \wedge (\neg v_2 \vee \neg v_3)  \wedge
(\neg v_3 \vee \neg v_4)  \wedge (\neg v_1 \vee \neg v_4) \wedge
\nonumber \\
& ( u_1 \vee \neg x_s) \wedge (\neg u_1 \vee x_s)  \wedge
(u_2 \vee \neg x_t)  \wedge (\neg u_2 \vee x_t).
\end{eqnarray}
На третьем этапе к функции $h$ будут добавляться новые дизъюнкции, уже имеющиеся дизъюнкции будут подвергаться
лишь переименованию переменных.
Новые имена переменных будут иметь вид $z_{i,j}$, где $z_i$~--- вершина переменной, с которой смежна вершина дизъюнкции,
а индекс $j$ будет вычисляться по положению ребра на изображении графа.
Мы будем предполагать, что в окончательной булевой функции переменные будут упорядочены следующим образом:
$$i_1 < i_2 \Rightarrow z_{i_1,j_1} < z_{i_2,j_2},$$
$$i_1 = i_2, j_1 < j_2 \Rightarrow z_{i_1,j_1} < z_{i_2,j_2}.$$
Кроме того, будем предполагать, что в окончательной булевой функции дизъюнкции из $h$ будут содержать литералы в порядке возрастания
переменных.
Еще до начала преобразования на третьем этапе мы можем вычислить общее количество дизъюнкций в функции $h$,
количество литералов в каждой дизъюнкции, первые индексы переменных и то, является ли литерал переменной или отрицанием переменной.
Всю эту информацию мы можем передать в память, предназначенную только для записи.
Таким образом, осуществляя преобразование на третьем этапе, нам нужно будет передать в память, предназначенную только для записи,
только вторые индексы переменных функции $h$ и новые дизъюнкции.

Хотя с точки зрения логики последовательного преобразования третий этап является третьим, вычисление на логарифмической памяти
предполагает, что он должен вызываться первым и осуществляться как основа всего вычислительного процесса: начинаем обход цикла,
если у вершины нет пересекающихся ребер, то преобразуем ее и переходим к следующей вершине, если пересечения есть, то
осуществляем одну замену подформулы вида (\ref{ee_09}) на подформулу вида (\ref{ee_15}), последовательно преобразуем все новые
вершины цикла, передаем информацию в память, предназначенную только для записи, и лишь после этого делаем очередную  замену подформулы вида (\ref{ee_09}) на подформулу вида (\ref{ee_15}).

Перейдем непосредственно к описанию преобразования третьего этапа.
Каждая вершина переменной $z_i$ смежна ровно с двумя другими вершинами других переменных и, вообще говоря с несколькими вершинами
дизъюнкций. Без ограничения общности можно предполагать, что ребро
$(z_i, z_{i+1})$ направлено горизонтально влево от вершины $z_i$, ребро
$(z_i, z_{i-1})$ направлено горизонтально вправо от вершины $z_i$
(для $i=1$, $i-1=l$; для $i=l$, $i+1=1$).
Рассмотрим последовательность
$$(z_i, z_{i+1}), e_1, e_2, \dots , e_p, (z_i, z_{i-1}), e_{p+1}, e_{p+2}, \dots , e_{p+q}$$
всех ребер, одной из вершин которых является вершина $z_i$,
образованную перечислением ребер на изображении графа по часовой стрелке.
Преобразование, соответствующее вершине $z_i$, заключается в следующей последовательности
действий.
\begin{itemize}
\item Если вершина дизъюнкции является вершиной ребра $e_j$, то соответствующая переменная функции $h$ получает обозначение
$z_{i,j}$. Соответственно, после полного завершения третьего этапа все переменные, входящие в $h$, будут иметь в $h$
единственное вхождение.
\item Вычисленные вторые индексы переменных $z_{i,j}$ по мере их вычисления передаются в память, предназначенную только для записи.
\item В окончательную функцию добавляется следующая подформула, которая по мере вычисления дизъюнкций передается в память, предназначенную только для записи.
\end{itemize}
\begin{eqnarray}
\label{ee_16}
& (u_{i+1} \vee v_{i,1} \vee \neg z_{i,1}) \wedge
  (z_{i,1} \vee \neg z_{i,2}) \wedge
\nonumber \\
&  (z_{i,2} \vee \neg z_{i,3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p-1} \vee \neg z_{i,p}) \wedge
  (z_{i,p} \vee \neg v_{i,2}) \wedge
\nonumber \\  %%верх
& (v_{i,3} \vee \neg z_{i,p+1}) \wedge
  (z_{i,p+1} \vee \neg z_{i,p+2}) \wedge
\nonumber \\
&  (z_{i,p+2} \vee \neg z_{i,p+3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p+q-1} \vee \neg z_{i,p+q}) \wedge
  (z_{i,p+q} \vee \neg v_{i,4} \vee u_{i}) \wedge \neg u_i  \wedge
\nonumber \\  %%низ
& (v_{i,4} \vee \neg v_{i,1}) \wedge
  (v_{i,1} \vee \neg v_{i,2}) \wedge
\nonumber \\
& (v_{i,2} \vee \neg v_{i,3}) \wedge
  (v_{i,3} \vee \neg v_{i,4}),
\end{eqnarray}
где $i+1=1$ для $i=l$.

Подформула, добавляемая по вершине $z_i$, $1 \leq i \leq l$, содержит ровно по три вхождения каждой из переменных
$v_{i,j}$, $1 \leq j \leq 4$.
Переменные $v_{i,j}$, $1 \leq j \leq 4$, содержатся только в формуле (\ref{ee_16}).
Каждая формула вида (\ref{ee_16}) содержит ровно по два вхождения переменных
$z_{i,j}$, $1 \leq j \leq p+q$. Функция $h$ имеет ровно по одному вхождению для каждой такой переменной.
Каждая формула вида (\ref{ee_16}) содержит ровно два вхождения переменной $u_{i}$ и одно вхождение переменной $u_{i+1}$.
Поэтому получаемая в итоге функция содержит ровно по три вхождения каждой переменной.

Заметим, что в графе $G_g$ ребер между дизъюнкциями из функции $h$ нет, поскольку каждая переменная имеет не более одного
вхождения в $h$.
Для подформулы
\begin{eqnarray}
\label{ee_17}
& (u_{i+1} \vee v_{i,1} \vee \neg z_{i,1}) \wedge
  (z_{i,1} \vee \neg z_{i,2}) \wedge
\nonumber \\
&  (z_{i,2} \vee \neg z_{i,3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p-1} \vee \neg z_{i,p}) \wedge
  (z_{i,p} \vee \neg v_{i,2})
\nonumber
\end{eqnarray}
формулы (\ref{ee_16}) ребра, соответствующие переменным $z_{i,j}$,
можно направить в верхнюю полуплоскость по маршрутам ребер
$e_1, e_2, \dots , e_p$.
Два ребра от вершины
$u_{i+1} \vee v_{i,1} \vee \neg z_{i,1}$,
 соответствующие переменной $u_{i+1}$,
 можно направить горизонтально влево по маршруту ребра
$(z_i, z_{i+1})$ к дизъюнкциям формулы вида  (\ref{ee_16}), соответствующей вершине $z_{i+1}$.

Для подформулы
\begin{eqnarray}
\label{ee_18}
& (v_{i,3} \vee \neg z_{i,p+1}) \wedge
  (z_{i,p+1} \vee \neg z_{i,p+2}) \wedge
\nonumber \\
&  (z_{i,p+2} \vee \neg z_{i,p+3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p+q-1} \vee \neg z_{i,p+q}) \wedge
  (z_{i,p+q} \vee \neg v_{i,4} \vee u_{i}) \wedge \neg u_i
\nonumber
\end{eqnarray}
формулы (\ref{ee_16}) ребра, соответствующие переменным $z_{i,j}$,
можно направить в нижнюю полуплоскость по маршрутам ребер
$e_{p+1}, e_{p+2}, \dots , e_{p+q}$.
Ребра от вершин
$z_{i,p+q} \vee \neg v_{i,4} \vee u_{i}$ и $\neg u_i$,
 соответствующие переменной $u_{i}$,
 можно направить горизонтально вправо по маршруту ребра
$(z_i, z_{i-1})$ к дизъюнкциям формулы вида  (\ref{ee_16}), соответствующей вершине $z_{i-1}$.
Непосредственной проверкой можно убедиться в том, что дизъюнкции формулы (\ref{ee_16}), содержащие локальные переменные $v_{i,j}$,
можно соединить ребрами без самопересечений. Таким образом, преобразование, связанное с добавлением формул вида (\ref{ee_16}),
позволяет получить планарный граф $G_g$.

Легко понять, что подграф графа $G_g$, соответствующий формуле (\ref{ee_16}), является связным. Переменные $u_i$
обеспечивают принадлежность всех формул вида (\ref{ee_16}) одной компоненте связности. Поскольку каждая дизъюнкция функции $h$
содержит переменную, которая содержится в некоторой формуле вида (\ref{ee_16}), граф $G_g$ является связным.

Непосредственной проверкой можно убедиться в том, что выполнимость формулы
\begin{eqnarray}
& (v_{i,4} \vee \neg v_{i,1}) \wedge
  (v_{i,1} \vee \neg v_{i,2}) \wedge
 (v_{i,2} \vee \neg v_{i,3}) \wedge
  (v_{i,3} \vee \neg v_{i,4})
  \nonumber
\end{eqnarray}
равносильна выполнимости системы равенств
$$v_{i,1} = v_{i,2} = v_{i,3} = v_{i,4}.$$
Поэтому выполнимость формулы (\ref{ee_16}) равносильна выполнимости формулы
\begin{eqnarray}
\label{ee_19}
& (u_{i+1} \vee v_{i,1} \vee \neg z_{i,1}) \wedge
  (z_{i,1} \vee \neg z_{i,2}) \wedge
\nonumber \\
&  (z_{i,2} \vee \neg z_{i,3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p-1} \vee \neg z_{i,p}) \wedge
  (z_{i,p} \vee \neg v_{i,2}) \wedge
\nonumber \\  %%верх
& (v_{i,3} \vee \neg z_{i,p+1}) \wedge
  (z_{i,p+1} \vee \neg z_{i,p+2}) \wedge
\nonumber \\
&  (z_{i,p+2} \vee \neg z_{i,p+3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p+q-1} \vee \neg z_{i,p+q}) \wedge
  (z_{i,p+q} \vee \neg v_{i,4} \vee u_{i}) \wedge \neg u_i  \wedge
\nonumber \\  %%низ
& v_{i,1} = v_{i,2} = v_{i,3} = v_{i,4}.
\end{eqnarray}
Дизъюнкция $\neg u_i$ может выполняться только при условии $u_i=0$.
Поэтому выполнимость формулы
(\ref{ee_19}) равносильна выполнимости формулы
\begin{eqnarray}
\label{ee_20}
& (u_{i+1} \vee v_{i,1} \vee \neg z_{i,1}) \wedge
  (z_{i,1} \vee \neg z_{i,2}) \wedge
\nonumber \\
&  (z_{i,2} \vee \neg z_{i,3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p-1} \vee \neg z_{i,p}) \wedge
  (z_{i,p} \vee \neg v_{i,2}) \wedge
\nonumber \\  %%верх
& (v_{i,3} \vee \neg z_{i,p+1}) \wedge
  (z_{i,p+1} \vee \neg z_{i,p+2}) \wedge
\nonumber \\
&  (z_{i,p+2} \vee \neg z_{i,p+3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p+q-1} \vee \neg z_{i,p+q}) \wedge
  (z_{i,p+q} \vee \neg v_{i,4} ) \wedge
\nonumber \\  %%низ
& v_{i,1} = v_{i,2} = v_{i,3} = v_{i,4}.
\end{eqnarray}
Легко проверить, что формула (\ref{ee_20})
выполняется тогда и только тогда, когда выполняется формула
\begin{eqnarray}
\label{ee_21}
& (u_{i+1} \vee v \vee \neg z_{i,1}) \wedge
  (z_{i,1} \vee \neg z_{i,2}) \wedge
\nonumber \\
&  (z_{i,2} \vee \neg z_{i,3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p-1} \vee \neg z_{i,p}) \wedge
  (z_{i,p} \vee \neg v) \wedge
\nonumber \\  %%верх
& (v \vee \neg z_{i,p+1}) \wedge
  (z_{i,p+1} \vee \neg z_{i,p+2}) \wedge
\nonumber \\
&  (z_{i,p+2} \vee \neg z_{i,p+3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p+q-1} \vee \neg z_{i,p+q}) \wedge
  (z_{i,p+q} \vee \neg v ).
\end{eqnarray}
Формула вида (\ref{ee_16}) для вершины $z_{i+1}$ содержит дизъюнкцию
$\neg u_{i+1}$, которая может быть выполнима лишь при условии $u_{i+1}=0$. Поэтому выполнимость формулы
(\ref{ee_21}) равносильна выполнимости формулы
\begin{eqnarray}
\label{ee_22}
& (v \vee \neg z_{i,1}) \wedge
  (z_{i,1} \vee \neg z_{i,2}) \wedge
\nonumber \\
&  (z_{i,2} \vee \neg z_{i,3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p-1} \vee \neg z_{i,p}) \wedge
  (z_{i,p} \vee \neg v) \wedge
\nonumber \\  %%верх
& (v \vee \neg z_{i,p+1}) \wedge
  (z_{i,p+1} \vee \neg z_{i,p+2}) \wedge
\nonumber \\
&  (z_{i,p+2} \vee \neg z_{i,p+3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p+q-1} \vee \neg z_{i,p+q}) \wedge
  (z_{i,p+q} \vee \neg v ).
\end{eqnarray}
Непосредственной проверкой можно убедиться в том,
что формула
\begin{eqnarray}
\label{ee_23}
& (v \vee \neg z_{i,1}) \wedge
  (z_{i,1} \vee \neg z_{i,2}) \wedge
\nonumber \\
&  (z_{i,2} \vee \neg z_{i,3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p-1} \vee \neg z_{i,p}) \wedge
  (z_{i,p} \vee \neg v)
\end{eqnarray}
выполняется тогда и только тогда, когда выполняется система равенств
$$z_{i,1} = z_{i,2} =  \dots = z_{i,p},$$
а формула
\begin{eqnarray}
\label{ee_24}
& (v \vee \neg z_{i,p+1}) \wedge
  (z_{i,p+1} \vee \neg z_{i,p+2}) \wedge
\nonumber \\
&  (z_{i,p+2} \vee \neg z_{i,p+3}) \wedge \dots \wedge
\nonumber \\
&  (z_{i,p+q-1} \vee \neg z_{i,p+q}) \wedge
  (z_{i,p+q} \vee \neg v )
\end{eqnarray}
выполняется тогда и только тогда, когда выполняется система равенств
$$z_{i,p+1} = z_{i,p+2} =  \dots = z_{i,p+q}.$$
Поскольку формула (\ref{ee_22}) является конъюнкцией формул (\ref{ee_23}) и (\ref{ee_24}),
отсюда вытекает, что формула (\ref{ee_22}) выполняется тогда и только тогда, когда
выполняется система равенств
$$z_{i,1} = z_{i,2} =  \dots = z_{i,p} =z_{i,p+1} = z_{i,p+2} =  \dots = z_{i,p+q}.$$
Отсюда вытекает, что в функцию $h$ вместо переменных $z_{i,j}$ можно подставить переменную $z_i$.
При этом мы получим равносильность выполнимости функции $g$ и выполнимости функции $h$.
\end{proof}

Из теоремы \ref{TT_03} получаем следующее утверждение.

\begin{corollary}
\label{CC_03}
Проблема \#{\sc PC-$\leq$3SAT} является \#{\bf P}-полной относительно экономной сводимости.
\end{corollary}


Хорошо известно, что проблема {\sc $\leq$3SAT} остается {\bf NP}-полной даже при ограничении, допускающем использование
лишь булевых функций, содержащих ровно три вхождения каждой переменной
(см., например, \cite{Goldreich__2008}, предложение 2.23).
Булевы функции, которые мы построили при доказательстве теоремы \ref{TT_03}, удовлетворяют этому ограничению.
Поэтому в предположении, что каждая булева функция содержит ровно три вхождения каждой переменной,
проблема \#{\sc PC-$\leq$3SAT} является \#{\bf P}-полной относительно экономной сводимости, а
проблема {\sc PC-$\leq$3SAT} является {\bf NP}-полной относительно экономной сводимости.



Фазовый переход для проблемы выполнимости принято связывать с отношением $\alpha = \frac{m}{n}$,
где $m$~--- количество дизъюнкций, $n$~--- количество переменных \cite{Mitchell__Selman__1992}.
Экспериментальные исследования показывают, что для случайных входов проблемы $k$-выполнимости
существует критическое значение $\alpha_c$ отношения $\frac{m}{n}$ такое, что для
$\alpha < \alpha_c$ булева функция с высокой вероятностью выполняется,
а для $\alpha > \alpha_c$ функция с высокой вероятностью выполнимой не является.
Более того, экспериментальные исследования показывают, что трудные случайные исходные данные имеют
близкие к $\alpha_c$ значения $\alpha$, а по мере удаления от $\alpha_c$ трудность падает \cite{Mitchell__Selman__1992}.
Существование $\alpha_c$ при $n \rightarrow + \infty$ для любого $k$ доказано в работе
\cite{Friedgut__Bourgain__1999}.
Для $k=2$ известно, что $\alpha_c = 1$
\cite{Chvatal__Reed__1992,Goerdt__1992}.
В частности, в работе
\cite{Goerdt__1996}
для $k=2$ показано, что для фиксированного $\varepsilon > 0$
при $\alpha > 1 + \varepsilon$ и $n \rightarrow + \infty$
вероятность невыполнимости булевой функции стремится к 1.
Кроме того, для $k=2$ и фиксированного $\varepsilon > 0$
при $\alpha < 1 - \varepsilon$ и $n \rightarrow + \infty$
вероятность выполнимости булевой функции стремится к 1 \cite{Goerdt__1996}.
В работе
\cite{Bolloba__Borgs__2001}
установлено, что поведение булевых функций при $k=2$ аналогично поведению графов.
Для $k=3$ известно, что $\alpha_c \approx 4.26$
\cite{Crawford__Auton__1996}.
Кроме того, известно, что $3.42 < \alpha_c < 4.506$
\cite{Dubois__Boufkhad__2000,Kaporis__Kirousis__2006}.
Нетривиальная сложность наблюдается при значениях $\alpha$,
удовлетворяющих соотношениям
$3.921 < \alpha_c < 4.256$
\cite{Mezard__Parisi__2002}.
Однако для статистических решателей трудность интервала
$3.921 < \alpha_c < 4.256$
начинает проявляться лишь при $n$ существенно больше 1000
\cite{Mezard__2003}.
Необходимость учитывать особенности фазового перехода существенно влияет на процесс разработки решателей.
Производительность решателей в значительной мере зависит от близости к пороговому значению.
В наибольшей степени это влияние сказывается на статистических решателях
(см., например,
\cite{Franco__2005,Fu__Cai__Wu__2024,Fu__Xu__Wu__2021}).
В последние годы все большее внимание уделяется исследованиям, связанным с структурными характеристиками булевых
функций и возможностью их использования для разработки решателей
(см., например,
\cite{Alyahya__Menai__2022,Alyahya__Menai__2__2022,Zhang__Xu__Zhou__2021}).
В частности, можно отметить подход, предложенный в работе
\cite{Newton__Polash__2021}, который основан на поиске логических преобразователей по их
представлениям в виде подформул
(см. \cite{Tseitin__1983,Ostrowski__Gregoire__2002,Plaisted__Greenbaum__1986})
и построении графовой структуры.
Однако статистические решатели по-прежнему играют определяющую роль.
Ярким примером является алгоритм WalkSAT
(см., например,
\cite{Bearden__Pei__2020,Cai__Luo__Su__2015,Fu__Xu__Chen__2020}).
Конструкция, рассмотренная при доказательстве теоремы \ref{TT_03},
представляется весьма перспективной для эффективной модификации булевых функций в зависимости
от требований, связанных с фазовым переходом.
Для булевых функций, определяемых сводимостью из доказательства теоремы \ref{TT_03},
значение $\alpha$ равно 1, т.е. они являются сильно разреженными.
Случайные булевы функции с таким значением $\alpha$
должны выполняться с вероятностью, которая близка к 1.
В то же время функции, получаемые при помощи сводимости, содержат всю трудность
проблемы {\sc SAT}. При этом они имеют весьма простую структуру. В частности,
трехмерных структур нет вообще.
Последовательностью преобразований, например, на основе замен формул вида (\ref{ee_01}) на формулы вида (\ref{ee_02}),
из этих функций можно получать функции с заданными структурными характеристиками и заданным значением $\alpha$.
В частности, это можно использовать для маскировки и затруднения работы статистических решателей и решателей
на основе машинного обучения.

\section{Заключение}

В данной работе мы установили, что проблема \#{\sc 3SAT} является \#{\bf P}-полной относительно экономной сводимости
в предположении, что в каждой дизъюнкции три литерала соответствуют трем различным переменным.
Кроме того, показана \#{\bf P}-полнота относительно экономной сводимости для проблем \#{\sc C-3SAT}, \#{\sc C-$\leq$3SAT},
\#{\sc C-SAT}, \#{\sc SC-3SAT}, \#{\sc PC-$\leq$3SAT}.
Использование экономной сводимости позволяет получить ряд важных следствий для различных классов вычислительной сложности.
В частности, согласно \cite{Bakali__Chalki__2024}, в предположении, что в каждой дизъюнкции три литерала соответствуют трем различным переменным, проблемы $\oplus{\sc 3SAT}$, ${\bf Mod}_k{\sc 3SAT}$, ${\bf Diff}{\sc 3SAT}_{=0}$, ${\bf Diff}{\sc 3SAT}_{>0}$,
${\bf Diff}{\sc 3SAT}_{=1}$ и
${\bf Diff}{\sc 3SAT}_{=g}$ являются полными для классов
$\oplus{\bf P}$, {\bf Mod}$_k${\bf P}, {\bf C$_=$P}, {\bf PP}, {\bf SPP} и {\bf WPP}, соответственно.

Трудность проблемы {\sc PC-$\leq$3SAT} показана для булевых функций с малым значением отношения $\frac{m}{n}$,
удобных для модификации и последующего использования в криптографических целях и при создании тестовых данных для решателей.


\bigskip
\begin{thebibliography}{1} % Ссылки на литературу приводятся только на английском языке (даже если у источника нет англоязычной версии).

\bibitem{Berman__Karpinski__2007}
P. Berman, M. Karpinski, A. D. Scott,
\href{https://doi.org/10.1016/j.dam.2006.07.009}{\it Computational complexity of some restricted instances of 3-SAT}, Discrete Applied Mathematics, {\bf 155} (2007), 649--653.

\bibitem{Darmann__Docker__2021}
A. Darmann, J. D{\" o}cker,
\href{https://doi.org/10.1016/j.dam.2020.12.010}{\it On simplified NP-complete variants of Monotone
 3-Sat}, Discrete Applied Mathematics, {\bf 292} (2021), 45--58.

\bibitem{Misra__Narayanaswamy__2010}
N. Misra, N. S. Narayanaswamy, V. Raman, B. S. Shankar,
\href{https://doi.org/10.1007/978-3-642-15155-2_48}{\it Solving MINONES-2-SAT as Fast as VERTEX COVER}, Lecture Notes in Computer Science, {\bf 6281} (2010), 549--555.

\bibitem{Tseitin__1983}
G. S. Tseitin,
\href{https://doi.org/10.1007/978-3-642-81955-1_28}{\it On the Complexity of Derivation in Propositional Calculus}, Symbolic Computation, {\bf 1064} (1983), 466--483.

\bibitem{Curtis__Tenenbaum__2022}
A. Curtis, J. B. Tenenbaum, T. Lozano-P{\' e}rez, L. Kaelbling,
\href{https://doi.org/10.1609/aaai.v36i5.20475}{\it Discovering State and Action Abstractions for Generalized Task and Motion Planning}, Proceedings of the AAAI Conference on Artificial Intelligence, {\bf 36} (2022), 5377--5384.

\bibitem{Ablad__Spensieri__2023}
E. Ablad, D. Spensieri, R. Bohlin, J. S. Carlson, A.-B. Str{\" o}mberg,
\href{https://doi.org/10.1109/TASE.2022.3214567}{\it Spatial–Temporal Load Balancing and Coordination of Multi-Robot Stations}, IEEE Transactions on Automation Science and Engineering, {\bf 20} (2023), 2203--2214.

\bibitem{Meli__Nakawala__2023}
D. Meli, H. Nakawala, P. Fiorini,
\href{https://doi.org/10.1007/s10462-022-10389-w}{\it Logic programming for deliberative robotic task planning}, Artifcial Intelligence Review, {\bf 56} (2023), 9011--9049.

\bibitem{Matlekovic__Schneider-Kamp__2023}
L. Matlekovic, P. Schneider-Kamp,
\href{https://doi.org/10.3390/drones7090563}{\it Constraint Programming Approach to Coverage-Path Planning for Autonomous Multi-UAV Infrastructure Inspection}, Drones, {\bf 7} (2023), 563.

\bibitem{Wang__Ma__Wang__2021}
L. Wang, W. Ma, L. Wang, Y. Ren, C. Yu,
\href{https://doi.org/10.1155/2021/5531063}{\it Enabling In-Depot Automated Routing and Recharging Scheduling for Automated Electric Bus Transit Systems}, Journal of Advanced Transportation, {\bf 2021} (2021), 5531063.

\bibitem{Abed__Ashkanan__2020}
S. Abed, A. Ashkanan, W. Mansoor, A. Gawanmeh,
\href{https://doi.org/10.1007/978-3-030-43020-7_26}{\it Enhanced SAT Solvers Based Hashing Method for Bitcoin Mining}, Advances in Intelligent Systems and Computing, {\bf 1134} (2020), 191--198.

\bibitem{Trimoska__Ionica__2020}
M. Trimoska, S. Ionica, G. Dequen,
\href{https://doi.org/10.1007/978-3-030-51938-4_11}{\it A SAT-Based Approach for Index Calculus on Binary Elliptic Curves}, Progress in Cryptology~--- AFRICACRYPT 2020, {\bf 12174} (2020), 214--235.

\bibitem{Utsumi__Sakamoto__2023}
S. Utsumi, K. Sakamoto, T. Isobe,
\href{https://doi.org/10.1049/ise2.12119}{\it Bit-level evaluation of piccolo block cipher by satisfiability
problem solver}, IET Information Security, {\bf 17} (2023), 616--625.

\bibitem{Huang__Newman__2020}
C. Huang, M. Newman, M. Szegedy,
\href{https://doi.org/10.1109/TIT.2020.3004427}{\it Explicit Lower Bounds on Strong Quantum Simulation}, IEEE Transactions on Information Theory, {\bf 66} (2020),  5585--5600.

\bibitem{Schneider__Burgholzer__2023}
S. Schneider, L. Burgholzer, R. Wille,
\href{https://doi.org/10.1145/3566097.3567929}{\it A SAT Encoding for Optimal Clifford Circuit Synthesis}, Proceedings of the 28th Asia and South Pacific Design Automation Conference (2023),  190--195.

\bibitem{Bliznets__Sagunov__2022}
I. Bliznets, D. Sagunov, K. Simonov,
\href{https://www.ijcai.org/proceedings/2022/0247.pdf}{\it Fine-grained Complexity of Partial Minimum Satisfiability}, Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, (2022), 1774--1780.

\bibitem{Lin__Althoff__2022}
Y. Lin, M. Althoff,
\href{https://doi.org/10.1109/IV51971.2022.9827357}{\it Rule-Compliant Trajectory Repairing using Satisfiability Modulo Theories}, IEEE Intelligent Vehicles Symposium, {\bf 4} (2022), 1--8.

\bibitem{Caballero__Gomez__2023}
D. Caballero, T. Gomez, R. Schweller, T. Wylie,
\href{https://doi.org/10.1007/s00453-023-01103-5}{\it Unique Assembly Verification in Two-Handed Self-Assembly}, Algorithmica, {\bf 85} (2023), 2427--2453.

\bibitem{Demaine__Eisenstat__2011}
E. D. Demaine, S. Eisenstat,
\href{https://doi.org/10.1007/978-3-642-22300-6_27}{\it Flattening Fixed-Angle Chains Is Strongly NP-Hard}, Lecture Notes in Computer Science, {\bf 6844} (2011), 314--325.

\bibitem{Imeson__Smith__2019}
F. Imeson, S. L. Smith,
\href{https://doi.org/10.1109/TRO.2019.2896401}{\it An SMT-Based Approach to Motion Planning for Multiple Robots With Complex Constraints}, IEEE Transactions on Robotics, {\bf 35} (2019), 669--684.

\bibitem{Giraldez__Levy__2016}
J. Gir{\' a}ldez-Cru, J. Levy,
\href{https://doi.org/10.1016/j.artint.2016.06.001}{\it Generating SAT instances with community structure}, Artificial Intelligence, {\bf 238} (2016), 119--134.

\bibitem{Amendola__Ricca__2020}
G. Amendola, F. Ricca, M. Truszczynski,
\href{https://doi.org/10.1016/j.artint.2019.103185}{\it New models for generating hard random boolean formulas and disjunctive logic programs}, Artificial Intelligence, {\bf 279} (2020), 103185.

\bibitem{Barak-Pelleg__Berend__2022}
D. Barak-Pelleg, D. Berend, J. C. Saunders,
\href{https://doi.org/10.1016/j.tcs.2022.01.038}{\it A model of random industrial SAT},
Theoretical Computer Science, {\bf 910} (2022), 91--112.

\bibitem{Heradio__Fernandez__2022}
R. Heradio, D. Fernandez-Amoros, J. A. Galindo, D. Benavides, D. Batory,
\href{https://doi.org/10.1007/s10664-021-10102-5}{\it Uniform and scalable sampling of highly configurable systems}, Empirical Software Engineering, {\bf 27} (2022), 1--34.

\bibitem{Ebert__Weyrich__2021}
C. Ebert, M. Weyrich, B. Lindemann, S. P. Chandrasekar,
\href{https://doi.org/10.1007/s38314-020-0575-6}{\it Systematic Testing for Autonomous Driving},  ATZelectronics worldwide, {\bf 16} (2021), 18--23.

\bibitem{Guo__Zhen__Li__2023}
W. Guo, H.-L. Zhen, X. Li, W. Luo, M. Yuan, Y. Jin, J. Yan,
\href{https://doi.org/10.1007/s11633-022-1396-2}{\it Machine Learning Methods in Solving the Boolean Satisfiability Problem},  Machine Intelligence Research, {\bf 20} (2023), 640--655.

\bibitem{Sun__Gerault__2020}
L. Sun, D. Gerault, A. Benamira, T. Peyrin,
\href{https://doi.org/10.1007/978-3-030-49785-9_5}{\it NeuroGIFT: Using a Machine Learning Based Sat Solver for Cryptanalysis},  Lecture Notes in Computer Science, {\bf 12161} (2020), 62--84.

\bibitem{Leventi__Peetz__2019}
A. M. Leventi-Peetz, J.-V. Peetz, M. Rohde,
\href{https://doi.org/10.1007/978-3-030-32520-6_7}{\it ML Supported Predictions for SAT Solvers Performance}, Advances in Intelligent Systems and Computing, {\bf 1069} (2019), 64--78.

\bibitem{Mosca__Verschoor__2022}
M. Mosca, S. R.Verschoor,
\href{https://doi.org/10.1038/s41598-022-11687-7}{\it Factoring semi-primes with (quantum) SAT-solvers}, Scientifc Reports, {\bf 12} (2022), 7982.

\bibitem{Branco__Mateus__2020}
P. Branco, P. Mateus, C. Salema, A. Souto,
\href{https://doi.org/10.1016/j.ins.2019.09.030}{\it Using Low-Density Parity-Check codes to improve the McEliece cryptosystem}, Information Sciences, {\bf 510} (2020),  243--255.

\bibitem{Egger__Xhemrishi__2023}
M. Egger, M. Xhemrishi, A. Wachter-Zeh, R. Bitar,
\href{https://doi.org/10.1109/ISIT54713.2023.10206979}{\it Sparse and Private Distributed Matrix Multiplication with Straggler Tolerance}, IEEE International Symposium on Information Theory, IEEE, Taipei, 2023.

\bibitem{Perez_Pacheco__Caballero_Gil__2023}
P. P{\' e}rez-Pacheco, P. Caballero-Gil,
\href{https://doi.org/10.1109/DRCN57075.2023.10108339}{\it McEliece Cryptosystem: Reducing the Key Size with QC-LDPC codes}, 19th International Conference on the Design of Reliable Communication Networks, IEEE, Vilanova i la Geltru, 2023.

\bibitem{Afzal__Yousaf__2020}
S. Afzal, M. Yousaf, H. Afzal, N. Alharbe, M. R. Mufti,
\href{https://doi.org/10.1155/2020/3189601}{\it Cryptographic Strength Evaluation of Key Schedule Algorithms}, Security and Communication Networks, {\bf 2020} (2020),  3189601.

\bibitem{Baldi__Deneuville__2021}
M. Baldi, J.-C. Deneuville, E. Persichetti, P. Santini,
\href{https://doi.org/10.1109/LCOMM.2021.3096256}{\it Cryptanalysis of a Code-Based Signature Scheme Based on the Schnorr-Lyubashevsky Framework}, IEEE Communications Letters, {\bf 25} (2021),  2829--2833.

\bibitem{Hartmann__Weigt__2005}
A. K. Hartmann, M. Weigt,
\href{https://doi.org/10.1002/3527606734}{\it Phase Transitions in Combinatorial Optimization Problems: Basics, Algorithms and Statistical Mechanics}, WILEY-VCH Verlag GmbH \& Co. KGaA, Weinheim, 2005.

\bibitem{Mezard__Montanari__2009}
M. M{\' e}zard, A. Montanari,
\href{https://doi.org/10.1093/acprof:oso/9780198570837.001.0001}{\it Information, Physics, and Computation}, Oxford University Press, New York, 2009.

\bibitem{Moore__Mertens__2011}
C. Moore, S. Mertens,
\href{https://doi.org/10.1093/acprof:oso/9780199233212.001.0001}{\it The Nature of Computation}, Oxford University Press, New York, 2011.

\bibitem{Mitchell__Selman__1992}
D. Mitchell, B. Selman, H. Levesque,
\href{https://cdn.aaai.org/AAAI/1992/AAAI92-071.pdf}{\it Hard and easy distributions of SAT problems}, Proceedings of the 10th National Conference on Artificial Intelligence, AAAI, 1992,  459--465.

\bibitem{Cheeseman__Kanefsky__1991}
P. Cheeseman, B. Kanefsky, W. M. Taylor,
\href{https://www.dcs.gla.ac.uk/~pat/cpM/papers/cheeseman91where.pdf}{\it Where the really hard problems are}, Proceedings of the 12th international joint conference on Artificial intelligence, {\bf 1} (1991),  331--337.

\bibitem{Sleegers__Olij__2000}
J. Sleegers, R. Olij, G. van Horn, D. van den Berg,
\href{https://doi.org/10.1016/j.orp.2020.100160}{\it Where the really hard problems aren’t}, Operations Research Perspectives, {\bf 7} (2000),  100160.

\bibitem{Mezard__Parisi__2002}
M. M{\' e}zard, G. Parisi, R. Zecchina,
\href{https://doi.org/10.1126/science.1073287}{\it Analytic and Algorithmic Solution of Random Satisfiability Problems}, Science, {\bf 297} (2002),  812--815.

\bibitem{Biroli__Cocco__2002}
G. Biroli, S. Cocco, R. Monasson,
\href{https://doi.org/10.1016/S0378-4371(02)00516-2}{\it Phase transitions and complexity in computer science: an overview of the statistical physics approach to the random satisfiability problem}, Physica A: Statistical Mechanics and its Applications, {\bf 306} (2002),  381--394.

\bibitem{Perkins__2024}
W. Perkins,
\href{https://doi.org/10.48550/arXiv.2401.01800}{\it Searching for (sharp) thresholds in random structures: where are we now?},  arXiv:2401.01800v1 (2024),  1--29.

\bibitem{Ding__Sly__2016}
J. Ding, A. Sly, N. Sun,
\href{https://doi.org/10.1007/s00220-015-2492-8}{\it Satisfiability Threshold for Random Regular NAE-SAT}, Communications in Mathematical Physics, {\bf 341} (2016),  435--489.

\bibitem{Ding__Sly__2022}
J. Ding, A. Sly, N. Sun,
\href{https://doi.org/10.4007/annals.2022.196.1.1}{\it Proof of the satisfiability conjecture for large k}, Annals of Mathematics, {\bf 196} (2022),  1--388.

\bibitem{Park__Pham__2024}
 J. Park, H. T. Pham,
\href{https://doi.org/10.1090/jams/1028}{\it A proof of the Kahn–Kalai conjecture}, Journal of the American Mathematical Society, {\bf 37} (2024),  235--243.

\bibitem{Schawe__Bleim__2019}
H. Schawe, R. Bleim, A. K. Hartmann,
\href{https://doi.org/10.1371/journal.pone.0215309}{\it Phase transitions of the typical algorithmic complexity of the random satisfiability problem studied with linear programming}, PLoS One, {\bf 14} (2019), e0215309.

\bibitem{Schmittner__2015}
S. E. Schmittner,
\href{https://doi.org/10.48550/arXiv.1507.08094}{\it A SAT-based Public Key Cryptography Scheme}, arXiv:1507.08094v3 (2015), 1--11.

\bibitem{Sun__Peng__Tian__2017}
R. Sun, Q. Peng, Y. Tian,
\href{https://doi.org/10.1109/GlobalSIP.2017.8309184}{\it A hybrid encryption scheme based on the satisfiability problem}, IEEE Global Conference on Signal and Information Processing, IEEE, Montreal, 2017.

\bibitem{Thomas__Chaudhari__2011}
J. Thomas, N. S. Chaudhari,
\href{https://research.ijcaonline.org/encc/number2/encc009.pdf}{\it Hybrid Cryptosystem Based on 2-SAT \& 3-SAT and
the Implications of Polynomial Solvability of 3-SAT}, International Journal of Computer Applications, {\bf 2} (2011), 1--6.

\bibitem{Li__Chen__Guo__2023}
Y. Li, X. Chen, W. Guo, X. Li, W. Luo, J. Huang, H.-L. Zhen, M. Yuan, J. Yan,
\href{https://doi.org/10.1145/3580305.3599837}{\it HardSATGEN: Understanding the Difficulty of Hard SAT Formula Generation and A Strong Structure-Hardness-Aware Baseline}, Proceedings of the 29th ACM SIGKDD Conference on Knowledge Discovery and Data Mining (2023), 4414--4425.

\bibitem{Newsham__Ganesh__2014}
Z. Newsham, V. Ganesh, S. Fischmeister, G. Audemard, L. Simon,
\href{https://doi.org/10.1007/978-3-319-09284-3_20}{\it Impact of Community Structure on SAT Solver Performance}, Lecture Notes in Computer Science, {\bf 8561} (2014), 252--268.

\bibitem{Slater__2002}
A. Slater,
\href{https://doi.org/10.1007/3-540-36187-1_52}{\it Modelling More Realistic SAT Problems}, Lecture Notes in Computer Science, {\bf 2557} (2002), 591--602.

\bibitem{Demaine__Karntikoon__2023}
E. D. Demaine, K. Karntikoon, N. Pitimanaaree,
\href{https://arxiv.org/abs/2309.09786}{\it 2-Colorable Perfect Matching is NP-complete in 2-Connected 3-Regular Planar Graphs},  arXiv:2309.09786v1 (2023), 1--11.

\bibitem{Cook__1971}
S. A. Cook,
\href{https://doi.org/10.1145/800157.805047}{\it The complexity of theorem-proving procedures}, Proceedings of the third annual ACM symposium on Theory of computing (1971) 151--158.

\bibitem{Garey__Johnson__1979}
M. R. Garey, D. S. Johnson,
\href{https://djvu.online/file/sEtkhOgJV2w9w}{\it Computers and Intractability: A Guide to the Theory of NP-Completeness}, W. H. Freeman, New York, 1979.

\bibitem{Karp__1972}
R. M. Karp,
\href{https://doi.org/10.1007/978-1-4684-2001-2_9}{\it Reducibility among combinatorial problems}, Complexity of Computer Computations, The IBM Research Symposia Series, Springer, Boston, 1972, 85--103.

\bibitem{Juban__1999}
L. Juban,
\href{https://doi.org/10.1007/3-540-48321-7_27}{\it Dichotomy theorem for the generalized unique satisfiability problem}, Lecture Notes in Computer Science, {\bf 1684} (1999), 327--337.

\bibitem{Sundermann__Hess__2023}
C. Sundermann, T. He{\ss}, M. Nieke, P. Bittner, J. Young, T. Th{\" u}m, I. Schaefer,
\href{https://doi.org/10.1007/s10664-022-10265-9}{\it Evaluating state-of-the-art \# SAT solvers on industrial configuration spaces}, Empirical Software Engineering, {\bf 28} (2023),  1--38.

\bibitem{Sundermann__Thum__2020}
C. Sundermann, T. Th{\" u}m, I. Schaefer,
\href{https://doi.org/10.1145/3377024.3377025}{\it Evaluating \#SAT solvers on industrial feature models}, Proceedings of the 14th International Working Conference on Variability Modelling of Software-Intensive Systems, {\bf 3} (2020),  1--9.

\bibitem{Zhao__Liao__Luo__2023}
D. Zhao, L. Liao, W. Luo, J. Xiang, H. Jiang, X. Hu,
\href{https://doi.org/10.1613/jair.1.13909}{\it Generating Random SAT Instances: Multiple Solutions could be Predefined and Deeply Hidden}, Journal of Artificial Intelligence Research, {\bf 76} (2023),  435--470.

\bibitem{Downey__Fellows__1999}
R. G. Downey, M. R. Fellows,
\href{https://doi.org/10.1007/978-1-4612-0515-9}{\it Parameterized Complexity}, Springer, New York,  1999.

\bibitem{Flum__Grohe__2004}
J. Flum, M. Grohe,
\href{https://doi.org/10.1137/S0097539703427203}{\it The Parameterized Complexity of Counting Problems}, SIAM Journal on Computing, {\bf 33} (2004),  1--29.

\bibitem{Ladner__Lynch__1975}
R. E. Ladner, N. A. Lynch, A. L. Selman,
\href{https://doi.org/10.1016/0304-3975(75)90016-X}{\it A comparison of polynomial time reducibilities}, Theoretical Computer Science, {\bf 1} (1975),  103--123.

\bibitem{Papadimitriou__1994}
C. H. Papadimitriou,
{\it Computational Complexity}, Addison-Wesley Publishing Co. Inc., Boston, 1994.

\bibitem{Jayasena__Mishra__2024}
A. Jayasena, P. Mishra,
\href{https://doi.org/10.1145/3638046}{\it Directed Test Generation for Hardware Validation: A Survey}, ACM Computing Surveys,  {\bf 56} (2024),  1--36.

\bibitem{Lin__Zhao__2004}
F. Lin, Y. Zhao,
\href{https://doi.org/10.1016/j.artint.2004.04.004}{\it ASSAT: computing answer sets of a logic program by SAT solvers}, Artificial Intelligence, {\bf 157} (2004),  115--137.

\bibitem{Rubio__Cantarero__2024}
A. Rubio, R. Cantarero, A. Margara, G. Cugola, D. Villa, J. C. L{\' o}pez,
\href{https://doi.org/10.1016/j.iot.2023.100998}{\it Commonsense reasoning and automatic generation of IoT contextual knowledge: An Answer Set Programming approach}, Internet of Things, {\bf 25} (2024),  100998.

\bibitem{Soh__Tamura__Banbara__2013}
T. Soh, N. Tamura, M. Banbara,
\href{https://doi.org/10.1007/978-3-642-39071-5_34}{\it Scarab: A Rapid Prototyping Tool for SAT-Based Constraint Programming Systems}, Lecture Notes in Computer Science,, {\bf 7962} (2013),  429--436.

\bibitem{Kim__Rahman__2024}
D. Kim, N. M. Rahman, S. Mukhopadhyay,
\href{https://doi.org/10.1109/JSSC.2024.3352585}{\it PRESTO: A Processing-in-Memory-Based k -SAT Solver Using Recurrent Stochastic Neural Network With Unsupervised Learning}, IEEE Journal of Solid-State Circuits,  (2024),  1--11.

\bibitem{Sohanghpurwala__Hassan__2017}
A. A. Sohanghpurwala, M. W. Hassan, P. Athanas,
\href{https://doi.org/10.1016/j.jpdc.2016.12.014}{\it Hardware accelerated SAT solvers~--- A survey}, Journal of Parallel and Distributed Computing, {\bf 106} (2017),  170--184.

\bibitem{Hu__Zhang__Ardeshiricham__2017}
W. Hu, L. Zhang, A. Ardeshiricham, J. Blackstone, B. Hou, Y. Tai, R. Kastner,
\href{https://doi.org/10.1109/ICCAD.2017.8203846}{\it Why you should care about don't cares: Exploiting internal don't care conditions for hardware Trojans}, IEEE/ACM International Conference on Computer-Aided Design, IEEE, Irvine, 2017.

\bibitem{Mahmoud__Shokry__2024}
D. G. Mahmoud, B. Shokry, V. Lenders, W. Hu, M. Stojilovi{\' c},
\href{https://doi.org/10.1109/ACCESS.2024.3353134}{\it X-Attack 2.0: The Risk of Power Wasters and Satisfiability Don’t-Care Hardware Trojans to Shared Cloud FPGAs}, IEEE Access, {\bf 12} (2024),  8983--9011.

\bibitem{Su__Kim__Kim__2024}
Y. Su, T. T.-H. Kim, B. Kim,
\href{https://doi.org/10.1109/JSSC.2024.3352907}{\it FlexSpin: A CMOS Ising Machine With 256 Flexible Spin Processing Elements With 8-b Coefficients for Solving Combinatorial Optimization Problems}, IEEE Journal of Solid-State Circuits, (2024),  1--12.

\bibitem{Spakowski__Thakur__2005}
H. Spakowski, M. Thakur, R. Tripathi,
\href{https://doi.org/10.1016/j.ic.2004.10.009}{\it Quantum and classical complexity classes: Separations, collapses, and closure properties}, Information and Computation, {\bf 200} (2005),  1--34.

\bibitem{Ogiwara__Hemachandra__1993}
M. Ogiwara, L. A. Hemachandra,
\href{https://doi.org/10.1016/0022-0000(93)90006-I}{\it A complexity theory for feasible closure properties}, Journal of Computer and System Sciences, {\bf 46} (1993),  295--325.

\bibitem{Gill__1977}
J. Gill,
\href{https://doi.org/10.1137/0206049}{\it Computational complexity of probabilistic Turing machines}, SIAM Journal on Computing, {\bf 6} (1977),  675--695.

\bibitem{Simon__1975}
 J. Simon,
{\it On Some Central Problems in Computational Complexity}, Cornell Department of Computer Science Technical Report TR75-224, PhD thesis, Cornell University, Ithaca, 1975.

\bibitem{Beigel__Gill__1992}
R. Beigel, J. Gill,
\href{https://doi.org/10.1016/0304-3975(92)90084-S}{\it Counting classes: thresholds, parity, mods, and fewness}, Theoretical Computer Science, {\bf 103} (1992),  3--23.

\bibitem{Cai__Hemachandra__1990}
J. Cai, L. Hemachandra,
\href{https://doi.org/10.1007/BFb0028987}{\it On the power of parity polynomial time}, Mathematical Systems Theory, {\bf 23} (1990),  95--106.

\bibitem{Hertrampf__1990}
U. Hertrampf,
\href{https://doi.org/10.1016/0304-3975(90)90081-R}{\it Relations among mod-classes}, Theoretical Computer Science, {\bf 74} (1990),  325--328.

\bibitem{Goldschlager__Parberry__1986}
L. Goldschlager, I. Parberry,
\href{https://doi.org/10.1016/0304-3975(86)90165-9}{\it On the construction of parallel computers from various bases of boolean functions}, Theoretical Computer Science, {\bf 43} (1986),  43--58.

\bibitem{Papadimitriou__Zachos__1983}
C. Papadimitriou, S. Zachos,
\href{https://doi.org/10.1007/BFb0036487}{\it Two remarks on the power of counting}, Lecture Notes in Computer Science, {\bf 145} (1983),  269--276.

\bibitem{Fenner__Fortnow__1994}
S. Fenner, L. Fortnow, S. Kurtz,
\href{https://doi.org/10.1016/S0022-0000(05)80024-8}{\it Gap-definable counting classes}, Journal of Computer and System Sciences, {\bf 48} (1994),  116--148.

\bibitem{Wagner__1986}
K. W. Wagner,
\href{https://doi.org/10.1007/BF00289117}{\it The complexity of combinatorial problems with succinct input representations}, Acta Informatica, {\bf 23} (1986),  325--356.

\bibitem{Rao__Rothe__1994}
R. P. N. Rao, J. Rothe, O. Watanabe,
\href{https://doi.org/10.1016/0020-0190(94)90123-6}{\it Upward separation for FewP and related classes}, Information Processing Letters, {\bf 52} (1994),  175--180.

\bibitem{Valiant__1979}
L. G. Valiant,
\href{https://doi.org/10.1016/0304-3975(79)90044-6}{\it A complexity theory for feasible closure properties}, Theoretical Computer Science, {\bf 8} (1979),  189--201.

\bibitem{Barbanchon__2004}
R. Barbanchon,
\href{https://doi.org/10.1016/j.tcs.2004.02.003}{\it On unique graph 3-colorability and parsimonious reductions in the plane}, Theoretical Computer Science, {\bf 319} (2004),  455--482.

\bibitem{Bakali__Chalki__2024}
E. Bakali, A. Chalki, S. Kanellopoulos, A. Pagourtzis, S. Zachos,
\href{https://doi.org/10.48550/arXiv.2306.11614}{\it On the power of counting the total number of computation paths of NPTMs}, arXiv:2306.11614v3 (2024),  1--18.

\bibitem{Lichtenstein__1982}
D. Lichtenstein,
\href{https://doi.org/10.1137/0211025}{\it Planar Formulae and Their Uses}, SIAM Journal on Computing, {\bf 11} (1982),  329--343.

\bibitem{Moret__1988}
B. M. E. Moret,
\href{https://doi.org/10.1145/49097.49099}{\it Planar NAE3SAT is in P}, ACM SIGACT News, {\bf 19} (1988),  51--54.

\bibitem{Dyer__Frieze__1986}
M. E. Dyer, A. M. Frieze,
\href{https://doi.org/10.1016/0196-6774(86)90002-7}{\it Planar 3DM is NP-complete}, Journal of Algorithms, {\bf 7} (1986),  174--184.

\bibitem{Hunt__Marathe__1998}
H. B. Hunt III, M. V. Marathe, V. Radhakrishnan, R. E. Stearns,
\href{https://doi.org/10.1137/S0097539793304601}{\it The Complexity of Planar Counting Problems}, SIAM Journal on Computing, {\bf 27} (1998),  1--25.

\bibitem{Goldreich__2008}
O. Goldreich,
\href{https://doi.org/10.1017/CBO9780511804106}{\it Computational Complexity: A Conceptual Perspective}, Cambridge University Press, Cambridge,  2008.

\bibitem{Friedgut__Bourgain__1999}
E. Friedgut, J. Bourgain,
\href{https://doi.org/10.1090/s0894-0347-99-00305-7}{\it Sharp Thresholds of Graph Properties, and the k-Sat Problem}, Journal of the American Mathematical Society, {\bf 12} (1999),  1017--1054.

\bibitem{Chvatal__Reed__1992}
V. Chvatal, B. Reed,
\href{https://doi.org/10.1109/SFCS.1992.267789}{\it Mick gets some (the odds are on his side) (satisfiability)}, Proceedings of the 33rd Annual Symposium on Foundations of Computer Science,  IEEE, Pittsburgh, 1992.

\bibitem{Goerdt__1992}
A. Goerdt,
\href{https://doi.org/10.1007/3-540-55808-X_25}{\it A threshold for unsatisfiability}, Lecture Notes in Computer Science, {\bf 629} (1992),  264--274.

\bibitem{Goerdt__1996}
A. Goerdt,
\href{https://doi.org/10.1006/jcss.1996.0081}{\it A Threshold for Unsatisfiability}, Journal of Computer and System Sciences, {\bf 53} (1996),  469--486.

\bibitem{Bolloba__Borgs__2001}
B. Bollob{\' a}s, C. Borgs, J. T. Chayes, J. H. Kim, D. B. Wilson,
\href{https://doi.org/10.1002/rsa.1006}{\it The scaling window of the 2-SAT transition}, Random Structures \& Algorithms, {\bf 18} (2001),  201--256.

\bibitem{Crawford__Auton__1996}
J. A. Crawford, L. D. Auton,
\href{https://doi.org/10.1016/0004-3702(95)00046-1}{\it Experimental results on the crossover point in random 3-SAT}, Artificial Intelligence, {\bf 81} (1996),  31--57.

\bibitem{Dubois__Boufkhad__2000}
 O. Dubois, Y. Boufkhad, J. Mandler,
\href{https://dl.acm.org/doi/pdf/10.5555/338219.338243}{\it Typical random 3-SAT formulae and the satisfiability threshold}, Proceedings of the eleventh annual ACM-SIAM symposium on Discrete algorithms,  2000.

\bibitem{Kaporis__Kirousis__2006}
A. C. Kaporis, L. M. Kirousis, E. G. Lalas,
\href{https://doi.org/10.1002/rsa.20104}{\it The probabilistic analysis of a greedy satisfiability algorithm}, Random Structures \& Algorithms, {\bf 28} (2001),  444--480.

\bibitem{Mezard__2003}
M. M{\' e}zard,
\href{https://doi.org/10.1007/978-3-0348-7907-1_37}{\it Optimization and Physics: On the Satisfiability of Random Boolean Formulae}, International Conference on Theoretical Physics, Birkh{\" a}user, Basel,  2003, 475--488.

\bibitem{Franco__2005}
J. Franco,
\href{https://doi.org/10.1016/j.dam.2005.05.008}{\it Typical case complexity of Satisfiability Algorithms and the threshold phenomenon}, Discrete Applied Mathematics, {\bf 153} (2005),  89--123.

\bibitem{Fu__Cai__Wu__2024}
H. Fu, S. Cai, G. Wu, J. Liu, X. Yang, Y. Xu,
\href{https://doi.org/10.1016/j.ins.2023.119751}{\it Improving two-mode algorithm via probabilistic selection for solving satisfiability problem}, Information Sciences, {\bf 653} (2024),  119751.

\bibitem{Fu__Xu__Wu__2021}
H. Fu, Y. Xu, G. Wu, J. Liu, S. Chen, X. He,
\href{https://doi.org/10.1016/j.ins.2021.03.009}{\it Emphasis on the flipping variable: Towards effective local search for hard random satisfiability}, Information Sciences, {\bf 566} (2021),  118--139.

\bibitem{Alyahya__Menai__2022}
T. N. Alyahya, M. E. B. Menai, H. Mathkour,
\href{https://doi.org/10.1145/3491210}{\it On the Structure of the Boolean Satisfiability Problem: A Survey}, ACM Computing Surveys, {\bf 55} (2022),  1--34.

\bibitem{Alyahya__Menai__2__2022}
T. Al-Yahya, M. E. B. A. Menai, H. Mathkour,
\href{https://doi.org/10.3390/a15090302}{\it Boosting the Performance of CDCL-Based SAT Solvers by
Exploiting Backbones and Backdoors}, Algorithms, {\bf 15} (2022),  302.

\bibitem{Zhang__Xu__Zhou__2021}
Z. Zhang, D. Xu, J. Zhou,
\href{https://doi.org/10.1007/s11704-021-0318-8}{\it An algorithm for solving satisfiability problem based on the structural information of formulas}, Frontiers of Computer Science, {\bf 15} (2021),  156405.

\bibitem{Newton__Polash__2021}
M. A. H. Newton, M. M. A. Polash, D. N. Pham, J. Thornton, K. Su, A. Sattar,
\href{https://doi.org/10.1007/s10462-021-10024-0}{\it Evaluating logic gate constraints in local search for structured satisfiability problems}, Artificial Intelligence Review, {\bf 54} (2021),  5347--5411.

\bibitem{Ostrowski__Gregoire__2002}
R. Ostrowski, {\' E}. Gr{\' e}goire, B. Mazure, L Sa{\" \i}s,
\href{https://doi.org/10.1007/3-540-46135-3_13}{\it Recovering and Exploiting Structural Knowledge from CNF Formulas}, Lecture Notes in Computer Science, {\bf 2470} (2002),  185--199.

\bibitem{Plaisted__Greenbaum__1986}
D. A. Plaisted, S. Greenbaum,
\href{https://doi.org/10.1016/S0747-7171(86)80028-1}{\it A Structure-preserving Clause Form Translation}, Journal of Symbolic Computation, {\bf 2} (1986),  293--304.

\bibitem{Bearden__Pei__2020}
S. R. B. Bearden, Y. R. Pei, M. Di Ventra,
\href{https://doi.org/10.1038/s41598-020-76666-2}{\it Efficient solution of Boolean satisfiability problems with digital memcomputing}, Scientific Reports, {\bf 10} (2020),  19741.

\bibitem{Cai__Luo__Su__2015}
S. Cai, C. Luo, K. Su,
\href{https://doi.org/10.1093/comjnl/bxu135}{\it Improving WalkSAT By Effective Tie-Breaking and Efficient Implementation}, The Computer Journal, {\bf 58} (2015),  2864--2875.

\bibitem{Fu__Xu__Chen__2020}
H. Fu, Y. Xu, S. Chen, J. Liu,
\href{https://doi.org/10.3897/jucs.2020.013}{\it Improving WalkSAT for Random 3-SAT Problems}, Journal of Universal Computer Science, {\bf 26} (2020),  220--243.


%результатов \cite{Creignou__Hermann__1996} (см. следствие 4.2) и
%\bibitem{Creignou__Hermann__1996}
%N. Creignou, M. Hermann,
%\href{https://doi.org/10.1006/inco.1996.0016}{\it Complexity of Generalized Satisfiability Counting Problems}, Information and Computation, {\bf 125} (1996),  1--12.


%%=====================================================






\end{thebibliography}
\end{document}
