\let\accentvec\vec
\documentclass{llncs}
\usepackage{llncsdoc}
\let\spvec\vec
\let\vec\accentvec

\usepackage{amsmath, amssymb, amsfonts}
\usepackage[pdftex]{graphicx}
\usepackage[english]{babel}

%\usepackage{xcolor}
%\usepackage[pdftex,color,outerbars]{changebar}
%\cbcolor{blue}

\newcommand{\vpi}{\overrightarrow{\pi}}

\newbox\boiteafilets

\newdimen\espaceavecfilets
\newdimen\hautdelaboite
\newdimen\basdelaboite

\newcommand{\boiteavecfilets}[4][B]{%
% Premier argument : le texte.
% Second argument : l'espace entre le texte et les filets
% Troisième argument : la taille des filets
  \setbox\boiteafilets\vbox{\hsize=\linewidth #2}%
  \hautdelaboite=\ht\boiteafilets
  \espaceavecfilets=#3\relax
  \advance\hautdelaboite by \espaceavecfilets
  \basdelaboite=-\espaceavecfilets
  \advance\basdelaboite by -#4
  \par\noindent
  \if#1b{\rlap{\rule[\basdelaboite]{\linewidth}{#4}}}\fi%
  \if#1B{\rlap{\rule[\basdelaboite]{\linewidth}{#4}}}\fi%
  \if#1t{\rlap{\rule[\hautdelaboite]{\linewidth}{#4}}}\fi%
  \if#1B{\rlap{\rule[\hautdelaboite]{\linewidth}{#4}}}\fi%
  \box\boiteafilets
}

\newcounter{PB}
\newdimen\dimboiteinstance
\newdimen\dimautreboite
\newbox\boiteinstance
\newcommand{\PB}[3]{
  \refstepcounter{PB}%
  \par\smallskip%
  \boiteavecfilets{\noindent \textbf{Problem \thePB:} #1}{2pt}{0.4pt}\par\smallskip%
  \boiteavecfilets[b]{\noindent%
    \setbox\boiteinstance\hbox{INSTANCE:\quad}%
    \dimboiteinstance=\wd\boiteinstance
    \dimautreboite=\linewidth%
    \advance\dimautreboite by -\dimboiteinstance%    
    \hbox{\vtop{\hsize\dimboiteinstance\noindent INSTANCE:}\vtop{\hsize\dimautreboite\noindent\ignorespaces#2}}\par
    \hbox{\vtop{\hsize\dimboiteinstance\noindent QUESTION:}\vtop{\hsize\dimautreboite\noindent\ignorespaces#3}}\par\smallskip
  }{0pt}{0.4pt}\par\smallskip%
}


\newcommand{\RAinstance}[3]{
  \begin{list}{}%
    {\renewcommand{\makelabel}[1]{##1\hfil}%
      \settowidth{\labelwidth}{\textbf{Preferences:\ }}%
      \setlength{\leftmargin}{\labelwidth}%
      \setlength{\listparindent}{\parindent}     %
      \setlength{\parsep}{0pt plus 1pt}          %
    }%
  \item[\textbf{Agents:}] #1
  \item[\textbf{Objects:}] #2
  \item[\textbf{Preferences:}] #3  
  \end{list}
}

%\newtheorem{theorem}{Theorem}
%\newtheorem{claim}[theorem]{Claim}
%\newtheorem{corollary}[theorem]{Corollary}
%\newtheorem{lemma}[theorem]{Lemma}
%\theoremstyle{remark}
%\newtheorem{remark}[theorem]{Remark}
%\theoremstyle{definition}
%\newtheorem{definition}[theorem]{Definition}
\newenvironment{proof-sketch}{\noindent{\it Proof sketch.}}{\smallskip}

\selectlanguage{english}
\hyphenation{pre-di-cates}
\hyphenation{pre-di-cate}

\newcommand{\build}{\text{~}|\text{~}}

\title{On the complexity of efficiency and envy-freeness in fair division of
indivisible goods with additive preferences}

\author{Bart de Keijzer\inst{1} \and Sylvain Bouveret\inst{2} \and Tomas Klos\inst{1} \and Yingqian Zhang\inst{1}}

\institute{Delft University of Technology \\
\email{B.deKeijzer@student.tudelft.nl, \textrm{\{}T.B.Klos,Yingqian.Zhang\textrm{\}}@tudelft.nl}
\and Onera-DTIM, Toulouse \\ \email{Sylvain.Bouveret@onera.fr}}

\begin{document}
\pagestyle{plain}
\maketitle

\begin{abstract}
We study the problem of allocating a set of indivisible goods to a
set of agents having additive preferences. We introduce two new
important complexity results concerning efficiency and fairness in
resource allocation problems: we prove that the problem of deciding
whether a given allocation is Pareto-optimal is
\textsf{coNP}-complete, and that the problem of deciding whether
there is a Pareto-efficient and envy-free allocation is
$\Sigma_2^p$-complete.
\end{abstract}

\section{Introduction}\label{section:introduction}
The problem of allocating a set of indivisible goods to a set of
agents arises in a wide range of applications including, among others,
auctions, divorce settlements, frequency allocation, airport traffic
management, fair and efficient exploitation of Earth Observation
Satellites \cite{mara}. In many such real-world problems, one needs to
find \emph{efficient} and \emph{fair} solutions, where an efficient
solution can be seen informally as ensuring the greatest possible
satisfaction to the agents, and where fairness refers to the need for
compromises between the agents' (often antagonistic) objectives.

In this paper, we study the resource allocation problem from the point
of view of computational complexity. We restrict our setting to
\emph{additive} preferences. In other words, the preferences of each
agent are represented by a set of weights $w(o)$, standing for the
utility (or satisfaction) she enjoys for each single object $o$. The
utility of an agent for a subset of objects $S$ is then given by the
sum of the weights of all the objects $o$ in $S$.

Moreover, we restrict our study to two particular definitions of
efficiency and fairness: \emph{Pareto-efficiency} (or
Pareto-optimality) and \emph{envy-freeness}. Pareto-efficient
allocations are such that we cannot increase the satisfaction of an
agent without strictly decreasing the satisfaction of another
agent. An allocation is envy-free if and only if each agent likes her
share at least as much as the share of any other agent.

In this paper, we introduce two new complexity results concerning the
resource allocation problem with additive preferences. Even if the
setting seems restrictive, we advocate that the particular problems we
address are important enough to justify an extensive study for the
following reasons. Firstly, one of the most natural ways of
(compactly) modeling cardinal preferences over sets of objects (or
more generally over combinatorial domains) is to suppose that they are
additive. Notice that this goes far beyond resource allocation:
matching problems, weighted path in a graph, valued constraints
satisfaction problems, etc. Secondly, Pareto-efficiency is one the most
prominent notion of efficiency used in collective decision making
problems. Thirdly, envy-freeness is a key concept in the literature
about resource allocation (see \textit{e.g.} \cite{BramsTaylor96}), as
it provides an elegant way of encoding the notion of fairness and does
not require, contrary to Rawlsian egalitarianism, the interpersonal
comparison of utilities.

This paper contributes to fill a gap. On the one hand resource
allocation with additive preferences have been extensively studied in
economics\footnote{In most social choice studies, utilities stand for
  amounts of money. Thus additivity is a very natural assumption in
  this framework.} (see \textit{e.g.}
\cite{BramsTaylor96,DemkoHill98}), but computational issues (and
\textit{a fortiori} complexity) have rarely been considered. 
On the other hand, computational issues in resource allocation with
additive preferences have been studied extensively in computer science
(see e.g. \cite{ShehoryK98,modi01,deWeerdt07}). However, these
works mainly concern the optimization of the system's performance as a whole. 
The properties of Pareto-efficiency and fairness are rarely addressed.
Two notable exceptions are the work from Lipton \textit{et al.} \cite{LMMS04} that
studies envy-freeness in fair resource allocation problems mainly from
an algorithmic point of view, and the work from Bouveret and Lang \cite{BL-JAIR08} that
introduces complexity results for fair resource allocation problems
under different hypotheses, including additive preferences. In the
latter paper, one result of importance misses, though being
conjectured: the complexity of the problem of deciding whether there
is a Pareto-efficient and envy-free allocation in a resource
allocation problem with additive preferences. This is one of the two main
complexity results introduced in our paper and is studied in section \ref{section:eef-existence}. 
The other main complexity result is about the related problem of deciding whether a given allocation is Pareto-efficient when agents have additive preferences. This result is more easily obtained, and is explained in section \ref{section:paretooptimal}.

\section{Background and notations}\label{preliminaries}

In what follows, we will write vectors using arrowed letters
  (\textit{e.g.} $\overrightarrow{v}$), or brackets for their explicit
  representations (\emph{e.g.} $\langle v_1, \dots, v_n
  \rangle$). $v_i$ will denote the $i^{\text{th}}$ component of a
  vector. Moreover, for any finite set $X$, $|X|$ will denote the
  cardinal of $X$.

In a resource allocation problem, a set of resources must be divided among a set of agents.
Since we will focus on additive utility functions only, it suffices to use the following definition of a resource allocation instance:
\begin{definition}[Resource allocation instance]\label{def:allocationproblem}
  A resource allocation problem is a triple $\mathcal{P} = \langle A, O,
  w \rangle$, where $A$ is a set of \emph{agents},
  $O$ is a set of \emph{indivisible items}, and
  $w: A \times O \to \mathbb{R}$ is a \emph{weight function}.
\end{definition}

We define an allocation as follows:
\begin{definition}[Allocation]
  An allocation for $\mathcal{P} = \langle A, O, w \rangle$ is a
  vector $\vpi = \langle \pi_1, \dots, \pi_n \rangle \in (2^O)^n$ such
  that for all $i, j \in A$, $i \neq j \Rightarrow \pi_i \cap
  \pi_j = \emptyset$. If for every $o \in O$ there exists an $i$ such
  that $o \in \pi_i$ then $\vpi$ is a \emph{complete allocation}.
\end{definition}
Thus, in the problems that we will focus on, the items are non-sharable.

\begin{definition}[Individual utility, utility profile]
  Let $\mathcal{P} = \langle A, O, w \rangle$ be a resource allocation
  instance. For all $i \in A$ and $\pi_i \subseteq O$, $u_i(\pi_i) =
  \sum_{o \in \pi_i} w(i, o)$ is agent $i$'s \emph{individual utility}
  regarding $\pi_i$. Given an allocation $\vpi$, the vector $\langle
  u_1(\pi_1), \dots, u_n(\pi_n) \rangle$ is the \emph{utility profile}
  associated to $\vpi$.
\end{definition}

Two properties that we will focus on, are \textit{Pareto-efficiency} and \textit{envy-freeness}.
\begin{definition}[Pareto-efficiency]
  Let $\vpi, \vpi'$ be two allocations. $\vpi$ \emph{Pareto-dominates} $\vpi'$ if
  and only if (a) for all $i$, $u_i(\pi_i) \geq u_i(\pi_i')$, and (b)
  there exists an $i$ such that $u_i(\pi_i) > u_i(\pi_i')$. $\vpi$ is
  \emph{(Pareto-)efficient} (or \emph{Pareto-optimal}) if and only if there is no $\vpi'$ such
  that $\vpi'$ Pareto-dominates $\vpi$.
\end{definition}

\begin{definition}[Envy \& envy-freeness]
We say that an agent $i \in A$ \textit{envies} another agent $j \in A$ iff $u_i(\pi_j) > u_i(\pi_i)$.
An allocation $\vpi$ is \emph{envy-free} if and only if $u_i(\pi_i) \geq u_i(\pi_j)$ holds for all $i$ and $j \neq i$.
\end{definition}

In this paper, we will refer to some complexity classes
  located in the polynomial hierarchy. We assume that the reader is
  familiar with the complexity class $\mathsf{NP}$ and its
  complementary class $\textsf{coNP}$. $\Sigma_2^p =
  \mathsf{NP}^{\mathsf{NP}}$ is the class of all languages
  recognizable by a nondeterministic Turing machine working in
  polynomial time using $\mathsf{NP}$ oracles. Its complementary class
  is denoted by $\Pi_2^p$.

\section{Complexity of deciding Pareto-optimal allocations for agents with additive utility}
\label{section:paretooptimal}
In this section we prove that it is $\mathsf{coNP}$-complete to decide whether an allocation of resources is Pareto-optimal if the agents have additive utility functions. $\mathsf{coNP}$-completeness has already been proved for a generalized case where agents express their utilities explicitly for each bundle of items \cite{dunne05}. $\mathsf{coNP}$-completeness is also known for the case where the agents have $k$-additive utility functions and $k \geq 2$ \cite{kadditive}.\footnote{Informally, an agent has $k$-additive utility if she has a coefficient associated for every set of $k$ items, and her individual utility is the sum of all coefficients associated to the sets of $k$ items that she gets.} This is not explicitly stated in \cite{kadditive}, but it follows directly from their proof that it is \textsf{NP}-complete to decide whether it is possible to increase the utilitarian collective utility (\textit{i.e.} sum of individual utilities) of a given allocation, when the agents have 2-additive utility functions. In addition to \cite{kadditive}, the problem of maximizing utilitarian collective utility is also explored in \cite{conitzer05}.

The problem we deal with is the following.

\PB{Pareto-optimality with additive utility functions
  (\textsc{po-add})} {A resource allocation instance $\mathcal{P} =
  \langle A, O, w \rangle$, an allocation $\vpi$.}  {Is $\vpi$
  Pareto-optimal?}

\begin{theorem}\label{the:poadd}
  \textsc{po-add} is \textsl{\textsf{coNP}}-complete.
\end{theorem}
Membership of \textsf{coNP} is easy to establish: a nondeterministic Turing machine could guess an allocation $\vpi'$, and check whether $\vpi'$ Pareto-dominates $\vpi$.

To prove \textsf{coNP}-hardness, we give a Karp reduction (\textit{i.e.} polynomial time many-one reduction) from the $\mathsf{coNP}$-complete language \textsc{3unsat}.

\PB{Unsatisfiability of propositional 3CNF formulas (\textsc{3unsat})}
{A set of clauses $C$ denoting a propositional formula in 3CNF.}  {Is $C$ unsatisfiable?}

Let $C$ be a set of propositional clauses of size 3 (we will suppose
w.l.o.g. that the same literal does not appear more than once in each
clause), $L(C)$ be the set of literals in $C$, and $V(C)$ be the set
of variables in $C$. We will write $\mathcal{P}(C)$ to denote the following
resource allocation instance:

\RAinstance { $2|V(C)| + |C| + 2$ agents: $\bigcup_{v \in V(C)} \{a_v,
  \overline{a_v}\} \cup \bigcup_{c \in C} \{a_c\} \cup \{a_{un},
  a_{sat}\}$, }
  { $4|C|+|V(C)|+1$ objects: $\bigcup_{c \in C}
  \{o_{c,l}\ |\ l \in c\} \cup \bigcup_{v \in V(C)} \{o_v\} \cup
  \bigcup_{c \in C} \{o_c\} \cup \{o_{sat}\}$,} {$w(i, o) = 0$ for
  all $i$ and all $o$, except:
  \begin{itemize}
  \item $w(a_v, o_v) = |\{c\ |\ v \in c \in C\}|$, and $w(\overline{a_v},
    o_v) = |\{c\ |\ \neg v \in c \in C\}|$ for all $v \in V(C)$ ;
  \item $w(a_v, o_{c,v}) = 1$ if $v \in c$, and $w(\overline{a_v},
    o_{c,\neg v}) = 1$ if $\neg v \in c$ for each $v \in V(C)$ and each $c \in
    C$ ;
  \item $w(a_c, o_{c, l}) = 1$ for each $c \in C$ and each $l \in c$ ;
  \item $w(a_c, o_c) = 1$ for all $c \in C$ ;
  \item $w(a_{un}, o_v) = 1$ for all $v \in V(C)$ ;
  \item $w(a_{sat}, o_c) = 1$ for all $c \in C$ ;
  \item $w(a_{un}, o_{sat}) = |V(C)| + 1$;
  \item $w(a_{sat}, o_{sat}) = |C|$.
  \end{itemize}
}

Let $I$ be a partial truth assignment of the variables
in $C$. We will define its corresponding allocation $\vpi(I)$ as
follows:
\begin{itemize}
\item $\pi(I)_{a_v} = \{o_v\}$ if $I(v) = \mathbf{true}$ and
  $\pi(I)_{a_v} = \{o_{c,v}\ |\ v \in c \in C\}$ otherwise, for each $v \in V(C)$;
\item $\pi(I)_{\overline{a_v}} = \{o_v\}$ if $I(v) = \mathbf{false}$
  and $\pi(I)_{\overline{a_v}} = \{o_{c,\neg v}\ |\ \neg v \in c \in C\}$ otherwise, for each $v \in V(C)$;
\item for each $c \in C$: $\pi(I)_{a_c} = \{o_c\}$ if $I \not\vDash c$, and $\pi(I)_{a_c} = \{o_{c, l}\ |\ l \in C \wedge I \vDash l\}$ otherwise;
\item $\pi(I)_{a_{un}} = \{o_{sat}\}$ if $I$ is complete, and
  $\bigcup_{v \in V(C), I(v) \not\in \{\mathbf{true},
    \mathbf{false}\}} \{o_v\}$ otherwise;
\item $\pi(I)_{a_{sat}} = \{o_{sat}\}$ if $I$ is partial, and $\{o_c\
  |\ I \vDash C\}$ otherwise.
\end{itemize}
It should be clear that for each assignment $I$, $\vpi(I)$ is well-defined.

Let $I_{\emptyset}$ be the empty assignment (\textit{i.e.} the partial
truth-assignment that leaves all variables unassigned). 
Our reduction transforms a \textsc{3unsat} instance $C$ into the \textsc{po-add}-instance $\langle \mathcal{P}(C), I_{\emptyset} \rangle$.

We will now give an example of this reduction. Consider the \textsc{3unsat} instance given by the set of clauses $\{ c_1 = \{v_1, v_2, \neg v_3 \}, c_2 = \{\neg v_1, \neg v_2, \neg v_3\} \}$.

If we run the reduction process on this instance, we get the \textsc{po-add}-instance that is displayed in the table below. The columns of the table represent the agents and the rows of the table represent the items. The entries in the table are the weights. An entry is displayed in \textit{\textbf{boldface italic}} and between brackets if the item of the corresponding row is allocated to the agent of the corresponding column. Empty cells in the table should be regarded as containing zero-weights.

% Table generated by Excel2LaTeX from sheet 'Sheet1'
\scriptsize{
\begin{center}
\begin{tabular}{r|c|c|c|c|c|c|c|c|c|c|}

           &    $a_{c_1}$ &    $a_{c_2}$ & $a_{v_1}$ & $\overline{a_{v_1}}$ & $a_{v_2}$ & $\overline{a_{v_2}}$ & $a_{v_3}$ & $\overline{a_{v_3}}$ & $a_{un}$ & $a_{sat}$ \\
\hline
   $o_{v_1}$ &            &            &          1 &          1 &            &            &            &            &    \textbf{\textit{[ 1 ]}} &            \\
%\hline
   $o_{v_2}$ &            &            &            &            &          1 &          1 &            &            &    \textbf{\textit{[ 1 ]}} &            \\
%\hline
   $o_{v_3}$ &            &            &            &            &            &            &            &          2 &    \textbf{\textit{[ 1 ]}} &            \\
\hline
   $o_{c_1}$ &    \textbf{\textit{[ 1 ]}} &            &            &            &            &            &            &            &            &          1 \\
%\hline
   $o_{c_2}$ &            &    \textbf{\textit{[ 1 ]}} &            &            &            &            &            &            &            &          1 \\
\hline
$o_{c_1,v_1}$ &          1 &            &    \textbf{\textit{[ 1 ]}} &            &            &            &            &            &            &            \\
%\hline
$o_{c_1,v_2}$ &          1 &            &            &            &    \textbf{\textit{[ 1 ]}} &            &            &            &            &            \\
%\hline
$o_{c_1,\neg v_3}$ &          1 &            &            &            &            &            &            &    \textbf{\textit{[ 1 ] }} &            &            \\
%\hline
$o_{c_2,\neg v_1}$ &            &          1 &            &    \textbf{\textit{[ 1 ]}} &            &            &            &            &            &            \\
%\hline
$o_{c_2,\neg v_2}$ &            &          1 &            &            &            &    \textbf{\textit{[ 1 ]}} &            &            &            &            \\
%\hline
$o_{c_2,\neg v_3}$ &            &          1 &            &            &            &            &            &    \textbf{\textit{[ 1 ] }} &          &            \\
\hline
$o_{sat}$ &            &            &            &            &            &            &            &            &          4 &    \textbf{\textit{[ 2 ]}} \\
\hline
\end{tabular}  
\end{center} 
}
\normalsize

\begin{lemma}\label{lem:01}
For each model $M$ for $C$, $\vpi(M)$ Pareto-dominates $\vpi(I_{\emptyset})$.
\end{lemma}
\begin{proof}
In $\vpi(M)$, agent $a_{un}$ has strictly higher utility: $u_{a_{un}}(\pi(M)_{a_{un}}) = |C|+1$, while $u_{a_{un}}(\pi(I_{\emptyset})_{a_{un}}) = |C|$.
By definition of $\vpi(M)$, the utility of all other agents is in $\vpi(M)$ at least as high as in $\vpi(I_{\emptyset})$. \qed
\end{proof}

\begin{lemma}\label{lem:02}
If $C$ is unsatisfiable, then $\vpi(I_{\emptyset})$ is Pareto-optimal.
\end{lemma}
\begin{proof}
Suppose for contradiction that there is an allocation $\vpi'$ that Pareto-dominates $\vpi(I_{\emptyset})$.

There is at least one
    agent $a$ such that $u_a(\pi_a') > u_a(\pi(I_{\emptyset})_a)$. It
    can be easily proved that, starting from $I_{\emptyset}$, strictly
    increasing the utility of any agent in $A \setminus \{a_{un},
    a_{sat}\}$ implies reallocating at least one item $o_v$ from agent
    $a_{un}$'s share to another agent. Then, the only solution for not
    decreasing $a_{un}$'s utility is to give her $o_{sat}$.

So then $\{o_c\ |\ c \in C \} \in \pi_{a_{sat}}'$. Consequently, for all $a_{c}$ with $c \in C$ we must have $|\{ o_{c,l} \ |\ l \in c \wedge o_{c,l} \in \pi_{a_{c}}' \}| \geq 1$. Let $o \in \{ o_{c,l} \ |\ l \in c \wedge o_{c,l} \in \pi_{a_{c}}' \}$. Let $a'$ be the agent for which it holds that $o \in \pi(I_{\emptyset})_{a'}$ (so $a' \in \{a_v, \overline{a_v} \}$). Let $\overline{a'}$ be the agent in $\{a_v, \overline{a_v} \}$ that does not equal $a'$. It must now be that $o_v \in \pi_{a'}'$, and as a consequence we now know that $\pi(I_{\emptyset})_{\overline{a}} = \pi_{\overline{a}}'$.

So, for each $v \in V(C)$ there are no two objects $o_{c, v}$ and $o_{c', \neg v}$ with $v \in c$, $\neg v \in c'$, and $c, c' \in C$ such that $o_{c,v} \in \pi_{a_c}$ and $o_{c', \neg v} \in \pi_{a_{c'}}'$. It then follows immediately from the construction of the reduction that there is a complete interpretation $I$ such that $\vpi' = \vpi(I)$. Moreover, one can check that $I \vDash c$ for each $c \in C$. Therefore, $I$ is a model of $C$, and we have a contradiction. \qed
\end{proof}

\begin{proof}[Theorem~\ref{the:poadd}]
  Let $C$ be a set of clauses of size 3. By Lemma~\ref{lem:01} and
  \ref{lem:02}, we have that $C$ is unsatisfiable if and only if
  $\vpi(I_{\emptyset})$ is a Pareto-optimal allocation for
  $\mathcal{P}(C)$. The reduction from $C$ to $\langle \mathcal{P}(C),
  \vpi(I_{\emptyset}) \rangle$ can clearly be done in polynomial time, hence \textsf{coNP}-hardness is proved. \qed
\end{proof}

\section{Complexity of deciding existence of efficient \& envy-free allocations for agents with additive utility}\label{section:eef-existence}
For this section, we are interested in finding allocations that are both Pareto-efficient and envy-free.

We will now state the problem and prove that this problem is $\Sigma_2^p$-complete.
\PB{Efficient \& envy-free allocation existence with additive utility functions (\textsc{$\exists$-eef-add})} 
{A resource allocation instance $\mathcal{P} = \langle A, O, w \rangle$.} 
{Does there exist an allocation that is both Pareto-efficient and envy-free?}

\begin{theorem}\label{the:eefadd}
\textsc{$\exists$-eef-add} is $\Sigma_2^p$-complete.
\end{theorem}
We will prove $\Sigma_2^p$-completeness by a Karp reduction from the complement of the $\Pi_2^p$-complete language \textsc{$\forall \exists$3cnf} \cite{polyhierarchy}.

\PB{Doubly quantified 3CNF satisfiability (\textsc{$\forall \exists$3cnf})}
{A set $V_{\forall}$ of propositional variables, a set $V_{\exists}$ of propositional variables, a set $C$ of clauses of three literals over the variables $V_{\forall} \cup V_{\exists}$.} 
{Does there exist for each assignment to the variables in $V_{\forall}$ an assignment to the variables in $V_{\exists}$ that satisfies $C$?}

Let $F = \langle V_{\forall} , V_{\exists}, C \rangle$ be an instance of \textsc{$\forall \exists$3cnf}.
We will assume w.l.o.g. that every possible literal occurs at least once in $C$, and that a literal does not appear more than once in each clause. Let $\text{\#occ}{\forall}$ be the number of literal occurrences in $C$ of variables in $V_{\forall}$.
We will write $L_\forall$ and $L_\exists$ for the sets of literals of variables in $V_\forall$ and $V_\exists$ respectively.
 We will write $\mathcal{P}(F)$ to denote the following resource allocation instance (also see the example that follows after Definition \ref{VA-allocations}):

\RAinstance { $4|V_{\forall}| + 2|V_{\exists}| + |C| + \text{\#occ}{\forall} + 3$ agents: $\bigcup_{v \in V_{\forall}} \{a_v^+, a_v^{+cl}, a_v, \overline{a_v}\} \cup \bigcup_{v \in V_{\exists}} \{a_v, \overline{a_v}\} \bigcup_{c \in C} \{a_c\} \cup \bigcup_{c \in C} \{a_{c,l}^{en}\ |\ l \in c \cap L_{\forall} \} \cup \{a_{un}, a_{sat}, a_{en}\}$ } 
{ $4|V_{\forall}| + |V_{\exists}| + 5|C| + L_{\forall} + 3$ objects: $\bigcup_{v \in V_{\forall}} \{o_v^{en}, o_v^{cmp}, o_v^h, \overline{o_v^h}\} \cup \bigcup_{v \in V_{\exists}} \{o_v\} \cup \bigcup_{c \in C, l \in c} \{o_c, o_c^{cmp} o_{c,l}\} \cup \bigcup_{c \in C} \{o_{c,l}^{en}\ |\ l \in c \cap L_{\forall} \} \cup \{o_{sat}, o_{en1}, o_{en2}\}$ }
{$w(i, o) = 0$ for all $i$ and all $o$, except:
  \begin{itemize}
  \item For all $v \in V_{\forall}$ and $o \in \{o_v^{en}, o_v^c, o_v^h, \overline{o_v^h}\}$: $w(a_v^+, o) = 1$ and $w(a_v^{+cl}, o) = 1$;\footnote{So, $a_v^{+cl}$ is a \textit{cl}one of $a_v^{+}$.} 
  \item For all $v \in V_{\forall}$: $w(a_v, o_v^h) = |\{c\ |\ v \in c\}|$, $w(\overline{a_v}, \overline{o_v^h}) = |\{c\ |\ \neg v \in c\}|$, $w(a_v, o_{c,v}) = 1$ for all $c \in C$ where $v \in c$, and $w(\overline{a_v}, o_{c,\neg v}) = 1$ for all $c \in C$ where $\neg v \in c$;
  \item For all $v \in V_{\exists}$: $w(a_v, o_v) = |\{c\ |\ v \in c\}|$, $w(\overline{a_v}, o_v) = |\{c\ |\ \neg v \in c\}|$, $w(a_v, o_{c,v}) = 1$ for all $c \in C$ where $v \in c$, and $w(\overline{a_v}, o_{c,\neg v}) = 1$ for all $c \in C$ where $\neg v \in c$;
  \item For all $c \in C$: $w(a_c, o_c) = M$, $w(a_c, o_c^{cmp}) = M-1$, and $w(a_c, o_{c,l}) = 1$ for all $l \in c$;
  \item For all $(c,l)$ where $c \in C$, $l \in c \cap L_{\forall}$: $w(a_{c,l}^{en}, o_c) = M$, $w(a_{c,l}^{en}, o_{c,l}) = 1$, $w(a_{c,l}^{en}, o_{c,l}^{en}) = M$;
  \item For all $c \in C$: $w(a_{sat}, o_c) = 1$, $w(a_{sat}, o_{sat}) = |C|$, $w(a_{sat}, o_{en1}) = \frac{1}{2}$;
  \item For all $c \in C$: $w(a_{un}, o_c^{cmp}) = 1$; For all $v \in V_{\forall}$: $w(a_{un}, o_v^{cmp}) = 1$; For all $v \in V_{\exists}$: $w(a_{un}, o_v) = 1$; 
  \item $w(a_{un}, o_c^{sat}) = |V_{\exists}| + |V_{\forall}| + |C| + 1$; $w(a_{un}, o_{en1}) = 2(|V_{\exists}| + |V_{\forall}| + |C| + 1)$; $w(a_{un}, o_{en2}) = 3(|V_{\exists}| + |V_{\forall}| + |C| + 1) - 1$; $w(a_{en}, o_{en2}) = M$;
  \end{itemize}
  where $M$ is a large number. It suffices to take for $M$ the sum of all weights that are not defined in terms of $M$.
}

For our proof that \textsc{$\exists$-eef-add} is $\Sigma_2^p$-complete, we need the notion of a special type of allocation for $\mathcal{P}(F)$. An example of an $X_{\forall}$-allocation is given in the example-instance that follows after this proof.
\begin{definition}[$V_{\forall}$-assignments and $V_{\forall}$-allocations]
\label{VA-allocations}
For $F$, we define a {\it $V_{\forall}$-assignment} as any complete assignment to the variables in $V_{\forall}$ only. Given a $V_{\forall}$-assignment $I$, we define a corresponding allocation $\vpi(I)$ for $\mathcal{P}(F)$ in the following way:
\begin{itemize}
\item $\pi(I)_{a_{v}^+} = \{o_v^{en}\}$ for each $v \in V_{\forall}$;
\item $\pi(I)_{a_{v}^{+cl}} = \{o_v^h\}$ if $I(v) = \mathbf{true}$ and $\{\overline{o_v^h}\}$ otherwise, for each $v \in V_{\forall}$;
\item $\pi(I)_{a_{v}} = \{o_{c,v}\ |\ v \in c \} \cup \{o_v^{h}\}$ if $I(v) = \mathbf{false}$, and $\{o_{c,v}\ |\ v \in c \}$ otherwise, for each $v \in V_{\forall}$;
\item $\pi(I)_{\overline{a_{v}}} = \{o_{c,\neg v}\ |\ \neg v \in c \} \cup \{\overline{o_v^{h}}\}$ if $I(v) = \mathbf{true}$, and $\{o_{c,\neg v}\ |\ \neg v \in c\}$ otherwise, for each $v \in V_{\forall}$;
\item $\pi(I)_{a_{v}} = \{o_{c,l}\ |\ l \in c \}$ for each $l \in L_{\exists}$;
\item $\pi(I)_{a_{c}} = \{o_c\}$ for each $c \in C$;
\item $\pi(I)_{a_{c,l}^{en}} = \{o_{c,l}^{en}\}$ for each $c,l$ where $c \in C$ and $l \in c \cap L_{\forall}$;
\item $\pi(I)_{a_{un}} = \{ o_c^{cmp}\ |\ c \in C \} \cup \{o_v\ |\ v \in V_{\exists}\} \cup \{ o_v^{cmp}\ |\ v \in V_{\forall}\} \cup \{o_{en1}\}$;
\item $\pi(I)_{a_{sat}} = \{o_{sat}\}$; 
\item $\pi(I)_{a_{en}} = \{o_{en2}\}$;
\end{itemize}
Given a $V_{\forall}$-assignment $I$, we define the set of $V_{\forall}$-allocations corresponding to $I$ as follows: any allocation that can be obtained from $\pi(I)$ by a sequence of swaps of the bundles of $a_v^+$ and $a_v^{+cl}$ for any $v \in V_{\forall}$, followed by a sequence of reallocations of $o_{c,l}$ to $a_{c,l}^{en}$ for any $l,c$ with $c \in C$, $l \in c \cap L_{\forall}$, and $I \not\vDash l$.\footnote{To remove any confusion, see the example allocation that follows, together with the explanation.}
\end{definition}

Let us give an example of this reduction, together with a $V_{\forall}$-allocation. Let the \textsc{$\forall \exists$3cnf}-instance be $F = \langle V_{\forall} = \{v_1\}, V_{\exists} = \{v_2\}, C = \{c_1 = \{v_1, \neg v_1, v_2 \}, c_2 = \{v_2, \neg v_2, v_1\} \}\rangle$. Then $\mathcal{P}(F)$ looks as follows.
% Table generated by Excel2LaTeX from sheet 'Sheet1'
\scriptsize{
\begin{center}
\begin{tabular}{r|c|c|c|c|c|c|c|c|c|c|c|c|c|c|}

           &    $a_{c_1}$ &    $a_{c_2}$ & $a_{v_1}^+$ & $a_{v_1}^{+cl}$ & $a_{v_1}$ & $\overline{a_{v_1}}$ & $a_{v_2}$ & $\overline{a_{v_2}}$ & $a_{c_1, v_1}^{en}$ & $a_{c_1, \neg v_1}^{en}$ & $a_{c_2, v_1}^{en}$ & $a_{un}$ & $a_{sat}$ & $a_{en}$ \\
\hline
   $o_{c_1}$               & \textbf{\textit{[ M ]}} &         &         &         &         &         &         &         &       M &       M &         &          &              1 &         \\
%\hline
   $o_{c_2}$               &         & \textbf{\textit{[ M ]}} &         &         &         &         &         &         &         &         &       M &          &              1 &         \\
\hline
   $o_{c_1}^{cmp}$         &     M-1 &         &         &         &         &         &         &         &         &         &         &  \textbf{\textit{[ 1 ]}} &                &         \\
%\hline
   $o_{c_2}^{cmp}$         &         &     M-1 &         &         &         &         &         &         &         &         &         &  \textbf{\textit{[ 1 ]}} &                &         \\ 
\hline
   $o_{c_1,v_1}$           &       1 &         &         &         &       1 &         &         &         & \textbf{\textit{[ 1 ]}} &         &         &          &                &         \\
%\hline
   $o_{c_1,\neg v_1}$      &       1 &         &         &         &         & \textbf{\textit{[ 1 ]}} &         &         &         &       1 &         &          &                &         \\
%\hline
   $o_{c_1,v_2}$           &       1 &         &         &         &         &         & \textbf{\textit{[ 1 ]}} &         &         &         &         &          &                &         \\
%\hline
   $o_{c_2,v_2}$           &         &       1 &         &         &         &         & \textbf{\textit{[ 1 ]}} &         &         &         &         &          &                &         \\
%\hline
   $o_{c_2,\neg v_2}$      &         &       1 &         &         &         &         &         & \textbf{\textit{[ 1 ]}} &         &         &         &          &                &         \\
%\hline
   $o_{c_2,v_1}$           &         &       1 &         &         &       1 &         &         &         &         &         & \textbf{\textit{[ 1 ]}} &          &                &         \\
\hline
   $o_{v_1}^h$             &         &         &       1 &       1 & \textbf{\textit{[ 2 ]}} &         &         &         &         &         &         &          &                &         \\
%\hline
   $\overline{o_{v_1}^h}$  &         &         & \textbf{\textit{[ 1 ]}} &       1 &         &       1 &         &         &         &         &         &          &                &         \\
%\hline
   $o_{v_1}^{en}$          &         &         &       1 & \textbf{\textit{[ 1 ]}} &         &         &         &         &         &         &         &          &                &         \\
%\hline
   $o_{v_1}^{cmp}$         &         &         &       1 &       1 &         &         &         &         &         &         &         &  \textbf{\textit{[ 1 ]}} &                &         \\
\hline
   $o_{v_2}$               &         &         &         &         &         &         &       2 &       1 &         &         &         &  \textbf{\textit{[ 1 ]}} &                &         \\
\hline
   $o_{c_1,v_1}^{en}$      &         &         &         &         &         &         &         &         & \textbf{\textit{[ M ]}} &         &         &          &                &         \\
%\hline
   $o_{c_1,\neg v_1}^{en}$ &         &         &         &         &         &         &         &         &         & \textbf{\textit{[ M ]}} &         &          &                &         \\
%\hline
   $o_{c_2,v_1}^{en}$      &         &         &         &         &         &         &         &         &         &         & \textbf{\textit{[ M ]}} &          &                &         \\
\hline
   $o_{sat}$               &         &         &         &         &         &         &         &         &         &         &         &        5 &        \textbf{\textit{[ 2 ]}} &         \\
\hline
   $o_{en1}$               &         &         &         &         &         &         &         &         &         &         &         & \textbf{\textit{[ 10 ]}} & $\frac{1}{2}$ &         \\
\hline
   $o_{en2}$               &         &         &         &         &         &         &         &         &         &         &         &       14 &                & \textbf{\textit{[ M ]}} \\
\hline
\end{tabular}  
\end{center} 
}
\normalsize
A $V_{\forall}$-allocation corresponding to a $V_{\forall}$-assignment $I$ with $I(v_1) = \mathbf{false}$ is displayed in \textit{\textbf{boldface italic}} and between brackets. This allocation has been obtained from $\pi(I)$ by swapping the bundles of $a_{v_1}^+$ and $a_{v_1}^{+cl}$, and reallocating item $o_{c_1,v_1}$ to $a_{c_1,v_1}^{en}$, and item $o_{c_2,v_1}$ to $a_{c_2,v_1}^{en}$.

In the following proofs, we will restrict attention to
  \emph{non-wasting} allocations, that is, allocations $\pi$ such that
  for all $(o, a) \in O \times A$, $o \in \pi(a) \Rightarrow w(a, o) >
  0$. It is obvious that every Pareto-efficient allocation is a
  non-wasting one.

\begin{lemma}
\label{correctness1}
Let $\vpi$ be an allocation. $\vpi$ is envy-free if and only if $\vpi$ is a $V_{\forall}$-allocation.
\end{lemma}
\begin{proof}
($\Leftarrow$) For any arbitrary $V_{\forall}$-allocation, it is easy (although a bit tedious) to check for each type of agent that she does not envy any other agent.

($\Rightarrow$) We show this by reasoning about how resources should be allocated in order to prevent envy. We start by noticing that $o_{en2}$ must necessarily be allocated to $a_{en}$. As a consequence $o_{en1}$ must be allocated to $a_{un}$, after which $o_{sat}$ should go to $a_{sat}$. In order prevent $a_{un}$ from envying $a_{en}$, we should give $a_{un}$ all remaining items for which his weight is positive. Now that we know we cannot allocate $o_c^{cmp}$ to $a_c$ (for any $c \in C$), we must give $o_c$ to $a_c$. For the same reason, for all $v \in V_{\exists}$ we cannot give $o_{v}$ to $a_{v}$ or $\overline{a_v}$, thus these agents should receive all remaining resources for which they have a positive weight. Next, we notice that we should give $o_{c,l}^{en}$ to $a_{c,l}^{en}$ because $a_{c,l}^{en}$ is the only agent with positive weight for this item. Now we see that for all $c,l$ with $l \in c \cap L_{\forall}$ and $c \in C$, we cannot give $o_{c,l}$ to $a_c$, because $a_{c,l}^{en}$ would then envy $a_c$. Next, for all $v \in V_{\forall}$ we must allocate $o_v^{en}$ to either $a_v^{+}$ or $a_v^{+cl}$. Because the weights of both agents are exactly the same, suppose w.l.o.g. that we allocate $o_v^{en}$ to $a_v^{+}$. In order to prevent envy between the two agents, we need to allocate either $o_v^h$ or $\overline{o_v^h}$ (but not both) to $a_v^{+cl}$ (we denote by $o$ this item and $\overline{o}$ the other one of the pair). Since $\overline{o}$ cannot be allocated to $a_v^{+}$ nor to $a_v^{+cl}$, $\overline{o}$ must go to $a_v$ if $\overline{o} = o_v^h$ and $\overline{a_v}$ otherwise. There is only one agent left that we can allocate $o$ to. Lastly, let $a \in \{a_v, \overline{a_v} \}$ be the agent that does not get $\overline{o}$. All items that $a$ has positive weight for should now be allocated to $a$, in order to prevent $a$ from envying the agent that gets $\overline{o}$. 

The restrictions that we just deduced, restrict the set of possibly efficient and envy-free allocations to the set of $V_{\forall}$-allocations. \qed
\end{proof}

\begin{lemma}
\label{correctness2}
No two $V_{\forall}$-allocations dominate each other.
\end{lemma}
\begin{proof}
Let $\vpi$ and $\vpi'$ be two $V_{\forall}$-allocations.
If $\vpi$ and $\vpi'$ correspond to the same $V_{\forall}$-assignment, then $\vpi$ does not dominate $\vpi'$ because swapping the bundles of $o_v^+$ and $o_v^{+cl}$ for any $v \in V_{\forall}$ does not increase nor decrease the utility of both agents. Reallocating $o_{c,l}$ between the agents $a_{c,l}^{en}$ and $a_v$ (or $\overline{a_v}$) for any $l,c$ with $l \in c \cap L_{\forall}$ and $c \in C$ can never result in a dominating allocation either, because both agents have exactly the same weights for all of these items.

For the case that $\vpi$ and $\vpi'$ correspond to different $V_{\forall}$-assignments, let $I$ and $I'$ be the two $V_{\forall}$-assignments respectively, and let $v$ be a variable such that $I(v) \not= I'(v)$. We will show that $\vpi$ does not Pareto-dominate $\vpi'$. Assume w.l.o.g. that $I(v) = \mathbf{true}$ and $I'(v) = \mathbf{false}$.
In $\vpi$ we have that $\overline{o_v^h}$ is allocated to $\overline{a_v}$; in $\vpi'$ this is not the case. Because of the weights that $\overline{a_v}$ has, we now know that $u_{\overline{a_v}}(\pi_{\overline{a_v}}) \leq u_{\overline{a_v}}(\pi_{\overline{a_v}}')$.
We can divide this up in two cases: in the case that $u_{\overline{a_v}}(\pi_{\overline{a_v}}) < u_{\overline{a_v}}(\pi_{\overline{a_v}}')$, we have immediately that $\vpi$ does not Pareto-dominate $\vpi'$. In the other case that $u_{\overline{a_v}}(\pi_{\overline{a_v}}) = u_{\overline{a_v}}(\pi_{\overline{a_v}}')$, any item $o_{c, \neg v}$ in the set $\{ o_{c,\neg v} \ |\ v \in c \in C \}$ is allocated to $a_{c, \neg v}^{en}$ under allocation $\vpi$, but not under allocation $\vpi'$, so in this case we have $u_{\overline{a_{c,\neg v}}}(\pi_{\overline{a_{c, \neg v}}}) < u_{\overline{a_{c,\neg v}}}(\pi_{\overline{a_{c, \neg v}}}')$, hence $\vpi$ does not Pareto-dominate $\vpi'$. \qed
\end{proof}

\begin{lemma}
\label{correctness3}
Given a $V_{\forall}$-assignment $I$ for $F$, and a $V_{\forall}$-allocation $\vpi$ for $\mathcal{P}(F)$ that corresponds to $I$; if $C$ is satisfiable on $I$ (\textit{i.e.} $I$ can be extended such that $C$ is satisfied), then there is an allocation $\vpi'$ that Pareto-dominates $\vpi$.
\end{lemma}
\begin{proof}
Let $I'$ be a complete assignment that satisfies $C$ such that $I \subseteq I'$.
The following allocation $\vpi'$ Pareto-dominates $\vpi$.
\begin{itemize}
\item For all $c \in C$: $\pi_c' = \{o_{c,l}\ |\ l \in c \wedge I' \vDash l \} \cup \{o_{c}^{cmp} \}$.
\item For all $v \in V_{\forall}$: Let $a = a_v$, $\overline{a} = \overline{a_v}$, $o = o_v^h$ if $I(v) = \mathbf{true}$, and let $a = \overline{a_v}$, $\overline{a} = a_v$, $o = \overline{o_v^h}$ otherwise. $\pi_{a}' = \{o\}$ and $\pi_{\overline{a}}' = \pi_{\overline{a}}$. Moreover, if $o \in \pi_{a_v^+}$ then $\pi_{a_v^+}' = \pi_{a_v^+} \backslash \{o\} \cup \{o_v^{cmp}\}$ and $\pi_{a_v^{+cl}}' = \pi_{a_v^{+cl}}$; otherwise $\pi_{a_v^{+cl}}' = \pi_{a_v^{+cl}} \backslash \{o\} \cup \{o_v^{cmp}\}$ and $\pi_{a_v^+}' = \pi_{a_v^+}$.
\item For all $v \in V_{\exists}$: If $I'(v) = \mathbf{true}$, then $\pi_{a_v}' = \{o_v\}$ and $\pi_{\overline{a_v}}' = \pi_{\overline{a_v}}$; otherwise $\pi_{\overline{a_v}}' = \{o_v\}$ and $\pi_{a_v}' = \pi_{a_v}$.
\item For all $c,l$ such that $c \in C$ and $l \in c \cap L_{\forall}$: $\pi_{a_{c,l}^{en}}' = \pi_{a_{c,l}^{en}}$.
\item $\pi_{a_{un}}' = \{o_{sat}, o_{en1} \}$; $\pi_{a_{sat}}' = \{o_c\ |\ c \in C\}$; $\pi_{a_{en}}' = \{o_{en2}\}$.
\end{itemize}
In $\vpi'$, the utility of $a_{un}$ is strictly higher than in $\vpi$. Moreover, one can easily check that in $\vpi'$ the utilities of all other agents are at least as high as in $\vpi$. \qed
\end{proof}

\begin{lemma}
\label{correctness4}
Given a $V_{\forall}$-assignment $I$ for $F$, and a $V_{\forall}$-allocation $\vpi$ in $\mathcal{P}(F)$ that corresponds to $I$; if $C$ is unsatisfiable on $I$, then $\vpi$ is Pareto-efficient.
\end{lemma}
\begin{proof}
We will first show that in any $\vpi'$ that Pareto-dominates $\vpi$ we necessarily have $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$.
We do this by exhaustion on the type of agent. Let $\vpi'$ Pareto-dominate $\vpi$. 
Let $a$ be an agent such that $u_a(\pi_a') > u_a(\pi_a)$. We show for each of the following cases of $a$ that necessarily $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$.
\begin{description}
\item[Case 1: $a = a_{un}$:] In this case we clearly have $o_{sat} \in \pi_a'$, and because $w(a_{sat}, o_{sat}) = |C|$ we have as a consequence that $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$.
\item[Case 2: $a \in \{a_v, \overline{a_v}\ |\ v \in V_{\exists}\}$:] Let $a = a_v$ for an arbitrary $v \in V_{\exists}$ (the case that $a = \overline{a_v}$ is analogous). It must be that $o_v \in \pi_a'$, so then, since $o_v$ has been removed from $a_{un}$'s share, we need to give her $o_{sat}$ as a compensation. From the argument in the previous case we get $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$. 
\item[Case 3: $a \in \{a_v^+\, a_v^{+cl} |\ v \in V_{\forall} \}$:] Let $a = a_v^+$ for an arbitrary $v \in V_{\forall}$ (the case that $a = a_v^{+cl}$ is analogous). Assume w.l.o.g. that $I(v) = \mathbf{true}$. Because $a_v^+$ and $a_v^{+cl}$ have identical weights, we may also w.l.o.g. assume that $\pi_{a_v^+}' \cap \pi_{a_v^{+cl}} = \emptyset$. If $o_v^{cmp} \in \pi_a'$, then from the argument in case 1 it follows that $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$. If $\overline{o_v^{h}} \in \pi_a'$, then it must be that $\{o_{c,\neg v}\ |\ \neg v \in c \in C \} \cap \pi_{\overline{a_{v}}} = \emptyset$ and $\{o_{c,\neg v}\ |\ \neg v \in c \in C \} \subseteq \pi_{\overline{a_{v}}}'$. Thus, for all $c \in C$ with $\neg v \in c$, we have $o_c \in \pi_{a_{c,\neg v}^{en}}'$. Consequently, we get $o_c^{cmp} \in \pi_{a_{c}}'$; and therefore by our argument that we gave in Case 1, $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$.
\item[Case 4: $a \in \{a_v, \overline{a_v}\ |\ v \in V_{\forall} \}$:] Assume w.l.o.g. that $I(v) = \mathbf{true}$. For any arbitrary $v \in V_{\forall}$, let $a = \overline{a_v}$. From the last part of the argument that we gave for the previous case, it follows directly that $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$. Now let $a = a_v$. Necessarily we have $o_v^h \in \pi_{a_v}'$, and from our reasoning in Case 3 it follows that $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$.
\item[Case 5: $a \in \{a_c\ |\ c \in C \}$:] Let $a = a_c$ for an arbitrary $c \in C$. If $o_c^{cmp} \in \pi_{a_{c}}'$, it follows from Case 1 that $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$. If $o_{c,l} \in \pi_{a_{c}}'$ then the same conclusion follows, but this time from the last part of the proof of Case 3.
\item[Case 6: $a \in a_{c,l}^{en}\ |\ c \in C \wedge l \in c \cap L_{\forall} \}$:] Let $a = a_{c,l}^{en}$ for an arbitrary $c,l$ with $c \in C$ and $l \in c \cap L_{\forall}$. We must have that $o_{c} \in \pi_{a_{c,l}^{en}}'$ or $o_{c,l} \in \pi_{a_{c,l}^{en}}'$ (or both), in both cases it follows from the last part of the proof of Case 3 that $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$.
\item[Case 7: $a = a_{sat}$:] Let $C'$ be any strict subset of $C$. If $\{o_c\ |\ c \in C'\} \subseteq \pi_a'$, then $\forall c \in C : o_c^{cmp} \in a_c$, so by the arguments in Case 1, $\{o_c\ |\ c \in C\} \subseteq \pi_a'$. If $o_{en1} \in \pi_a'$, then the same follows, also from the proof in Case 1.
\item[Case 8: $a = a_{en}$:] This case is obviously impossible.
\end{description}

Now we will finish the proof by obtaining the contradiction that an extension $I'$ of $I$ can be made to the variables in $V_{\exists}$, such that $I'$ satisfies $C$.

Recall that we assume that $\vpi'$ Pareto-dominates $\vpi$, and as we have just shown, $\{o_c\ |\ c \in C \} \subseteq \pi_{a_{sat}}'$. For all $c \in C : o_c^{cmp} \cup L_c \subseteq \pi_{a_c}'$, where $L_c$ is any subset of $\{o_{c,l}\ |\ l \in c\}$. Let $o_{c,l} \in L_c$ and let $v \in l$. There are two cases: either $v \in V_{\forall}$ or $v \in V_{\exists}$. 

Suppose $v \in V_{\forall}$. Let $a = a_{v}$, $\overline{a} = \overline{a_v}$ if $I(v) = \mathbf{true}$, and let $a = \overline{a_v}$, $\overline{a} = a_v$ otherwise. It is easy to see that $\not\exists o_{c,l} \in L_c : o_{c,l} \in \pi_{a_{c,l}^{en}}$ and $\not\exists o_{c,l} \in L_c : o_{c,l} \in \pi_{\overline{a}}$, so $o_{c,l} \in \pi_{a}$. As a consequence, we know that $l$ is satisfied by $I$. Hence, it must hold that if $o_{c,l} \in L_c$, then $c$ is satisfied by $I$.

Suppose $v \in V_{\exists}$. Let $a = \overline{a_{v}}$ if $l = \neg v$ and let $a = a_v$ otherwise. Then it must be that $o_{c,l} \in \pi_{a}$ and $o_v \in \pi_{a}'$. 

From the construction of the reduction, it follows that there must exist an assignment to the variables in $V_{\exists}$ that satisfies all clauses not satisfied by $I$, \textit{i.e.}, we obtain the contradiction that $C$ is satisfiable on $I$. \qed
\end{proof}

\begin{proof}[Theorem~\ref{the:eefadd}]
Membership is easily established: A nondeterministic $\mathsf{NP}^{\mathsf{NP}}$ Turing machine that decides this problem could work as follows. On input $\langle A, \mathcal{O}, w \rangle$:
\begin{enumerate}
 \item Guess an allocation $\vpi$.
 \item Check whether $\vpi$ is envy-free. If not, then REJECT.
 \item Check whether $\vpi$ is Pareto-optimal by querying the oracle. If it is, then ACCEPT. Otherwise, REJECT.
\end{enumerate}
The difficult part is proving $\Sigma_2^p$-hardness.

Given a \textsc{$\forall \exists$3cnf}-instance $F = \langle V_{\forall}, V_{\exists}, C \rangle$, we can clearly construct $\mathcal{P}(F)$ in polynomial time.

If $F$ is a NO-instance of \textsc{$\forall \exists$3cnf}, then there is a $V_{\forall}$-assignment $I$ that cannot be extended to an assignment that satisfies $C$. Let $\vpi$ be a $V_{\forall}$-allocation for $\mathcal{P}(F)$ that corresponds to $I$. By Lemma \ref{correctness1}, $\vpi$ is envy-free and by Lemma \ref{correctness4}, $\vpi$ is Pareto-efficient. Hence, $\mathcal{P}(F)$ is a YES-instance of \textsc{$\exists$-eef-add}.

If $F$ is a YES-instance of \textsc{$\forall \exists$3cnf}, then for any $V_{\forall}$-assignment $I$ that we pick, $C$ is satisfiable on $I$. Let $\vpi$ be any $V_{\forall}$-allocation for $\mathcal{P}(F)$ that corresponds to $I$. By Lemma \ref{correctness3}, there is an allocation $\vpi'$ that Pareto-dominates $\vpi$. By Lemma \ref{correctness2}, $\vpi$ is not a $V_{\forall}$-allocation. Finally, because $\vpi$ is not a $V_{\forall}$-allocation, it follows from Lemma \ref{correctness1} that $\vpi'$ is not envy free. Because we had taken $\vpi$ to be an arbitrary $V_{\forall}$-allocation for an arbitrary $V_{\forall}$-assignment $I$, it follows that $\mathcal{P}(F)$ is a NO-instance of \textsc{$\exists$-eef-add}.

Therefore we conclude that \textsc{$\exists$-eef-add} is $\Sigma_2^p$-hard. \qed
\end{proof}

\section{Discussion}
We have introduced in this paper two new complexity results for the
resource allocation problem with additive preferences, thus filling an
important gap in the previous complexity studies of this problem,
mainly in \cite{BL-JAIR08}. Our main result shows that, even with very
simple preferences (additive), deciding whether there is a
Pareto-efficient and envy-free allocation is computationally very
hard. This goes slightly beyond the results in \cite{BL-JAIR08}, as it
shows that the high complexity of the problem is not only related to
the presence of preferential dependencies (complementarity or
substitutability) between objects, since the hardness holds under the
assumption of additive independence.

There are several natural ways of overcoming this high complexity. The
first one could be to impose some restrictions on the setting to
decrease the complexity. However, as stated in \cite{BL-JAIR08}, the
natural restrictions of the problem imply a huge loss of generality,
and thus are of limited practical interest. Another solution is to
relax envy-freeness or Pareto-efficiency, such as in \cite{LMMS04},
where envy-freeness is replaced by a measure of envy, and where
allocations are only required to be \emph{complete} (that is, all
objects must be allocated) instead of being Pareto-efficient. An idea
could be to mix collective utility maximization (\textit{e.g.}
classical utilitarian or egalitarian) with
envy-minimization.\footnote{A similar idea is proposed in \cite{BramsKing05}.} And lastly, designing efficient approximation
algorithms could be a way of getting around the high complexity of the
problem.

\bibliographystyle{splncs}
\bibliography{adt09}

\end{document}