\documentclass[11pt,twoside]{article}\makeatletter

\IfFileExists{xcolor.sty}%
  {\RequirePackage{xcolor}}%
  {\RequirePackage{color}}
\usepackage{colortbl}
\usepackage{wrapfig}
\usepackage{ifxetex}
\ifxetex
  \usepackage{fontspec}
  \usepackage{xunicode}
  \catcode`⃥=\active \def⃥{\textbackslash}
  \catcode`❴=\active \def❴{\{}
  \catcode`❵=\active \def❵{\}}
  \def\textJapanese{\fontspec{Noto Sans CJK JP}}
  \def\textChinese{\fontspec{Noto Sans CJK SC}}
  \def\textKorean{\fontspec{Noto Sans CJK KR}}
  \setmonofont{DejaVu Sans Mono}
  
\else
  \IfFileExists{utf8x.def}%
   {\usepackage[utf8x]{inputenc}
      \PrerenderUnicode{–}
    }%
   {\usepackage[utf8]{inputenc}}
  \usepackage[english]{babel}
  \usepackage[T1]{fontenc}
  \usepackage{float}
  \usepackage[]{ucs}
  \uc@dclc{8421}{default}{\textbackslash }
  \uc@dclc{10100}{default}{\{}
  \uc@dclc{10101}{default}{\}}
  \uc@dclc{8491}{default}{\AA{}}
  \uc@dclc{8239}{default}{\,}
  \uc@dclc{20154}{default}{ }
  \uc@dclc{10148}{default}{>}
  \def\textschwa{\rotatebox{-90}{e}}
  \def\textJapanese{}
  \def\textChinese{}
  \IfFileExists{tipa.sty}{\usepackage{tipa}}{}
\fi
\def\exampleFont{\ttfamily\small}
\DeclareTextSymbol{\textpi}{OML}{25}
\usepackage{relsize}
\RequirePackage{array}
\def\@testpach{\@chclass
 \ifnum \@lastchclass=6 \@ne \@chnum \@ne \else
  \ifnum \@lastchclass=7 5 \else
   \ifnum \@lastchclass=8 \tw@ \else
    \ifnum \@lastchclass=9 \thr@@
   \else \z@
   \ifnum \@lastchclass = 10 \else
   \edef\@nextchar{\expandafter\string\@nextchar}%
   \@chnum
   \if \@nextchar c\z@ \else
    \if \@nextchar l\@ne \else
     \if \@nextchar r\tw@ \else
   \z@ \@chclass
   \if\@nextchar |\@ne \else
    \if \@nextchar !6 \else
     \if \@nextchar @7 \else
      \if \@nextchar (8 \else
       \if \@nextchar )9 \else
  10
  \@chnum
  \if \@nextchar m\thr@@\else
   \if \@nextchar p4 \else
    \if \@nextchar b5 \else
   \z@ \@chclass \z@ \@preamerr \z@ \fi \fi \fi \fi
   \fi \fi  \fi  \fi  \fi  \fi  \fi \fi \fi \fi \fi \fi}
\gdef\arraybackslash{\let\\=\@arraycr}
\def\@textsubscript#1{{\m@th\ensuremath{_{\mbox{\fontsize\sf@size\z@#1}}}}}
\def\Panel#1#2#3#4{\multicolumn{#3}{){\columncolor{#2}}#4}{#1}}
\def\abbr{}
\def\corr{}
\def\expan{}
\def\gap{}
\def\orig{}
\def\reg{}
\def\ref{}
\def\sic{}
\def\persName{}\def\name{}
\def\placeName{}
\def\orgName{}
\def\textcal#1{{\fontspec{Lucida Calligraphy}#1}}
\def\textgothic#1{{\fontspec{Lucida Blackletter}#1}}
\def\textlarge#1{{\large #1}}
\def\textoverbar#1{\ensuremath{\overline{#1}}}
\def\textquoted#1{‘#1’}
\def\textsmall#1{{\small #1}}
\def\textsubscript#1{\@textsubscript{\selectfont#1}}
\def\textxi{\ensuremath{\xi}}
\def\titlem{\itshape}
\newenvironment{biblfree}{}{\ifvmode\par\fi }
\newenvironment{bibl}{}{}
\newenvironment{byline}{\vskip6pt\itshape\fontsize{16pt}{18pt}\selectfont}{\par }
\newenvironment{citbibl}{}{\ifvmode\par\fi }
\newenvironment{docAuthor}{\ifvmode\vskip4pt\fontsize{16pt}{18pt}\selectfont\fi\itshape}{\ifvmode\par\fi }
\newenvironment{docDate}{}{\ifvmode\par\fi }
\newenvironment{docImprint}{\vskip 6pt}{\ifvmode\par\fi }
\newenvironment{docTitle}{\vskip6pt\bfseries\fontsize{22pt}{25pt}\selectfont}{\par }
\newenvironment{msHead}{\vskip 6pt}{\par}
\newenvironment{msItem}{\vskip 6pt}{\par}
\newenvironment{rubric}{}{}
\newenvironment{titlePart}{}{\par }

\newcolumntype{L}[1]{){\raggedright\arraybackslash}p{#1}}
\newcolumntype{C}[1]{){\centering\arraybackslash}p{#1}}
\newcolumntype{R}[1]{){\raggedleft\arraybackslash}p{#1}}
\newcolumntype{P}[1]{){\arraybackslash}p{#1}}
\newcolumntype{B}[1]{){\arraybackslash}b{#1}}
\newcolumntype{M}[1]{){\arraybackslash}m{#1}}
\definecolor{label}{gray}{0.75}
\def\unusedattribute#1{\sout{\textcolor{label}{#1}}}
\DeclareRobustCommand*{\xref}{\hyper@normalise\xref@}
\def\xref@#1#2{\hyper@linkurl{#2}{#1}}
\begingroup
\catcode`\_=\active
\gdef_#1{\ensuremath{\sb{\mathrm{#1}}}}
\endgroup
\mathcode`\_=\string"8000
\catcode`\_=12\relax

\usepackage[a4paper,twoside,lmargin=1in,rmargin=1in,tmargin=1in,bmargin=1in,marginparwidth=0.75in]{geometry}
\usepackage{framed}

\definecolor{shadecolor}{gray}{0.95}
\usepackage{longtable}
\usepackage[normalem]{ulem}
\usepackage{fancyvrb}
\usepackage{fancyhdr}
\usepackage{graphicx}
\usepackage{marginnote}

\renewcommand{\@cite}[1]{#1}


\renewcommand*{\marginfont}{\itshape\footnotesize}

\def\Gin@extensions{.pdf,.png,.jpg,.mps,.tif}

  \pagestyle{fancy}

\usepackage[pdftitle={A Proposed SAT Algorithm},
 pdfauthor={}]{hyperref}
\hyperbaseurl{}

	 \paperwidth210mm
	 \paperheight297mm
              
\def\@pnumwidth{1.55em}
\def\@tocrmarg {2.55em}
\def\@dotsep{4.5}
\setcounter{tocdepth}{3}
\clubpenalty=8000
\emergencystretch 3em
\hbadness=4000
\hyphenpenalty=400
\pretolerance=750
\tolerance=2000
\vbadness=4000
\widowpenalty=10000

\renewcommand\section{\@startsection {section}{1}{\z@}%
     {-1.75ex \@plus -0.5ex \@minus -.2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\Large\bfseries}}
\renewcommand\subsection{\@startsection{subsection}{2}{\z@}%
     {-1.75ex\@plus -0.5ex \@minus- .2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\Large}}
\renewcommand\subsubsection{\@startsection{subsubsection}{3}{\z@}%
     {-1.5ex\@plus -0.35ex \@minus -.2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\large}}
\renewcommand\paragraph{\@startsection{paragraph}{4}{\z@}%
     {-1ex \@plus-0.35ex \@minus -0.2ex}%
     {0.5ex \@plus .2ex}%
     {\reset@font\normalsize}}
\renewcommand\subparagraph{\@startsection{subparagraph}{5}{\parindent}%
     {1.5ex \@plus1ex \@minus .2ex}%
     {-1em}%
     {\reset@font\normalsize\bfseries}}


\def\l@section#1#2{\addpenalty{\@secpenalty} \addvspace{1.0em plus 1pt}
 \@tempdima 1.5em \begingroup
 \parindent \z@ \rightskip \@pnumwidth 
 \parfillskip -\@pnumwidth 
 \bfseries \leavevmode #1\hfil \hbox to\@pnumwidth{\hss #2}\par
 \endgroup}
\def\l@subsection{\@dottedtocline{2}{1.5em}{2.3em}}
\def\l@subsubsection{\@dottedtocline{3}{3.8em}{3.2em}}
\def\l@paragraph{\@dottedtocline{4}{7.0em}{4.1em}}
\def\l@subparagraph{\@dottedtocline{5}{10em}{5em}}
\@ifundefined{c@section}{\newcounter{section}}{}
\@ifundefined{c@chapter}{\newcounter{chapter}}{}
\newif\if@mainmatter 
\@mainmattertrue
\def\chaptername{Chapter}
\def\frontmatter{%
  \pagenumbering{roman}
  \def\thechapter{\@roman\c@chapter}
  \def\theHchapter{\roman{chapter}}
  \def\thesection{\@roman\c@section}
  \def\theHsection{\roman{section}}
  \def\@chapapp{}%
}
\def\mainmatter{%
  \cleardoublepage
  \def\thechapter{\@arabic\c@chapter}
  \setcounter{chapter}{0}
  \setcounter{section}{0}
  \pagenumbering{arabic}
  \setcounter{secnumdepth}{6}
  \def\@chapapp{\chaptername}%
  \def\theHchapter{\arabic{chapter}}
  \def\thesection{\@arabic\c@section}
  \def\theHsection{\arabic{section}}
}
\def\backmatter{%
  \cleardoublepage
  \setcounter{chapter}{0}
  \setcounter{section}{0}
  \setcounter{secnumdepth}{2}
  \def\@chapapp{\appendixname}%
  \def\thechapter{\@Alph\c@chapter}
  \def\theHchapter{\Alph{chapter}}
  \appendix
}
\newenvironment{bibitemlist}[1]{%
   \list{\@biblabel{\@arabic\c@enumiv}}%
       {\settowidth\labelwidth{\@biblabel{#1}}%
        \leftmargin\labelwidth
        \advance\leftmargin\labelsep
        \@openbib@code
        \usecounter{enumiv}%
        \let\p@enumiv\@empty
        \renewcommand\theenumiv{\@arabic\c@enumiv}%
	}%
  \sloppy
  \clubpenalty4000
  \@clubpenalty \clubpenalty
  \widowpenalty4000%
  \sfcode`\.\@m}%
  {\def\@noitemerr
    {\@latex@warning{Empty `bibitemlist' environment}}%
    \endlist}

\def\tableofcontents{\section*{\contentsname}\@starttoc{toc}}
\parskip0pt
\parindent1em
\def\Panel#1#2#3#4{\multicolumn{#3}{){\columncolor{#2}}#4}{#1}}
\newenvironment{reflist}{%
  \begin{raggedright}\begin{list}{}
  {%
   \setlength{\topsep}{0pt}%
   \setlength{\rightmargin}{0.25in}%
   \setlength{\itemsep}{0pt}%
   \setlength{\itemindent}{0pt}%
   \setlength{\parskip}{0pt}%
   \setlength{\parsep}{2pt}%
   \def\makelabel##1{\itshape ##1}}%
  }
  {\end{list}\end{raggedright}}
\newenvironment{sansreflist}{%
  \begin{raggedright}\begin{list}{}
  {%
   \setlength{\topsep}{0pt}%
   \setlength{\rightmargin}{0.25in}%
   \setlength{\itemindent}{0pt}%
   \setlength{\parskip}{0pt}%
   \setlength{\itemsep}{0pt}%
   \setlength{\parsep}{2pt}%
   \def\makelabel##1{\upshape ##1}}%
  }
  {\end{list}\end{raggedright}}
\newenvironment{specHead}[2]%
 {\vspace{20pt}\hrule\vspace{10pt}%
  \phantomsection\label{#1}\markright{#2}%

  \pdfbookmark[2]{#2}{#1}%
  \hspace{-0.75in}{\bfseries\fontsize{16pt}{18pt}\selectfont#2}%
  }{}
      \def\TheFullDate{2013-05-15 (revised: 15 May 2013)}
\def\TheID{\makeatother }
\def\TheDate{2013-05-15}
\title{A Proposed SAT Algorithm}
\author{}\makeatletter 
\makeatletter
\newcommand*{\cleartoleftpage}{%
  \clearpage
    \if@twoside
    \ifodd\c@page
      \hbox{}\newpage
      \if@twocolumn
        \hbox{}\newpage
      \fi
    \fi
  \fi
}
\makeatother
\makeatletter
\thispagestyle{empty}
\markright{\@title}\markboth{\@title}{\@author}
\renewcommand\small{\@setfontsize\small{9pt}{11pt}\abovedisplayskip 8.5\p@ plus3\p@ minus4\p@
\belowdisplayskip \abovedisplayskip
\abovedisplayshortskip \z@ plus2\p@
\belowdisplayshortskip 4\p@ plus2\p@ minus2\p@
\def\@listi{\leftmargin\leftmargini
               \topsep 2\p@ plus1\p@ minus1\p@
               \parsep 2\p@ plus\p@ minus\p@
               \itemsep 1pt}
}
\makeatother
\fvset{frame=single,numberblanklines=false,xleftmargin=5mm,xrightmargin=5mm}
\fancyhf{} 
\setlength{\headheight}{14pt}
\fancyhead[LE]{\bfseries\leftmark} 
\fancyhead[RO]{\bfseries\rightmark} 
\fancyfoot[RO]{}
\fancyfoot[CO]{\thepage}
\fancyfoot[LO]{\TheID}
\fancyfoot[LE]{}
\fancyfoot[CE]{\thepage}
\fancyfoot[RE]{\TheID}
\hypersetup{citebordercolor=0.75 0.75 0.75,linkbordercolor=0.75 0.75 0.75,urlbordercolor=0.75 0.75 0.75,bookmarksnumbered=true}
\fancypagestyle{plain}{\fancyhead{}\renewcommand{\headrulewidth}{0pt}}

\date{}
\usepackage{authblk}

\providecommand{\keywords}[1]
{
\footnotesize
  \textbf{\textit{Index terms---}} #1
}

\usepackage{graphicx,xcolor}
\definecolor{GJBlue}{HTML}{273B81}
\definecolor{GJLightBlue}{HTML}{0A9DD9}
\definecolor{GJMediumGrey}{HTML}{6D6E70}
\definecolor{GJLightGrey}{HTML}{929497} 

\renewenvironment{abstract}{%
   \setlength{\parindent}{0pt}\raggedright
   \textcolor{GJMediumGrey}{\rule{\textwidth}{2pt}}
   \vskip16pt
   \textcolor{GJBlue}{\large\bfseries\abstractname\space}
}{%   
   \vskip8pt
   \textcolor{GJMediumGrey}{\rule{\textwidth}{2pt}}
   \vskip16pt
}

\usepackage[absolute,overlay]{textpos}

\makeatother 
      \usepackage{lineno}
      \linenumbers
      
\begin{document}

             \author[1]{Dr. Bagais  A.}

             \author[2]{Abdullahi  M.}

             \affil[1]{  Ahmadu Bello University, Zaria-Nigeria}

\renewcommand\Authands{ and }

\date{\small \em Received: 11 April 2013 Accepted: 1 May 2013 Published: 15 May 2013}

\maketitle


\begin{abstract}
        


This paper reviews existing SAT algorithms and proposes a new algorithm that solves the SAT problem.  The proposed algorithm differs from existing algorithms in several aspects. First, the proposed algorithm does not do any backtracking during the searching process that usually consumes significant time as it is the case with other algorithms.  Secondly, the searching process in the proposed algorithm is simple, easy to implement, and each step is determined instantly unlike other algorithms where decisions are made based on some heuristics or random decisions. For clauses with three literals, the upper bound for the proposed algorithm is O(1.8171n). While some researchers reported better upper bounds than this, those upper bounds depend on the nature of the clauses while our upper bound is independent of the nature of the propositional formula.

\end{abstract}


\keywords{propositional satisfiability, NP-complete, complexity, complete algorithms.}

\begin{textblock*}{18cm}(1cm,1cm) % {block width} (coords) 
\textcolor{GJBlue}{\LARGE Global Journals \LaTeX\ JournalKaleidoscope\texttrademark}
\end{textblock*}

\begin{textblock*}{18cm}(1.4cm,1.5cm) % {block width} (coords) 
\textcolor{GJBlue}{\footnotesize \\ Artificial Intelligence formulated this projection for compatibility purposes from the original article published at Global Journals. However, this technology is currently in beta. \emph{Therefore, kindly ignore odd layouts, missed formulae, text, tables, or figures.}}
\end{textblock*}


\let\tabcellsep& 	 	 		 
\section[{Introduction}]{Introduction}\par
ropositional satisfiability (SAT) is one of the classical problems in Computer Science. The importance of SAT comes from the fact that a large class of real-world problems can be expressed in terms of a SAT instance and that it was the first problem proven to be NP-Complete \hyperref[b2]{(Cook, 1971)}. The SAT problem has a wide range of practical real world applications \hyperref[b0]{(Barbour, 1992;}\hyperref[b3]{Crawford \& Baker, 1994;}\hyperref[b8]{Devadas, 1989;}\hyperref[b14]{Kauts \& Selman, 1992;}\hyperref[b16]{Larrabee, 1992)}. Many algorithms, categorized into complete and incomplete algorithms, were proposed to solve this problem efficiently over the last decades.\par
Complete algorithms can state whether a SAT instance is satisfiable giving the satisfying assignments or unsatisfiable giving a 'no' answer. Incomplete algorithms can only give an answer of 'yes' for satisfiable SAT instances only but cannot give an answer for unsatisfiable instances.\par
This paper proposes a new complete algorithm that differs from the ones in the literature in the following aspects:\par
? No backtracking during the searching process that usually consumes significant amount of time. ? Has a simple, deterministic and easy to implement search process, unlike other algorithms where decisions are either made randomly or based on some heuristics. The remainder of the paper is structured as follows. Section 2 describes the proposed algorithm with the aid of an example. Section 3 captures the algorithm in pseudo code while Section 4 presents the complexity analysis of the algorithm. We present related work in Section 5. Sections 6 and 7 summarize and provide references, respectively. 
\section[{II.}]{II.} 
\section[{Illustrating the Proposed Algorithm}]{Illustrating the Proposed Algorithm}\par
Unlike other algorithms that make a decision on a single value (true/false) for a variable x , the proposed algorithms takes into consideration all satisfying assignments for a clause C and use them for the next clauses so that backtracking is avoided.\par
Consider the following formula:4 1 5 3 1 3 2 2 4 ( ) ( ) ( ) F x x x x x x x x x = ? ? ? ? ? ? ? ?\par
The first clause can be satisfied by any of the following assignments 1 The algorithm tries to find assignments for all variables in clause while preserving at least one of the given assignments for 1 3 , x x , or 4\par
x in the first clause.\par
In general, the process starts from the first clause 1\par
If the clause has k literals, then k assignments can satisfy it (as in the previous formula, the first clause has three assignments). In the next step, the set of assignments that satisfy the set of previous clause(s) are checked with all the literals of the next clause. The process continues until all the clauses in the formula are covered, after which the resulting set of assignments each satisfies the formula.\par
When a set of assignments from previous clause(s) is checked with the literals of the current clause, each literal may agree, disagree or be neutral to the assignment. A literal agrees with an assignment when the assignment includes the literal. A literal disagrees with an assignment when the assignment includes a negation of the literal. A literal is neutral to an  
\section[{D}]{D}\par
assignment when the assignment neither agrees nor disagrees with the literal.4 1 5 3 1 3 2 2 4 ( ) ( ) ( ) F x x x x x x x x x = ? ? ? ? ? ? ? ? Figure 1 : Assignment Production\par
In the first step, the satisfying assignments for the first clause are its literals. The assignments produced for the first clause are shown in the top-left rectangle in Figure  {\ref 1}. Each of these assignments is checked with the literals of the second clause,1 5 2 ( ) x x x ? ?\par
. The assignment of 1\par
x disagrees with the first literal of the second clause, 1\par
x resulting in no assignment produced. The same assignment, 1\par
x is checked with the second literal, 2\par
x . Since this literal is neutral to 1\par
x , a new assignment is produced by combining 1\par
x and 2 x , as shown in the middle rectangle in Figure  {\ref 1}. Next, 1\par
x is checked with 5 x , giving 5 1\par
x x , since 5\par
x is neutral to 1 x . Similarly, the assignments Note that each of these 18 assignments satisfies the given formula. Note that when an assignment agrees with the clause in consideration, the process might produce shorthand for 1 2 x x ? etc. We will illustrate this with the pair of clauses:1 2 3 1 4 5 ( ) ( ) x x x x x x ? ? ? ?\par
The satisfying assignments for this pair of clauses are:1 1 1 2 1 3 1 1 4 2 4 3 4 1 5 2 5 3 5 ( ) x x or x x x x x x x x x x x x x x x x x\par
From this group, it can be seen that the assignments \} \{ 1 4 1 5 2 1 3 1 , , , x x x x x x x x are subsumed in the first assignment 1\par
x . This is because each of these assignments produces the same result as 1\par
x .\par
Thus, these assignments can be dropped to avoid redundancy. Therefore, Figure  {\ref 1} can now be redrawn without the subsumed assignments as shown in Figure 2. x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x x Since the subsumed assignments are produced from clauses that have a literal in common, the proposed algorithm starts by extracting all clauses that do not share a literal. For a satisfiability formula with n literals each clause containing exactly k literals, the minimum number of clauses in which no two clauses have a common literal is 2n k4 1 3 ( ) x x x ? ? 1 5 2 ( ) x x x ? ? 3 2 4 ( ) x x x ? ?. 4 1 3 2 6 5 6 5 1 2 3 4 1 6 5 4\textbf{2 3 ( ) ( ) ( ) ( ) ( )}( ) F x x x x x x x x x x x x x x x x x x = ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ? ?\par
For example, we need at least 4 clauses to have the 12 literals in the following formula. But because of the distribution of literals, we need 5 for that purpose. Therefore, the algorithm will extract the clauses that do not have common literals. There are two advantages in doing so: 1. The algorithm will save the time to check the existence of subsumed assignments which is a process that consumes an amount of time equal to the number of assignments. 2. The time complexity of the algorithm becomes easier to prove (see Section 4). m i m i k k i k k i m ? ? ? ? = ? ? ? ? ? redundant assignments.\par
Proof: (By induction). 
\section[{Base Case}]{Base Case}\par
The base case is when i m = and the total number of redundant assignments will be0 ( 1) ( 1)\textbf{( 1)}m m k k k k k ? ? = ? = ? .\par
Clearly, the theorem holds for i m = . 
\section[{Inductive Hypothesis}]{Inductive Hypothesis}\par
Suppose the theorem holds for 2,3, 4,..., i p = for some clause 2 p m ? < . The total redundant assignments will be 2\par
; 3m p m p k k p k k p m ? ? ? ? = ? ? ? < ? . If a literal\par
with which an assignment agrees is in1 p + clause,\par
then the total redundant assignments will be1 ( 1) 1 ( 1) 2( 1) 2( 1) 2( 1) ; 2 ( 1) ( 1)\textbf{( 1)}\par
; 3m p m p m p m p m p m p k k k k k k i k k k k k k k i m k ? ? ? ? + ? ? ? ? + ? ? =? =? = ? ? ? ? ? = ? = ? ? ? ? ?\par
That is, the theorem holds for 1 p + . By induction on p , the theorem is true for all values of i .  x x x x x x x x x x x x x x x x x x x x x x x x 1 3 4 x x x 4 1 3 ( ) x x x ? ? 1 5 2 ( ) x x x ? ? 3 2 4 ( ) x x x ? ? ( D D D D D D D D ) Year 013 2 D . 
\section[{Base Case}]{Base Case}\par
The base case is when i m =\par
and the total number of assignments will be reduced by0 1 m m k k ? = = .\par
Clearly, the theorem holds for i m = .\par
Inductive Hypothesis Suppose the theorem holds for 2,3, 4,..., i p = for some clause 2 p m ? < . The total assignments will be reduced by m p k ? . If a literal with which an assignment agrees with is in 1 p + clause, then the total assignments will be reduced by1 ( 1) m p m p m p k k k k ? ? ? ? + = =\par
. That is, the theorem holds for 1 p + . There by induction on p , the theorem is true for all values of i . 
\section[{III.}]{III.} 
\section[{The Proposed Algorithm Pseudocode}]{The Proposed Algorithm Pseudocode}\par
The most important step in any complete or incomplete SAT algorithm is the decision over the value of a given variable in the formula. If the decision on that variable is wrong, the algorithm will waste its time searching for a solution before it discovers that the value assigned to the variable does not lead to a satisfying assignment and consequently a backtrack is done to change that value. The problem with making a decision for a variable x using the heuristics is that they do not consider how this decision or assignment will affect other related variables that appear in the same clauses as the variable x . If the search process keeps all possible assignments that satisfy a clause before moving forward, then no backtrack is needed. Instead, these assignments can be used to determine the values of variables that satisfy the next clauses. In the case that none of the variables in the current clause agrees with all the assignments, then the formula is unsatisfiable. This leads to the main idea of the proposed algorithm for assigning values to the variables. 
\section[{The Algorithm}]{The Algorithm} 
\section[{Input: F[m]; //formula with m clauses}]{Input: F[m]; //formula with m clauses}\par
Output : A[k m ]; //Possible assignment satisfying m clauses. 
\section[{getDistinctClauses(F[m]); 2. For i = 1 to disticntclauses.length -1;//number of distinct clauses For j = 1 to k //k is the number of literals in a clause LIT[i][j] := disticntclauses[i];}]{getDistinctClauses(F[m]); 2. For i = 1 to disticntclauses.length -1;//number of distinct clauses For j = 1 to k //k is the number of literals in a clause LIT[i][j] := disticntclauses[i];}\par
End for End for 
\section[{For i = 1 to k A[i] := LIT[1][i]; //literals of the first clause(initial set of satisfying substitutions) End for 4. For i = 2 to disticntclauses.length;//number of distinct clauses For j = 1 to k generateAssignment(LIT[i][j], A[], temp[]); //A[] contains the set of satisfying substitutions from previous clauses //temp[] contains assignments formed by combining assignments in A[] with a literal LIT[i][j] End for A[] := A[] + temp[];}]{For i = 1 to k A[i] := LIT[1][i]; //literals of the first clause(initial set of satisfying substitutions) End for 4. For i = 2 to disticntclauses.length;//number of distinct clauses For j = 1 to k generateAssignment(LIT[i][j], A[], temp[]); //A[] contains the set of satisfying substitutions from previous clauses //temp[] contains assignments formed by combining assignments in A[] with a literal LIT[i][j] End for A[] := A[] + temp[];}\par
End for 
\section[{For i = distinctclauses.length + 1 to m;//number of distinct clauses For j = 1 to k //k is the number of literals in a clause LIT[i][j] := nondistinctclauses[i]; End for End for}]{For i = distinctclauses.length + 1 to m;//number of distinct clauses For j = 1 to k //k is the number of literals in a clause LIT[i][j] := nondistinctclauses[i]; End for End for}\par
For i = distinctclauses.length to m For j=1 to k  
\section[{generateAssignment(LIT[i][j], A[], temp); End for removeSubsumedAssignments(tempassignments[], arraysubsumed[]); A[] := A[] + temp;}]{generateAssignment(LIT[i][j], A[], temp); End for removeSubsumedAssignments(tempassignments[], arraysubsumed[]); A[] := A[] + temp;}\par
End for 
\section[{If A[] is empty}]{If A[] is empty}\par
Output "the formula is unsatisfiable"; Else Output the assignments in A[] as the satisfying assignments for the formula F. 
\section[{Procedure getDistinctClauses(F[m])}]{Procedure getDistinctClauses(F[m])}\par
Input: Formula with m clauses Output: arrayofdistinctclauses and arrayofnondistinccaluses distinctclauses \hyperref[b0]{[1]} = clause \hyperref[b0]{[1]}  
\section[{Procedure: removeSubsumedAssignments(tempassignments[], arraysubsumed[])}]{Procedure: removeSubsumedAssignments(tempassignments[], arraysubsumed[])}\par
Input: list of assignments containing subsumed assignments and list of assignments subsuming the subsume assignments. Output: list of assignments without subsumed assignments. n:=0; For i = 0 to tempassignments.length -1\par
For j = 0 to arraysubsumeb.length -1 where m is some number of clauses. In step four, clauses in CLS could either be: 
\section[{If (arraysubsumed[j] is not contained in tempassignents[i]) arrayassignments[n++] = tempassignment[i] ; Endfor Endfor Return arrayassignments[];}]{If (arraysubsumed[j] is not contained in tempassignents[i]) arrayassignments[n++] = tempassignment[i] ; Endfor Endfor Return arrayassignments[];} 
\section[{Procedure: generateAssignment(lit, A[], temp[]); Input: a literal in a clause and a list of assignments in A[]. Output: a list of assignments stored in temp[] produced by combining lit with A[].}]{Procedure: generateAssignment(lit, A[], temp[]); Input: a literal in a clause and a list of assignments in A[]. Output: a list of assignments stored in temp[] produced by combining lit with A[].}\par
1.\par
2n k clauses (worst case). Because of the existence of repeated literals in Case 2, Case 1 will produce the maximum number of assignments (see  {\ref Theorem 3)}.\par
We now determine the number of possible assignments, ( ) A n , in the worst case. If the clauses in CLS have conflicting literals, ( )m A n k ? .\par
In this case, a literal in one clause will not be combined with a literal 1\par
x in another clause. The number of substitutions to be eliminated is shown by Theorem 2.\par
To count the exact number of assignments, the principle of inclusion-exclusion is used. The principle states that the number of elements that have property 1, property 2, property 3, ?, or property n is found by the summation.1 1 2 3 1 2 3 1 1 1\par
( , , ,..., ) ... ( 1) ... . For any satisfiability instance, the previous quantity cannot be found. That is because unlike the example given earlier, the arrangement of variables or literals differs from one instance to another. However, there is an arrangement that will produce the highest number of variables.n n i i j i j k n i n i j n i j k n 
\section[{N P P P P A A A A A A A A A A}]{N P P P P A A A A A A A A A A}+ ? ? ? < ? ? < < ? = ? ? + ? ? ? + ? ? ? ? ? ? ? ? If i P is 
\section[{b) The upper bound}]{b) The upper bound}\par
At this point, we need to prove two theorems. One that states case 1 is the worst case and the other states the arrangement that will produce the highest number of assignments. 
\section[{Theorem 3}]{Theorem 3}\par
In step 5 of the algorithm, generating assignments with the least number of clauses 
\section[{( ) n k}]{( ) n k}\par
that include 2n literals is the worst case. 
\section[{Proof}]{Proof}\par
If more than 2n k clauses are needed to include the 2n literals then we must have literals that are repeated. If we have one additional clause, then there must be k literals repeated and this will make the set of assignments to be excluded more than n. Having a repeated literal means that we have three clauses of this form:1 1 2 3 1 4 5 6 7 x x x x x x x x x ? ? ? ? ? ? .\par
The two clauses that have the repeated literal 1\par
x will produce the unnecessary assignments. These assignments are generated when the repeated literal is combined with the ( 1) k ? literals of the other clause.\par
This means that the assignments that include\{ \} 1 4 1 5 1 2 1 3\par
, , , x x x x x x x x are unnecessary. The only useful assignment is 1x produced from 1 1 ( ) x x . This indicates that 2( 1)\par
k ? sets of assignments should be discarded. In addition to these assignments, the two repeated literals when combined with 1\par
x will produce  
\section[{D}]{D}\par
The first three steps of the algorithm take polynomial time of number of clauses. Steps four and five are clearly the main contributors to the time complexity of the whole algorithm. These two steps rely on the number of assignments generated in each iteration of the for-loop. For step four, that number is determined by the clauses in CLS and for step five, that number is determined by the end of step four. Therefore, let us start with step four.\par
The proof of the principle can be found in \hyperref[b24]{(Rosen, 1999)}.\par
two sets of assignments of the form 1 1 ( ) x x that are also discarded from the total number of assignments when we count them using the inclusion exclusion principle. Therefore, a repeated literal will result to discard 2( 1) 1 k ? + additional sets excluded.\par
Writing the inclusion exclusion series with n sets plus (2( 1) 1) k k ? + sets is hard because there will be many possibilities for the intersection of sets. The approach to show that 2n/k is the worst case is to exclude the additional sets first from the total number of assignments and compare that with the worst case. The number of assignments of the additional sets can be counted by: ( 1) (2( 1) 1) ( , )n n k k n n k k k k k n k i i i k i A k C k k k C k k k C k k k C k k k k C k i k ? ? ? ? + + ? + + = = ? + ? ? + + ? + ? + ? ? + = ? ? + ?\par
Excluding this from the total assignments2 2 1 2 1 1 1 2 2 1 2\textbf{1 2( ) 1 ( 1) (2( 1) 1) ( , ) ( ( 1) (2( 1) 1) ( , )}\par
)n n k i i i k k i n k k k i i k i k i N k k C k i k N k k k C k i k + ? + + = ? + + ? = = ? ? ? + = ? ? ? + ? ? Evaluating 2\textbf{1 2( ) 1 ( ( 1) (2( 1) 1) ( , )}\par
)k k i i k i i k k C k i k + ? = ? ? ? + ?\par
for values of k gives quantity less than2 1 k k ?\par
and result to a number of assignments less than 2n k k and excluding the n sets of the form (v -v) from N gives a value that is less than the one in the worst case.2n k k excld(n sets) 2 2 1 2\textbf{1 2( ) 1 ( ( 1) (2( 1) 1) ( , )}\par
)n k k k i i k i k i k k k C k i k ? + + ? = > ? ? ? + ? excld(n sets) because 2n k k 2 2 1 2\textbf{1 2( ) 1 ( ( 1) (2( 1) 1) ( , ) )}\par
.n k k k i i k i k i k k k C k i k ? + + ? = > ? ? ? + ?\par
This is for one additional clause. For i additional clauses the limit of the summation is to ik and this also will give the same result.\par
Theorem 3 tells us that step six will not generate assignments that are more than step five. This should make step 5 the dominant factor for time complexity. 
\section[{Theorem 4}]{Theorem 4}\par
For the worst case, the upper bound is ( ( 1))n k k k ? Proof\par
The inclusion-exclusion principle takes care of assignments that are counted more than once by considering the intersections between the n sets to be excluded as seen in the summation. Therefore, the least value of x literals:1 2 3 1 4 5 x x x x x x\par
The assignments that include 1\par
x and 1 x can never occur with assignments that include 2\par
x and 2 x , ( 1) k k ? assignments, then the number of assignments will be ( 1)n k k k ? . c) Related Work\par
Complete algorithms for SAT satisfiability problems include those algorithms that can state whether or not a SAT instance is satisfiable, giving a 'yes' answer together with a satisfying assignment or a 'no' answer as the case may be. The first complete algorithm is the Davis Putnam procedure . This procedure is based on resolution rule to eliminate variables one by one till the formula is satisfied. When a variable is eliminated in each iteration, all resolvents are added to the set of the clauses. This algorithm requires polynomial space. It handles CNF formulas and it is one of the efficient SAT algorithms. \hyperref[b7]{(Davis, Logemann, \& Loveland, 1962}) Developed a divide-and-conquer algorithm that enhances on . This improved algorithm is the main procedure for most state-of-the-art SAT solvers today.\par
The search space of DPLL could grow as large as 2 n which is the worst case for any complete algorithm. Due to the possibility of consuming huge amount of time, researchers have been focusing on mechanisms to reduce that and came up with more reasonable time complexities. These improvements usually come in two aspects: the decision to branch to next literal and the backtracking mechanism if a solution is not found in the chosen branch. The achievements accomplished in improving SAT algorithm in these two aspects show that the complexity could be reduced significantly.\par
i. Branching Decisions DPLL procedure chooses any literal for branching and goes down that region in the search space. The procedure will spend time searching for a solution and if it discovers that the branch is not successful, it backtracks to the other branch and continues searching. Choosing the next literal for branching more carefully will allow the algorithm to save time exploring a region where a satisfying assignment cannot be found at all and direct the searching to regions where a solution is likely to be found. In order to accomplish this, several heuristics have been proposed and the most effective ones can be found in \hyperref[b1]{(Bruni \& A., 2003} ii. Backtracking Mechanisms When the algorithm fails to find an answer or an empty clause (contradiction) appears down the path of the search tree, it backtracks to a certain point and continues searching in another part of the tree. The DP backtracks to the most recently untoggled (complemented) literal and tests its complement branch. As mentioned earlier this will cost a lot of time for DP to discover that this part of the search space does not have a solution and search for a solution elsewhere. For backtracking in the DP procedure, much work has not been done as compared to branching decision. This is due to the fact that backtracking is an essential step in any algorithm to prove its completeness. Nevertheless, there are a number of proposals to improve the backtracking in the DP procedure.  
\section[{iii. Upper Bounds}]{iii. Upper Bounds}\par
The improvements made in backtracking and branching heuristics are of practical interests. However, the experimental analysis of these improvements indicates that satisfiability could be solved in time less than 2 n . A number of people gave lower bounds for this problem but most of them rely on a certain structure or property that exists in the formula. The following are some of the achievements made to find an upper bound that is better than the trivial one. 
\section[{a. Autarkness Principle}]{a. Autarkness Principle}\par
The first attempt to achieve a non-trivial upper bound for SAT was done by \hyperref[b21]{(Monien \& Speckenmeyer, 1985)}. They introduced the notion of autarks which are partial assignments of variables. If all clauses that include the variables in the assignment are satisfied, then that assignment is an autark. They proved that the time complexity of their algorithm is  When dealing with 3-SAT problem, the clauses with 2 literals help in reducing the search space. Schiermeyer was the first to make use of the number of clauses with 2 literals after the resolution step is made \hyperref[b25]{(Schiermeyer, 1993)}. He said that for the next branch, a 2-clause is chosen such that it produces at least one new 2-clause in every branch that follows. With the help n ). \hyperref[b15]{(Kullmann, 1999)} showed that the algorithm of Schiermeyer can perform better through a new concept called blocked clauses. A clause C is blocked for a literal l if every clause C' containing l has also another literal that is complemented with C. By making use of these blocked clauses, Kullmann proved that the algorithm in \hyperref[b25]{(Schiermeyer, 1993)}  \begin{figure}[htbp]
\noindent\textbf{4}\includegraphics[]{image-2.png}
\caption{\label{fig_2}3 x and 4 x}\end{figure}
           			\footnote{© 2013 Global Journals Inc. (US) Global Journal of Computer Science and Technology} 			\footnote{Communications of the ACM, 5, (pp. 394-397).} 			\footnote{© 2013 Global Journals Inc. (US)} 		 		\backmatter  			 \par
respectively where m is the number of clauses and L is the length of the formula. An improvement was made to the second algorithm in \hyperref[b10]{(Hirsch, 2000)} to become O( 0.10299L 
\subsection[{2}]{2}\par
).\par
e. Covering Codes \hyperref[b4]{(Danstin, et al., 2002)} proposed a deterministic algorithm that is based on covering codes. This algorithm can be seen as a derandomization of \hyperref[b26]{(Schoning, 1999)} algorithm that uses random walk model. The search space is divided into group of assignments say balls of some radius r. Each group or ball represents some assignment a and all assignments that differ with it in r variables. The algorithm checks in each ball if there is a satisfying assignment and if there is none in any ball then the formula is unsatisfied. The authors of \hyperref[b4]{(Danstin, et al., 2002)} showed that the time complexity of this V. 
\subsection[{Conclusion and Future Work}]{Conclusion and Future Work}\par
The proposed does not require the clauses or the formula to have any specific structure to achieve a competitive upper bound which is a significant advantage over the existing algorithms in the literature where they derive their time complexity based on a property that must exist in the formula. The algorithm gives a new insight towards solving SAT. Most of the other algorithms are based on the classical rule of splitting the search space into regions and search for a solution in each one. The new perspective of the algorithm has the potential to design further effective SAT algorithms that outperforms the existing ones in theory and practice.\par
The implementation of the proposed algorithm will be considered in future work. The algorithm proposed here can also be improved. The time complexity of the proposed algorithm is based on preprocessing of clauses in the formula. This arrangement is so unlikely to exist in all clauses considered. That means that there exists a tighter upper bound for the algorithm but to achieve that the order in which clauses are considered should be more intelligent. To show that such an upper bound exists, many cases have to be covered and counted. Parallelisation of the proposed algorithm is also a potential future work.			 			  				\begin{bibitemlist}{1}
\bibitem[Marques-Silva and Sakallah ()]{b20}\label{b20} 	 		\textit{},  		 			J P Marques-Silva 		,  		 			K A Sakallah 		.  	 	 		\textit{IEEE Transactions on Computers. GRASP-A Search Algorithm for Propositional Satisfiability}  		1999. p. .  	 
\bibitem[Bruni ()]{b1}\label{b1} 	 		‘A Complete Adaptive Algorithm for Propositional Satisfiability’.  		 			R Bruni 		,  		 			S 		.  	 	 		Discrete Applied Mathematics  		2003. p. 127.  	 
\bibitem[Davis and Putnam ()]{b5}\label{b5} 	 		‘A Computing Procedure for Quantification Theory’.  		 			M Davis 		,  		 			H Putnam 		.  	 	 		\textit{Journal of Association for Computing Machinery}  		1960. p. .  	 
\bibitem[Davis and Putnam ()]{b6}\label{b6} 	 		‘A Computing Procedure for Quantification Theory’.  		 			M Davis 		,  		 			H Putnam 		.  	 	 		\textit{Journal of Association for Computing Machinery}  		1960. p. .  	 
\bibitem[Danstin et al. ()]{b4}\label{b4} 	 		‘A Deterministic (2-2 / k+1)n Algorithm fork-SAT based on Local Search’.  		 			E Danstin 		,  		 			A Goerdt 		,  		 			E A Hirsch 		,  		 			R Kannan 		,  		 			J Kleinberg 		,  		 			C Papadimitriou 		.  	 	 		\textit{Theoretical Computer Science}  		2002. p. .  	 
\bibitem[Davis et al. ()]{b7}\label{b7} 	 		\textit{A Machine Program for Theorem Proving},  		 			M Davis 		,  		 			G Logemann 		,  		 			D Loveland 		.  		1962.  	 
\bibitem[Schoning ()]{b26}\label{b26} 	 		‘A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems’.  		 			U Schoning 		.  	 	 		\textit{Proceedings of the 40th Annual Symposium on Foundations of Computer Science (FOCS)},  				 (the 40th Annual Symposium on Foundations of Computer Science (FOCS))  		1999. IEEE. p. .  	 
\bibitem[Hooker and Vinay ()]{b12}\label{b12} 	 		\textit{Branching Rules for Satisfiability. GSIA Working Paper 1994-09. Pennsylvania: Graduate School of Industrial Administration},  		 			J N Hooker 		,  		 			V Vinay 		.  		1994. Pittsburgh.  		 			Carnegie-Mellon University 		 	 
\bibitem[Lynce and Marques-Silva ()]{b18}\label{b18} 	 		‘Building Stateof-The-Art SAT Solver’.  		 			I Lynce 		,  		 			J Marques-Silva 		.  	 	 		\textit{Proceedings of the European Conference on Artificial Intelligence (ECAI)},  				 (the European Conference on Artificial Intelligence (ECAI))  		2002. p. 105.  	 
\bibitem[Pretolani ()]{b23}\label{b23} 	 		‘Efficient and Stability of Hypergraph SAT Algorithms’.  		 			D Pretolani 		.  	 	 		\textit{Proceedings of DIMACS Challenge II Workshop},  				 (DIMACS Challenge II Workshop)  		1993.  	 
\bibitem[Moskewicz et al. ()]{b22}\label{b22} 	 		‘Engineering an Efficient SAT Solver’.  		 			M Moskewicz 		,  		 			C Madigan 		,  		 			Y Zhao 		,  		 			L Zhang 		,  		 			S Malik 		.  	 	 		\textit{Proceedings of the Design Automation Conference},  				 (the Design Automation Conference)  		2001.  	 
\bibitem[Crawford and Baker ()]{b3}\label{b3} 	 		\textit{Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems},  		 			J M Crawford 		,  		 			A B Baker 		.  		1994. AAAI-94.  	 
\bibitem[Stallman and Sussman ()]{b27}\label{b27} 	 		‘Forward Reasoning \& Dependencydirected Backtracking in A System for Computeraided Circuit Analysis’.  		 			R M Stallman 		,  		 			G J Sussman 		.  	 	 		\textit{Artificial Intelligence}  		1977. 9 p. .  	 	 (Artificial Intelligence 9) 
\bibitem[Li and Anbulagan ()]{b17}\label{b17} 	 		‘Heuristics Based on Unit Propagation for Satisfiability Problems’.  		 			C M Li 		,  		 			Anbulagan 		.  	 	 		\textit{Proceedings of 15th International Joint Conference on Artificial Intelligence},  				 (15th International Joint Conference on Artificial IntelligenceNagoya, Japan)  		1997. 1 p. .  	 
\bibitem[Freeman ()]{b9}\label{b9} 	 		\textit{Improvements to Propositional Satisfiability Search Algorithms},  		 			J W Freeman 		.  		1995.  		 			Computer and Information Science, University of Pennsylvania 		 	 	 (Ph. D. Dissertation. Department of) 
\bibitem[Kullmann ()]{b15}\label{b15} 	 		‘New Methods for 3-SAT Decision and Worst Case Analysis’.  		 			O Kullmann 		.  	 	 		\textit{Theoretical Computer Science}  		1999. p. .  	 
\bibitem[Hirsch ()]{b10}\label{b10} 	 		‘New Worst Case Upper Bounds for SAT’.  		 			E Hirsch 		.  	 	 		\textit{Journal of Automated Reasoning}  		2000. 24 p. .  	 
\bibitem[Devadas ()]{b8}\label{b8} 	 		‘Optimal Layout via Boolean Satisfiability’.  		 			S Devadas 		.  	 	 		\textit{Proceedings of ICCAD 89},  				 (ICCAD 89)  		1989. p. .  	 
\bibitem[Kauts and Selman ()]{b14}\label{b14} 	 		‘Planning as Satisfiability’.  		 			H Kauts 		,  		 			B Selman 		.  	 	 		\textit{Proceedings of the 10th European Conference on Artificial Intelligence (ECAI 92},  				 (the 10th European Conference on Artificial Intelligence (ECAI 92)  		1992.  	 
\bibitem[Rosen ()]{b24}\label{b24} 	 		 			K H Rosen 		.  		\textit{Discrete Mathematics and Its Applications},  				1999. McGraw Hill.  	 	 (4th Edition ed.) 
\bibitem[Barbour ()]{b0}\label{b0} 	 		‘Solutions to The Minimization Problem of Fault-Tolerant Logic Circuits’.  		 			A E Barbour 		.  	 	 		\textit{IEEE Transactions on Computers}  		1992. 41  (4)  p. .  	 
\bibitem[Schiermeyer ()]{b25}\label{b25} 	 		‘Solving 3-Satisfiability in less than 1.579n’.  		 			I Schiermeyer 		.  	 	 		\textit{Selected papers from Computer Science Logic 12},  				1993. 702 p. .  	 
\bibitem[Jeroslow and Wang ()]{b13}\label{b13} 	 		‘Solving Propositional Satisfiability Problems’.  		 			R G Jeroslow 		,  		 			J Wang 		.  	 	 		\textit{Annals of Mathematics \& Artificial Intelligence}  		1990. 1 p. .  	 
\bibitem[Monien and Speckenmeyer ()]{b21}\label{b21} 	 		‘Solving Satisfiability in less than 2n steps’.  		 			B Monien 		,  		 			E Speckenmeyer 		.  	 	 		\textit{Discrete Applied Mathematics}  		1985. p. .  	 
\bibitem[Larrabee ()]{b16}\label{b16} 	 		‘Test Pattern Generation Using Boolean Satisfiability’.  		 			T Larrabee 		.  	 	 		\textit{IEEE Transactions Computer Aided Design}  		1992. 1 p. .  	 
\bibitem[Cook ()]{b2}\label{b2} 	 		‘The Complexity of Theorem Proving Procedures’.  		 			S Cook 		.  	 	 		\textit{Proceedings of the 3rd Annual ACM Symposium on Theory of Computing},  				 (the 3rd Annual ACM Symposium on Theory of Computing)  		1971. p. .  	 
\bibitem[Lynce and Silva ()]{b19}\label{b19} 	 		\textit{The Effect of Nogood Recording in MAC-CBJ SAT Algorithms},  		 			I Lynce 		,  		 			J P Silva 		.  		 RT/4/2002.  		2002.  	 	 (Technical Report) 
\bibitem[Hirsch ()]{b11}\label{b11} 	 		‘Two New Upper Bounds for SAT’.  		 			E Hirsch 		.  	 	 		\textit{Proceedings of 9th Annual ACM Siam Symposium on Discrete Algorithms},  				 (9th Annual ACM Siam Symposium on Discrete Algorithms)  		1998. p. .  	 
\end{bibitemlist}
 			 		 	 
\end{document}
