%File: formatting-instruction.tex
\documentclass[letterpaper]{article}
\usepackage{aaai}
\usepackage{times}
\usepackage{helvet}
\usepackage{courier}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{graphics}
\usepackage{natbib}
\bibliographystyle{named}

\newtheorem{definition}{Definition}[section]
\newtheorem{lemma}[definition]{Lemma}

 \begin{document}
% The file aaai.sty is the style file for AAAI Press 
% proceedings, working notes, and technical reports.
%

\title{Planning Sudoku for SAT}
\author{<NAME>\\
              <EMAIL>\\
Center for Computational Logic (ICCL), Technische Universitet Dresden
}

\maketitle

\begin{abstract}
Sudoku is a very simple and well-known puzzle. Many encoding schemes such as Minimal, Efficient, Extended, and Pre-Processed are known for this puzzle. Any Sudoku puzzle is formulated as a CNF formula $\phi$ which is satisfiable if the Sudoku has a solution. We restrict our attention to consider only the instance of Sudoku which has only one solution and can only be solved using reasoning (i.e.with no search). Pre-Processed encoding suffices for this characterization, where other encoding schemes adds redundant clauses to minimal satisfying formulae; We observe that updating Pre-Processed encoding regarding pre-assigned cells configurations facilitate a higher degree of pre-processing and unit propagation can reduce the number of final clauses generated to be checked for a model.
\end{abstract}

\section{Introduction}
In recent years, there has been a considerable renewed interest in the satisfiability problem (SAT) and many efficient SAT solvers are available. Traditionally planning has been formalized as deduction~\citet{McCarthy1969}, but we'd formulated our model on satisfiability rather than on deduction. This approach not only provides a more flexible framework for stating different kinds of constraints on plans but also more accurately reflects the theory behind modern constraint-based planning systems~\citet{Henry2006}.

\section{Preliminaries}

\subsection{Sudoku}
Standard Sudoku puzzle usually appear in Newspapers is a $9\ast9$ grid instance of a very easy problem;


\begin{definition} A Sudoku puzzle is represented by a $\mathbb{N}\ast\mathbb{N}$ grid, which comprises of an $\sqrt{\mathbb{N}} \ast \sqrt{\mathbb{N}}$ sub-grids (also called boxes). 
Some of the entries in the grid are filled with numbers from $1$ to $\mathbb{N}$, whereas other entries are left blank~\citet{Lynce2006};\end{definition}

Puzzles are often assigned a difficulty level, which usually depends on the number of initial non-blank entries provided. This number may be as few as $17$ to test expert players for $9\ast9$ instance~\citet{Lynce2006}. But it could also be shown that with an automated planning system it can be reduced further to only one assignment and the planner still able to solve the problem correctly.

\begin{definition} A Sudoku puzzle is solved by assigning numbers from $1$ to $\mathbb{N}$ (size of puzzle) to the blank entries such that every row, every column, and every $\sqrt{\mathbb{N}} \ast \sqrt{\mathbb{N}}$ block (sub-grid) contains each of the any $\mathbb{N}$ possible numbers;\end{definition} 

Propositional logic formalism is used to encode Sudoku puzzle in our encoding and other well known encoding schemes~\citet{Weber2005}~\citet{Lynce2006}~\citet{Gihwon2006}.

\section{Planning as Satisfiability}
The complementary problem to deducibility is satisfiability that is finding a model for set of axioms. The formalism of planning as satisfiability turns out to have a number of  attractive properties like~\citet{Stefik1981}~\citet{chapman1987}: 
\begin{itemize}
\item It is easy to state arbitrary facts about any state of the world not just the initial and goal states;
\item It is likewise easy to state arbitrary constraints on the plan e.g. spcifying an action performed at a any specifal time interval;
\item Finally the approach provides a more accurate formal model of modern constraint based planners.
\end{itemize}

