\documentclass{ctwart}

\parindent0pt

\usepackage{amsmath}
\usepackage{amssymb}

\addtolength{\textwidth}{1.3em}
\addtolength{\textheight}{1.3em}
\pagestyle{plain}
\newcommand{\n}{{\mathbb N}}

\begin{document}
\setcounter{page}{97}
\begin{frontmatter}
		 
\author{G. J\"ager}
\ead{gej@informatik.uni-kiel.de}
\address{Computer Science Institute, University of Kiel, D-24118 Kiel, 
Germany}


\title{An Effective SAT Encoding for Magic Labeling}


\begin{keyword}
Magic Labeling, Boolean Satisfiability, Backtracking.
\end{keyword}

\end{frontmatter}

\section{Introduction}
\label{sec_intro}

This work presents a Boolean satisfiability (SAT) encoding
for a special problem from combinatorial optimization.
In the last years much progress has been made in the optimization of
practical SAT solvers (see the SAT competition~\cite{satcomp}).
This has made SAT encodings for combinatorial problems highly attractive. 
In this work we propose an encoding for the combinatorial problem
{\em Magic Labeling} which has important applications in the field
of wireless networks~\cite{Wal01}. It is defined as follows.
Let an undirected, unweighted graph $ G = (V,E) $ 
be given with vertex set $V$ 
and edge set $E$, where $ |V| = n $ and $ |E| = m $. A {\em labeling} 
is a one-to-one mapping 
$ \lambda: V \cup E \rightarrow \{1,2,\dots,m+n\} $. 
Define the {\em weight $ \omega(e) $} of an edge $e \in E$ 
as the sum of the 
label of $e$ and of the labels of its two endpoints. 
An {\em edge-magic total labeling (EMTL)} is a labeling $ \lambda $ for which 
a constant $ h \in \n $ exists such that $ \omega(e) = h $ 
for each edge $ e \in E $.
Similarly, define the {\em weight $ \omega(v) $} of a vertex 
$v \in V$ as the sum of the label of $v$ and of the labels 
of all edges incident to $v$. 
A {\em vertex-magic total labeling (VMTL)} is a 
labeling $ \lambda $ for which 
a constant $ k \in \n $ exists such that $ \omega(v) = k $ 
for each vertex $ v \in V $.
Finally, a {\em totally magic labeling (TML)} is a labeling $ \lambda $ for
which (not necessarily equal) constants $ h,k \in \n $ exist 
such that $ \lambda $ is edge-magic with constant $h$ and 
vertex-magic with constant $k$.
$h$ and $k$ are called {\em magic constants}. 
A vertex $ v \in V $ and an edge $ e \in E $ 
are denoted {\em neighboring}, if $e$ is incident \mbox{to $v$}.
Note that different EMTLs exist for the same graph, 
and the same holds for VMTLs.
Surveys of results for magic graphs are given
in~\cite{Wal01}. 
We consider the following three problems for a given graph:
\\
{\bf (1)} Does an EMTL exist with given magic 
constant $h \in \n $?
\\
{\bf (2)} Does a VMTL exist with given 
magic constant $k \in \n $?
\\
{\bf (3)} Does a TML exist with given 
magic constants $h, k \in \n $?

The obvious method for these problems 
would be to use a backtracking approach.
In Section~\ref{sec_encode} we propose a general algorithm based
on a SAT encoding and extend the encoding and 
the resulted algorithm to the following problems: 
\\
{\bf (4)} Enumerate all EMTLs with given magic 
constant $h \in \n $?
\\
{\bf (5)} Enumerate all VMTLs with given magic constant $k \in \n $?
\\
{\bf (6)} Enumerate all TMLs with given 
magic constants $h, k \in \n $?
\\
In Section~\ref{sec_expres} we compare the performance
of this SAT based algorithm and of a backtracking
algorithm for the problems (1) and (2).

\section{SAT Encoding for Magic Labeling}
\label{sec_encode}

In this section we consider the problems 
(1) to (3).
Let $ G = (V,E) $ with $ |V| = n $, $ |E| = m $ and
$ r := n+m $. For our convenience, we define a fixed 
ordering on the set $ V \cup E $ by the numbers $ 1,2,\dots,n+m $, 
i.e., each number of $ \{1,2,\dots,n+m\} $ represents an edge
or a vertex of the graph. 
For the encoding we use $ r^2 $ Boolean variables $x_{i,j}$ with
$ 1 \le i,j \le r $, where we set
$ x_{i,j} \; = \; 
\left\{ 
\begin{array}{cl}
\mbox{{\sc True}}, & \mbox{\hspace*{0.2em} if edge/vertex 
$i$ receives label $j$}
\\
\mbox{{\sc False}}, & \mbox{\hspace*{0.2em} 
if edge/vertex $i$ does not receive label $j$}
\end{array}
\right.$
\\
{\bf Labeling Clauses:}
For receiving a feasible labeling we need the 
following conditions.
First each edge/vertex needs to have exactly one label. 
This leads to the condition
that for $i=1,2,\dots,r $ exactly one $ j \in \{1,2,\dots,r\} $ 
exists with $ x_{i,j} = $ {\sc True}.  
Second each label has to be used by exactly one edge/vertex. 
This leads to the condition
that for $j=1,2,\dots,r $ exactly one $ i \in \{1,2,\dots,r\} $ 
exists with $ x_{i,j} = $ {\sc True}.  
All $2r$ restrictions  have the same structure, 
namely that exactly one of the $r$ 
involved Boolean variables is 
set to {\sc True} and the rest to {\sc False}. 
To represent this, we introduce $2r^2$ auxiliary variables 
$ y_1, y_2, \dots, y_{2r^2} $, with $r$ $y$'s for one restriction. 
W.l.o.g., consider the first restriction, which contains the 
Boolean variables 
$ x_{1,1},x_{1,2},\dots,x_{1,r} $, and the corresponding auxiliary 
variables $y_1, y_2, \dots, y_{r} $.
For $ 1 \le k \le r $ we use $y_k$ to represent that at least  
one of $x_{1,1}, x_{1,2}, \dots, x_{1,k}$ is {\sc True}. 
Precisely, the $y$ variables are defined as 
$ y_1 = x_{1,1} $ or equivalently $ (\neg
x_{1,1} \vee y_1) \wedge (x_{1,1} \vee \neg y_1) $,
and $ y_k = x_{1,k} \vee y_{k-1} $ or equivalently
$ (y_k \vee \neg x_{1,k}) \wedge (y_k \vee \neg y_{k-1}) 
\wedge (\neg y_k \vee x_{1,k} \vee y_{k-1}) $
for $k = 2,3,\dots,r$.
In addition, we need to enforce that only one $x_{1,i}$ with 
$ 1 \le i \le r$ can be {\sc True}. This means, if $x_{1, k}$ is 
{\sc True}, none of the $x_{1i}$ for $1 \le i < k \le r$ 
can be {\sc True}. This is formulated as
$ \neg y_{k-1} \vee \neg x_{1k} $ for $k = 2,\dots,r $.
Finally $ y_r $ must be {\sc True}.
\\
{\bf Magic Clauses:}
Furthermore we have to add clauses which ensure that the 
conditions of EMTL/ \linebreak[3] VMTL/TML are fulfilled. 
The following two conditions occur:
\\
EMTL/TML: Set $ l:=2 $. For given $ h \in \n $ 
and a given edge the sum of $l+1 $ labels (namely the label of the edge
and of its $ l $ endpoint vertices) equals $h$.
\\
VMTL/TML: For given $ k \in \n $ 
and a given vertex with degree $ l \in \n $  
the sum of $l+1$ labels (namely the label of the vertex
and of its $l$ incident edges) \mbox{equals $k$}.
\\
Observe that both conditions have the following structure:
For given constants $ c,l \in \n $ the sum of $l+1$ labels equals $c$.
For $ l \in \n $ let $W$ be the set containing all 
possible \mbox{$l$-tuples} $ \overrightarrow{w} = (w_1,w_2,\dots,w_l) $ with
$ w_i \in \{1,2,\dots,r\} $ for $ 1 \le i \le l $ and $ w_i \not= w_j $ 
for $ 1 \le i < j \le l $.
Now let a constant $ c \in \n $ be given and an edge 
or vertex $f$ with corresponding $l \in \n $, 
i.e., if $f$ is an edge, then
$l=2$, and otherwise $ l $ is the degree of $f$.
We want to fulfill the magic condition for $f$.
This means that the sum of the label of $f$ and of its neighboring 
elements is $c$. Let $ f_1,f_2,\dots,f_l $ 
be the neighboring elements of $f$.
For this $l$ compute the set $W$ (which is easy for small $l$) 
and choose an arbitrary element
$ \overrightarrow{w} \in W $ with $ w:= \sum_{i=1}^l w_i $. 
Then label $ f_1,f_2,\dots,f_l $ by $ w_1,w_2,\dots,w_l $, 
and consider the four cases:
\\
{\bf Case $1$:} $ i \in \{1,2,\dots,l\} $ exists with
$ c-w = w_i $;  
{\bf Case $2$:} $ w \ge c $;
{\bf Case $3$:} $ w < c-r $;
{\bf Case $4$:} Otherwise.
\\
As all labels are different and are contained 
in the set $ \{1,2,\dots,r\} $, it is 
clear that for the Cases $1$, $2$, or $3$ no labeling of 
$ f $ exists such 
that the sum of the labels of $f,f_1,f_2,\dots,f_l $ is $c$.
In these cases we add the clause 
$ \neg x_{f_1,w_1} \vee \neg x_{f_2,w_2} \vee \dots \vee 
\neg x_{f_l,w_l} $
meaning that labeling $ f_1,f_2,\dots,f_l $ by 
$ w_1,w_2,\dots,w_l $ is not possible.
For Case 4 such a labeling is possible, but only if $f$
is labeled with $c-w$. This leads to the clause
$ \neg x_{f_1,w_1} \vee \neg x_{f_2,w_2} \vee \dots \vee 
\neg x_{f_l,w_l} \vee x_{f,c-w} $.
Thus for each $ \overrightarrow{w} \in W $ we have an additional clause. 
Clearly, the number of possible sums and therefore the 
number of magic clauses becomes rather large, 
if we consider VMTLs or TML for dense graphs.
In these cases the resulted algorithm has 
bad performance (see Section \ref{sec_expres}). 
\\
{\bf Enumerating All Magic Labelings:}
The SAT based representation allows us to enumerate
all magic labelings using a technique of Jin, Han, 
Somenzi~\cite{JHS05}, which is applicable to general SAT instances. 
The main idea of this technique is to add new clauses to a SAT 
model with purpose to enumerate all SAT solutions. 
In our case we start with the presented SAT encoding.
If this SAT encoding is satisfiable, we receive a first magic labeling
$ \lambda: \{1,2,\dots,r\} \rightarrow  \{1,2,\dots,r\} $.
This means that in the SAT solution exactly
the Boolean variables $ x_{1,\lambda(1)}, x_{2,\lambda(2)}, \dots, $
$ x_{r,\lambda(r)} $ are set to {\sc True}.
Then we explicitly forbid this magic 
labeling by adding the new clause 
$ \neg x_{1,\lambda(1)} \vee \neg x_{2,\lambda(2)} \vee \dots \vee
\neg x_{r,\lambda(r)} $
to the current SAT instance. 
For the updated SAT instance there are two possibilities. If the instance
is satisfiable, this leads to another magic labeling, as the first one
is not allowed. If not, the first magic labeling  was the only one.
This process can be iterated, until 
all or a determined number of magic labelings has been found. 

\section{Experimental Results}
\label{sec_expres}

In this section we compare our algorithm (called {\sc Sat-Magic}) 
with a natural backtracking algorithm (called {\sc Back-Magic}).
In {\sc Back-Magic} all vertices and edges are labeled in a fixed order, 
and if a partial labeling makes a magic labeling impossible, 
then a backtracking step occurs, i.e., a previous labeling 
of a edge/vertex is changed, and the search continues at 
this step. 
All algorithms have been implemented in C++,
where we make use of an effective SAT solver 
implemented by E\'{e}n and S\"orensson, 
called {\sc MiniSat}~\cite{ES03}.
The experiments were carried out on a PC with
an Athlon 1900MP CPU with 2GB of memory.
We test random graphs with size $ n= 10, 15 $, where 
$ p = 10 \%, 20 \%, 30 \%, 40 \% $ edges are 
chosen randomly and uniformly distributed 
from all possible $ n\cdot(n-1)/2 $ ones. 
As only $3$ connected TMLs are known~\cite{BS08}, we do not consider TMLs,
but only EMTLs and VMTLs.
Note that for each single instance we can easily compute 
a lower bound $ lb \in \n $ and an upper bound 
$ ub \in \n $ for possible magic constants. Then we choose 
$ \min \{ 10, ub-lb+1\} $ values of this interval $ [lb,ub] $ and 
for each value we receive a single instance of the 
form (1) or (2).
Thus we have $ 16 = 2 \cdot 2 \cdot 4 $ test classes, where each test class
consists of up to $10$ single instances.
\\
In Table \ref{tab1} for both algorithms and for each 
test class a percentage value is given describing
how many instances of this test class can be solved in 
$600$ seconds. 
The results clearly demonstrate the
superiority of {\sc Sat-Magic} in comparison to {\sc Back-Magic}.
As expected, {\sc Sat-Magic} behaves rather bad for VMTLs with large density. 

\setlength{\tabcolsep}{0.15em}
\begin{center}
\begin{footnotesize}
\begin{table}
\label{tab1}
\begin{tabular}{c||c|c|c|c|c|c|c|c|c|c|c|c|c|c|c|c}
Size $n$ & \multicolumn{8}{|c}{10} & \multicolumn{8}{|c}{15} 
\\ \hline
Type & \multicolumn{4}{|c}{EMTL} & \multicolumn{4}{|c}{VMTL} & 
\multicolumn{4}{|c}{EMTL} & \multicolumn{4}{|c}{VMTL}  
\\ \hline
Density $p$ (\%) & 10 & 20 & 30 & 40 & 10 & 20 & 30 & 40 & 10 & 20 & 
30 & 40 & 10 & 20 & 30 & 40
\\ \hline\hline
Suc. {\sc Back} (\%) & \phantom{0}40 & \phantom{0}20 & \phantom{0}10 & 
\phantom{00}0 & 100 & \phantom{00}0 & \phantom{00}0
& \phantom{00}0 & \phantom{00}0 & \phantom{00}0 & \phantom{00}0 & 
\phantom{00}0 & \phantom{00}0 & \phantom{00}0 & \phantom{00}0 & \phantom{00}0
\\ \hline
Suc. {\sc Sat} (\%) & 100 & 100 & 100 & \phantom{0}80 & 100 & 100 & \phantom{00}0
& \phantom{00}0 & \phantom{0}80 & \phantom{0}60 & \phantom{0}50 & \phantom{00}0 & 100 & \phantom{00}0 & \phantom{00}0 & \phantom{00}0 
\end{tabular}
\vspace*{0.5em}
\caption{Comparison of {\sc Sat Magic} and {\sc Back Magic}}
\end{table}
\end{footnotesize}
\end{center}


\begin{thebibliography}{99}

\bibitem{BS08}
A.~Baker, J.~Sawada:
{\em Magic Labelings on Cycles and Wheels.}
In B.~Yang, D.-Z.~Du, C.A.~Wang (Eds.):
Proc.~2nd Annual International Conference on
Combinatorial Optimization and Applications (\mbox{COCOA}).
Lecture Notes in Comput.~Sci.~\textbf{5165}, 361-373, 200

\bibitem{ES03}
N.~E\'{e}n, N.~S\"orensson:
{\em An Extensible SAT-Solver.}
In E.~Giunchiglia, A. Tacchella (Eds.):
Proc. 6th International Conference on Theory
and Applications of Satisfiability Testing (SAT).
Lecture Notes in Comput. Sci.~\textbf{2919}, 502-518, 2003.

\bibitem{JHS05}
H.~Jin, H.~Han, F.~Somenzi:
{\em Efficient Conflict Analysis for Finding All Satisfying 
Assignments of a Boolean Circuit.}
In N.~Halbwachs, L.D.~Zuck (Eds.):
Proc. 11th International Conference on
Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
Lecture Notes in Comput.~Sci.~\textbf{3440}, 287-300, 2005.

\bibitem{Wal01}
W.D.~Wallis:
{\em Magic Graphs.}
Birkh\"auser, Boston, 2001.


\bibitem{satcomp}
International SAT Competition: ``http://www.satcompetition.org/''.

\end{thebibliography}

\end{document}

ab paper 12 weiter