\subsection{Sudoku Axiomatization}
Many Sudoku solvers are already available~\citet{Pete2005}~\citet{DeadMan2005} and since there are more than $6.10^{21}$ possible grids for a simple looking $9\ast9$ puzzle instance~\citet{Bertram2005}; hence, a naive backtracking algorithm would be infeasible and the only feasible approach in this scenario is to combine backtracking with some form of constraint propagation. But we utilize a SAT-based approach in which a puzzle is translated into propositional formula $\Phi$ then we use any standard SAT solver to obtain the model (satisfying assignment) of $\Phi$; this model can then be readily translated into the solution of puzzle.

\subsubsection{Sudoku Encoding}
Since puzzles are regarded as a propositional SAT problem, we'll provide an overview of various existing encoding schemes. A SAT problem is represented as a propositional formula  $\Phi$ where each variable $P_i$ is assigned $0$ ($\mathbb{F}$) or $1$ ($\mathbb{T}$) where i $\in$ $(1,\cdot\cdot\cdot,n)$. % ($|n|$ is the length of formula).

	In an $\mathbb{N}\ast\mathbb{N}$ puzzle each cell can contains a number from $1$ to $n$. Each tuple $(r,c,v)$ denotes a variable which is true iff the cell in row $r$ and column $c$ is assigned a number $v$; $[r, c] = v$. The resulting set of formulas turn out to be $V$ = \{$(r,c,v)$ $|$ 1 $\leq$ $r,c,v$ $\leq$ n\}. Exactly one number for each cell, row, column and block can be viewed as a \textit{definedness} and \textit{Uniquness constraints}. Following is the formulae:
\begin{itemize}
\item There is at exactly one number in each cell\\
$\phi_{cell.ex}$ := $\phi_{cell.def}$ $\wedge$ $\phi_{cell.uniq}$\\
There is at least one number for each cell \\
 $\phi_{cell.def}$ := $\bigwedge_{r=1}^n$ $\bigwedge_{c=1}^n$ $\bigvee_{v=1}^n$ $(r,c,v)$\\
Each number appears at most one in each cell\\
$\phi_{cell.uniq}$ := $\bigwedge_{r=1}^n$ $\bigwedge_{c=1}^n$ $\bigwedge_{v_{i}=1}^{(n-1)}$ $\bigwedge_{v_{j}=v_{i} + 1}^n$$\neg(r,c,v_i)$ $\vee$ $\neg(r,c,v_j)$

\item There is at exactly one number in each row\\
$\phi_{row.ex}$ := $\phi_{row.def}$ $\wedge$ $\phi_{row.uniq}$\\
There is at least one number for each row \\
 $\phi_{row.def}$ := $\bigwedge_{r=1}^n$ $\bigwedge_{v=1}^n$ $\bigvee_{c=1}^n$ $(r,c,v)$\\
Each number appears at most one in each row\\
$\phi_{row.uniq}$ := $\bigwedge_{r=1}^n$ $\bigwedge_{v=1}^n$ $\bigwedge_{c_{i}=1}^{(n-1)}$ $\bigwedge_{c_{j}=c_{i} + 1}^n$$\neg(r,c_i,v)$ $\vee$ $\neg(r,c_j,v)$


\item There is at exactly one number in each column\\
$\phi_{col.ex}$ := $\phi_{col.def}$ $\wedge$ $\phi_{col.uniq}$\\
There is at least one number for each column \\
 $\phi_{col.def}$ = $\bigwedge_{c=1}^n$ $\bigwedge_{v=1}^n$ $\bigvee_{r=1}^n$ $(r,c,v)$\\
Each number appears at most one in each column\\
$\phi_{col.uniq}$ := $\bigwedge_{c=1}^n$ $\bigwedge_{v=1}^n$ $\bigwedge_{r_{i}=1}^{(n-1)}$ $\bigwedge_{r_{j}=r_{i} + 1}^n$$\neg(r_i,c,v)$ $\vee$ $\neg(r_j,c,v)$


\item There is at exactly one number in each block\\
$\phi_{blk.ex}$ = $\phi_{blk.def}$ $\wedge$ $\phi_{blk.uniq}$\\
There is at least one number for each block \\
 $\phi_{blk.def}$ = $\bigwedge_{rof=1}^{m}$ $\bigwedge_{cof=1}^{m}$ $\bigwedge_{v=1}^n$ $\bigvee_{r=1}^{m}$ $\bigvee_{c=1}^{m}$ $(rof \ast m + r,cof \ast m + c,v)$ where m := $\sqrt{n}$;\\
Each number appears at most one in each block\\
$\phi_{blk.uniq}$ = $\bigwedge_{rof=1}^{m}$ $\bigwedge_{cof=1}^{m}$ $\bigwedge_{v=1}^n$ $\bigwedge_{r=1}^{n}$ $\bigwedge_{c = r +1}^{n}$ \\
$\neg(rof \ast m + (r$ $mod$ $m),cof \ast m + (r$ mod $m),v)$ $\vee$ \\
$\neg(rof \ast m + (c$ mod $m),cof \ast m + (c$ mod $m),v)$ where m := $\sqrt{n}$;
\end{itemize}

\noindent The fixed cells are naturally represented as unit clauses in encoding of puzzle:

$V^{+}$ = $\{ (r,c,v) \in V | [r,c]$ is a fixed cell and has a pre-assigned  value $v$\}.

$\phi_{assign}$ = $\bigwedge_{i=1}^k$ $(r,c,v)$ where $(r,c,v)$ $\in$ $V^{+}$

\noindent Now encoding is nothing more than the following set of clauses:

\begin{itemize}
\item $\Phi_{extended}$ := $\phi_{cell.ex}$ $\wedge$ $\phi_{row.ex}$ $\wedge$ $\phi_{col.ex}$ $\wedge$ $\phi_{blk.ex}$ $\wedge$ $\phi_{assign}$. 

\item $\Phi_{efficient}$ := $\phi_{cell.ex}$ $\wedge$ $\phi_{row.uniq}$ $\wedge$ $\phi_{col.uniq}$ $\wedge$ $\phi_{blk.uniq}$ $\wedge$ $\phi_{assign}$. 

\item $\Phi_{minimal}$ := $\phi_{cell.def}$ $\wedge$ $\phi_{row.uniq}$ $\wedge$ $\phi_{col.uniq}$ $\wedge$ $\phi_{blk.uniq}$ $\wedge$ $\phi_{assign}$. 
 
\end{itemize}
%\begin{Minimal} \end{Minimal}
%\begin{Efficient} \end{Efficient}

$V^{\neg}$ = $\{ (r,c,v) \in V | \exists (r',c',v') \in V^{+} 
((r = r') \wedge (c = c') \wedge (v \neq v')) \vee 
((r = r') \wedge (c \neq c') \wedge (v = v')) \vee
((r \neq r') \wedge (c = c') \wedge (v = v')) \vee 
((r \neq r') \wedge (c = c') \wedge (v = v')) \wedge
\exists_{lRow, lCol}(lRow \leq r, r' \leq lRow + m) \wedge 
(lCol \leq c, c' \leq lCol + m)\}$\\
where:\\ \\
lRow = $\left\{\begin{array}{ll}
         	 $1$ & \mbox{$true$};\\
				 ((r-1)/m)\ast (m + 1)) & \mbox{$false$}. 
				 \end{array}\right.$
\\
lCol = $\left\{\begin{array}{ll}
         	 $1$ & \mbox{$true$};\\
				 ((c-1)/m)\ast (m + 1)) & \mbox{$false$}. 
				 \end{array}\right.$\\ \\
$m = \sqrt{n}$.\\

\noindent Reduction operators described in pre-assigned formulae is as follows:\\
$U := \{V^{+},V^{\neg}\}$
$\phi \Downarrow U = \{ C \in \phi | \neg\exists_{L \in C}.(L = x \wedge x \in U)\}$ \\

$\phi \downarrow V^{+} = \{ \forall C \in \phi. \forall {L \in C} | \neg(L = \neg x \Rightarrow x \in V^{+})\}$\\ 

$\phi \downarrow V^{\neg} = \{ \forall C \in \phi. \forall {L \in C} | \neg(L = x \Rightarrow x \in V^{\neg})\}$\\ 
\\
\noindent Giwhown~\citet{Gihwon2006} encoding is formulated as:
\begin{itemize}
\item $\Phi_{pre.process}$ := ($\phi_{cell.uniq}$ $\cup$ $\phi_{row.uniq}$ $\cup$ $\phi_{col.uniq}$ $\cup$ $\phi_{blk.uniq})\Downarrow V^{\neg}$ $\cup$ \\
($\phi_{cell.def}$ $\cup$ $\phi_{row.def}$ $\cup$ $\phi_{col.def}$ $\cup$ $\phi_{blk.def})\downarrow V^{\neg}$ $\cup$ 
 $\phi_{assign}\Downarrow V^{+}$. 
\end{itemize}

\begin{lemma}
\label{lemma:Satisfiablity}
A satisfiability equivalence relation holds between $\Phi_{extended}$ and $\Phi_{pre.process}$ with respect to a satisfying assignment $\alpha$ ,i.e.
$\alpha$ satisfies $\Phi_{extended}$ iff $\alpha$ satisfies $\Phi_{pre.process}$.
\end{lemma}

%\begin{proof}\textbf{(\ref{th:main})}
%\end{proof}
\section{Proposed Encoding}
\noindent The phenomenon we'd used to further reduce redundancies is explained using an example for $4\ast4$ puzzle instance. Suppose, we have some pre-assigned cells $[1,1]=4$ , $[1,2]=3$, $[1,3]=2$:
\begin{itemize}
\item Literals in  \textit{row definedness clause} are $(1,1,1)$, $(1,2,1)$, $(1,3,1)$, $(1,4,1)$;
\item Literals $(1,1,1)$ is falsified by pre-assigned $[1,1]=4$ because of same cell constraint; likewise $(1,2,1),(1,3,1)$ are falsified because of same row constraint.
\item $(1,4,1)$ is the only literal left where definedness constraint imposed it to be true thus assigning $[1,4]=4$.
\end{itemize}

The fact which we want to reveal from the above example is that by imposing all the above constraints consequence to obtaining new assigned values for the cells which are blank before and are not even in $\phi_{assign}$. So, rendering this process to include these newly assigned cells within our $\phi_{assign}$ set and perform the deletion and removal of clauses level and literals up to saturation result in further reductions and the following formulea confers it's detail as followed: 

$\varphi_{new}$ := ($\phi_{cell.def}$ $\cup$ $\phi_{row.def}$ $\cup$ $\phi_{col.def}$ $\cup$ $\phi_{blk.def})\downarrow V^{\neg}$\\
$V^{*}$ := $\{ \forall C \in \varphi_{new} . |C| = 1 \wedge C \not\in \phi_{assign} \Rightarrow C \cup V^{+} \}$\\
$\Phi_{new}$ := $\varphi_{new}\Downarrow V^{\neg}$ $\cup$
($\phi_{cell.uniq}$ $\cup$ $\phi_{row.uniq}$ $\cup$ $\phi_{col.uniq}$ $\cup$ $\phi_{blk.uniq})\Downarrow V^{\neg}$\\

\begin{lemma}
\label{lemma:Satisfiablity}
A satisfiability equivalence relation holds between $\Phi_{pre.process}$ and $\Phi_{new}$ with respect to a satisfying assignment $\alpha$, i.e.$\alpha$ satisfies $\Phi_{pre.process}$ iff $\alpha$ satisfies $\Phi_{new}$.
\end{lemma}

\section{Conclusion}
Our proposed encoding not only reduces a large amount of redundant clauses but also this process of redundant clause elimination coincides with the logic of finding newly assigned values for the blank cells. Thus not only eliminating a larger set of clauses for the solver but also filling in the blank cells in a correct fashion.

\bibliography{ref1}

\end{document}
