\documentstyle[jair,twoside,11pt,theapa]{article}
\input epsf %% at top of file

\jairheading{1}{1994}{309-314}{1/94}{6/94}
\ShortHeadings{Applying GSAT to Non-Clausal Formulas}{Sebastiani}
\firstpageno{309}

\setcounter{totalnumber}{1}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% INSERTED MACROS                                                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                   %
%%% This file contains the definition of the invironments for         %
%%% writing theorems, proofs, definitions, various enumeration        %
%%% environments, etc. etc. ...      %                                %
%%%                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                   %
%%% \newplaintheorem{<name>}{<text>}                                  %
%%%                                                                   %
%%% has the same effect as \newtheorem{<name>}{<text>}, except that   % 
%%% the text within the theorem is not written in italic style        %
%%%                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\newplaintheorem#1#2{%
\newtheorem{#1plain}{#2}[section]%
\newenvironment{#1}{\begin{#1plain}\rm }{\end{#1plain}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                   %
%%% \makenewenumerate{<name>}{<itemformat>}                           %
%%%                                                                   %
%%% create a list environment named <name> whose items are labeled    %
%%% as specified in <itemformat>. <itemformat> can contain the counter%
%%% cnt<name> which is created by this macro.                         %
%%%                                                                   %
%%% for example:                                                      %
%%%                                                                   %
%%% \makenewenumerate{Aromanenumerate}{(A\roman{cntromanenumerate})}  %
%%%                                                                   %
%%% generate the new list environment `Aromanenumerate' such that:    %
%%%                                                                   %
%%% \begin{Aromanenumerate}                                           %
%%% \item first bla bla...                                            %
%%% \item second bla bla...                                           %
%%% ...                                                               %
%%% \end{Aromanenumerate}                                             %
%%%                                                                   %
%%% produces the output:                                              %
%%%                                                                   %
%%%    (Ai) first bla bla...                                          %
%%%   (Aii) second bla bla...                                         %
%%%   ......                                                          %
%%%                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\makenewenumerate#1#2{%
\newcounter{cnt#1}
\newenvironment{#1}%
{\begin{list}{\makebox[0pt][r]{#2}}%
{\setlength{\itemsep}{0pt}%
 \setlength{\parsep}{.2em}%
 \setlength{\leftmargin}{2em}%
 \setlength{\labelwidth}{.4em}%
 \usecounter{cnt#1}}}%
{\end{list}}}

\newtheorem{definition}{Definition}[section]
\newtheorem{intfact}{Intuitive Fact}[section]
\newtheorem{proposition}{Proposition}[section]
\newtheorem{conjecture}{Conjecture}[section]
\newtheorem{theorem}{Theorem}[section]
\newtheorem{corollary}{Corollary}[section]
\newtheorem{lemma}{Lemma}[section]
\newplaintheorem{notation}{Notation}
\newplaintheorem{remark}{Remark}
\newplaintheorem{example}{Example}
\newenvironment{proof}{{\bf Proof }}{\mbox{\hspace{0cm}}\hfill Q.E.D.} 

\makenewenumerate{renumerate}{\rm(\roman{cntrenumerate})}
\makenewenumerate{renumerateprime}{\rm(\roman{cntrenumerateprime}$'$)}
\makenewenumerate{renumeratesecond}{\rm(\roman{cntrenumeratesecond}$''$)}

\makenewenumerate{aenumerate}{({\it\alph{cntaenumerate}})}
\makenewenumerate{aenumerateprime}{({\it\alph{cntaenumerateprime}$'$})}
\makenewenumerate{aenumeratesecond}{({\it\alph{cntaenumeratesecond}$''$})}

\newcommand{\TODOitem}{\fbox{\bf To do}}
\newcommand{\TODO}[1]{\begin{itemize} \item[\TODOitem]#1\end{itemize}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% The environment ``sentence'' is the analogous of the environment         %
%%% equation for the natural language sentences.                             %
%%%                                                                          %
%%% The latex source:                                                        %
%%%                                                                          %
%%% \begin{sentence}                                                         %
%%% \label{labeltext}                                                        %
%%% text                                                                     %
%%% \end{sentence}                                                           %
%%%                                                                          %
%%% generates a left numbered statement which can be refered by the command  %
%%% \ref{labeltest}. The \label command can be omitted.                      %
%%% The environment ``sentence'' uses the same counter as the ``equation''   %
%%% and ``eqnarray'' environments.                                           %
%%%                                                                          %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcounter{sentencecnt}
\setcounter{sentencecnt}{0}
\newenvironment{sentence}%
 {\begin{list}%
  {\makebox[2em][l]{(\arabic{sentencecnt})}}%
  {\usecounter{sentencecnt}%
   \setlength{\leftmargin}{5em}%
   \setlength{\labelwidth}{2em}%
   \setlength{\labelsep}{3em}%
   \setlength{\itemsep}{\parsep}%
   \setcounter{sentencecnt}{\value{equation}}}\item}%
 {\setcounter{equation}{\value{sentencecnt}}\end{list}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                   %
%%% By the environments "bnf" you can write a bnf grammar as follows: %
%%%                                                                   %
%%% \begin{bnf}                                                       %
%%% \T{aa} \sep \T{bbb} | \T{ccc} \\                                  %
%%% \T{bbb} \sep \T{bbb} BBB | \\                                     %
%%%            & \T{eee}  \\                                          %
%%% \T{eeeeeee} \sep EEE | FFF | \\                                   %
%%%            & GGG | \\                                             %
%%%            & HHH                                                  %
%%% \end{bnf}                                                         %
%%%                                                                   %
%%% obtaining the output:                                             %
%%%                                                                   %
%%%      <aa> ::= <bbb> | <ccc>                                       %
%%%     <bbb> ::= <bbb> BBB                                           %
%%%               <eee>                                               %
%%% <eeeeeee> ::= EEE | FFF |                                         %
%%%               GGG |                                               %
%%%               HHH                                                 %
%%%                                                                   %
%%% in a \tt style.                                                   %
%%%                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\sep}{::= &}
\newcommand{\T}[1]{{\tt <#1>}}
\newenvironment{bnf}{\begin{quote}\tt \begin{tabular}{rl}}{\end{tabular}\end{quote}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                   %
%%% This environment writes a boxed verbatim text;                    %
%%%                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newlength{\verbboxwidth}% 
\setlength{\verbboxwidth}{\textwidth}
\addtolength{\verbboxwidth}{-2\arrayrulewidth}
\addtolength{\verbboxwidth}{-2\tabcolsep}
\newenvironment{boxverbatim}%
   {\begin{flushleft}%
    \begin{tabular}{|l|}\hline%
    \\%
    \begin{minipage}{\verbboxwidth}}%
   {\vspace*{.5\baselineskip}%
    \end{minipage}%
    \\\hline%
    \end{tabular}%
    \end{flushleft}}




\newcommand{\gap}{\vspace{0.2cm}}

\newcommand{\vi}{\varphi}
\newcommand{\vim}{$\varphi$}
\newcommand{\vk}{\varphi_k}
\newcommand{\vkm}{$\varphi_k$}
\newcommand{\ai}{V_i}
\newcommand{\aim}{$V_i$}
\newcommand{\ar}{V_r}
\newcommand{\arm}{$V_r$}

\newcommand{\noi}{\noindent}
\newcommand{\iffo}{INF}
\newcommand{\ti}{T_{i}}
\newcommand{\tr}{T_{r}}
\newcommand{\tri}{T_{ri}}
\newcommand{\trr}{T_{rr}}


\newcommand{\dsi}{\Delta s_i}
\newcommand{\dsim}{$\Delta s_i$}
\newcommand{\dsr}{\Delta s_r}

\newcommand{\scorepos}[2]{\mbox{$s(#1,#2)$}}
\newcommand{\scoreneg}[2]{\mbox{$s^{-}(#1,#2)$}}

\newcommand{\I}[1]{\scorepos{T}{#1}}
\newcommand{\II}[1]{\scorepos{\ti}{#1}}
\newcommand{\IR}[1]{\scorepos{\tr}{#1}}
\newcommand{\IRR}[1]{\scorepos{\tri}{#1}}
\newcommand{\IRI}[1]{\scorepos{\trr}{#1}}

\newcommand{\NI}[1]{\scoreneg{T}{#1}}

\newcommand{\NII}[1]{\mbox{$s^{\pm}(#1,T)$}}
\newcommand{\NIII}[1]{\mbox{$s^{\pm}(#1,\ti)$}}


\newcommand{\sfi}{F_{\varphi}^{\ai}}
\newcommand{\sfm}{\overline{F}_{\varphi}}


\newcommand{\Ti}[1]{\mbox{$Time(\I{#1})$}}
\newcommand{\Nti}[1]{\mbox{$Time(\NI{#1})$}}
\newcommand{\PNti}[1]{\mbox{$Time(\NII{#1})$}}
\newcommand{\F}[1]{\mbox{$F(#1,T)$}}
\newcommand{\sco}[1]{\scorepos{T}{#1}}
\newcommand{\scoi}[1]{\scorepos{\ti}{#1}}
\newcommand{\C}[1]{\mbox{$\overline{C}_{#1}$}}
\newcommand{\li}[1]{\mbox{$\overline{l}_{#1}$}}
\newcommand{\CI}[1]{\mbox{$C_{#1}^{\ai}$}}

\renewcommand{\gap}{\vspace{0.1cm}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                         %
%%% BEGIN OF DOCUMENT                                                       %
%%%                                                                         %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\title{Applying GSAT to Non-Clausal Formulas}

\author{\name Roberto Sebastiani \email rseba@dist.unige.it\\
\addr Mechanized Reasoning Group, DIST,
 viale Causa 13, 16145 Genova, Italy. \\
Mechanized Reasoning Group, IRST,
loc. Pant\`e, 38050  Povo, Trento, Italy.
}

\begin{LARGE}
\begin{it}
\noindent
Research Note
\end{it}
\end{LARGE}

\maketitle


\begin{abstract}
\noindent In this paper we describe how to modify GSAT so that it can be
applied  to non-clausal formulas.
 The idea is to use  a particular ``score'' function which gives the number of 
clauses of 
the CNF conversion of a formula which are false under a given   truth
assignment. Its value is computed in linear time, without constructing  the
 CNF conversion itself.  
The proposed methodology applies to most of the variants of GSAT proposed so far.
\end{abstract}


        
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% INTRODUCTION                                                           %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Introduction}
\label{intro}


GSAT \cite{selman1,selman2} is an incomplete 
 model-finding algorithm for clausal propositional formulas which performs a
  randomized local search.
GSAT has been shown to solve many ``hard'' problems
much more efficiently than other traditional algorithms like, e.g., DP
\cite{davis2}.
Since GSAT applies only to clausal formulas, using it to find models for ordinary 
propositional formulas requires some previous clausal-form conversion.
This requires extra  computation (which can be
extremely heavy  if the ``standard'' clausal conversion is used).
Much worse, clausal-form conversion  causes either a large increase in the size of
 the input formula or an enlargement of the search space. 


In this paper we describe how to modify GSAT so that it can be
applied   to non-clausal formulas {\em directly\/}, i.e., with no previous
clausal form conversion. An extended version of the
paper (Sebastiani, 1994) provides the proofs of the theorems and a detailed
description of the algorithm introduced.


This achievement could enlarge GSAT's application domain.
\citeA{selman1} suggest that some traditional AI problems  
can be formulated as model-finding tasks; e.g., 
visual interpretation \cite{reiter6}, planning \cite{kautz2}, 
generation of ``vivid'' knowledge representation \cite{levesque3}.  
It is often the case  that non-clausal representations are more compact for 
such problems. For instance, 
each rule in the form 
``$\bigwedge_i \phi_i \supset \psi$'' gives  rise to 
several %a relevant number of 
distinct clauses if some $\phi_i$ are  disjuncts or $\psi$ is 
a conjunct.
In automated theorem proving (a.t.p.) some applications of model-finding
have been proposed  
(see, e.g., \cite{artosi1,klingerbeck1}). 
For instance, some decision procedures 
for decidable subclasses of first-order logic 
iteratively perform   non-clausal model-finding for propositional instances 
of the input formulas \cite{jeroslow2}. 
More generally, some
model-guided techniques for proof search,  
like {\em goal deletion\/} \cite{ballantyne1}, {\em false preference\/}, 
or {\em semantic resolution\/} \cite{slaney1},  seem to be applicable 
to non-clausal a.t.p. as well.



\newpage
\section{GSAT}
\label{gsat}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% GSAT                                                                    %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{figure}[t]
\begin{center}
\makebox[3.902in][l]{ %3.902in
\vbox to 2.319in{%2.819in
\vfill
%\setlength{\unitlength}{0.0081in}%
\vspace{-1.cm}
\begin{tabbing}
\hspace{.7cm}\= \hspace{.7cm}\= \hspace{.7cm}\= \hspace{.7cm}\= \hspace{.7cm}\= \hspace{5cm}\= \hspace{.7cm}\= \hspace{.7cm}\= \\
{\bf procedure} {\em GSAT($\phi$)\/}\\
\>{\bf for\/} $j := 1$ {\bf to\/} {\em Max-tries} {\bf do\/}\\
\>\>{\em T\/} := {\em initial($\phi$)\/}  \>\>\>\>\>%; generate an initial assignment
\\
\>\>{\bf for\/} $k := 1$ {\bf to\/} {\em Max-flips}  {\bf do\/}\\
\>\>\>{\bf if\/} $T \models \phi$ \\
\>\>\>{\bf then\/} {\bf return\/} {\em T\/}\\
\>\>\>{\bf else\/}\ \= {\em Poss-flips\/} := {\em hill-climb($\phi,T$)\/} 
\>\>%; compute best ``neighbours''
\\
\>\>\>\>{\em V\/} := {\em pick(Poss-flips)\/} \>\>%; pick one variable to flip
\\
\>\>\>\>{\em T\/} := {\em flip(V,T)\/} \>\>%; invert (``flip'')  {\em V\/} inside {\em T\/}
\\
\>\>\>\>{\em UpdateScores($\phi,V$)\/} \>\>%;  update  the values of \dsim 
\\
\>\>{\bf end\/}\\
\>{\bf end\/}\\
\>{\bf return\/} ``no satisfying assignment found''.\\
\end{tabbing}
  }
}
\caption{A general schema for GSAT.}
\end{center}
\label{GSATschema}
\vspace{-.5cm}
\end{figure}


If $\phi$ is a clausal propositional formula and $T$ is a 
truth assignment for the variables of $\phi$, then 
the number of  clauses of  $\phi$ which are  falsified by
$T$ is called the {\em score\/} of $T$ for $\phi$ ($score(T,\phi)$). 
$T$ satisfies $\phi$ iff  $score(T,\phi) = 0$.
The notion of score plays a key role in GSAT, as it is considered as the 
``distance'' from a truth assignment to a satisfying one.

The schema of Figure \ref{GSATschema} describes GSAT as well as
many of its possible variants. We use the  notation from \cite{gent2}. 
GSAT performs an iterative search for a satisfying truth assignment for 
 $\phi$, starting from
 a random assignment
 provided by {\em initial()\/}. At each step, 
the successive assignment is obtained by flipping (inverting) the truth value 
of one single variable $V$ in $T$.
$V$ is chosen to minimize the  score. 
Let  $\ti$ be the assignment obtained from $T$ by flipping its $i$-th variable 
$\ai$. 
 {\em hill-climb()\/} returns the set 
{\em Poss-flips\/} of the variables $\ar$ which minimize $score(T_r,\phi)$.
If the current values of  $\dsi =  score(T_i,\phi) - score(T,\phi)$ 
are stored for every variable $\ai$, then 
 {\em hill-climb()\/} simply returns the set 
of the variables $\ar$ with the best $\dsr$. 
{\em pick()\/} chooses randomly one of such variables. {\em flip()\/} returns 
$T$ with $V$'s value flipped.  After each flipping, {\em UpdateScores()\/}
updates the values of $\dsi$, for all $i$. 


This paper exploits the observation that the functions 
{\em  initial()\/},  {\em  hill-climb()\/}, {\em  pick()\/}  and  {\em
flip()\/} do not depend on the structure of the input formula $\phi$, and that 
%in the  schema of Figure \ref{GSATschema} 
the computation of the scores is the only step  
where the input formula $\phi$ is required to be in clausal form. 
The idea is thus to find a suitable notion of score for non-clausal 
formulas, and an efficient algorithm computing it.

%Thus, if we find a suitable notion of score for non-clausal 
%formulas and an efficient algorithm to compute it, then we shall be able to apply 
%the GSAT algorithm to non-clausal formulas {\em directly\/}, i.e., without
%clausal form  conversion. 

%Thus, the problem  of applying GSAT directly to non-clausal formulas can be 
%solved by finding a suitable easy-to-compute notion of score for non-clausal 
%formulas.



%\newpage
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% SCORE                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{An extended notion of score}
\label{algorithm}


Let {\em cnf($\varphi$)\/} be the result of
converting a propositional formula $\varphi$ into clausal form by
the standard method (i.e.,  
by applying the rules of De Morgan). Then the following definition
extends the  notion of score to all propositional formulas.


\begin{definition}
\label{scoredef}
 The  {\em score\/} of a truth assignment $T$ for a propositional formula 
$\varphi$ is 
the number of the clauses of cnf($\varphi$) which are falsified by $T$.  
\end{definition}

\noi %We claim this is a very suitable definition for our purposes. 
{\em cnf()\/} represents the ``natural'' clausal form conversion. 
%Unlike in the other conversion methods,  
{\em cnf($\vi$)\/} has
the same number of propositional variables as $\vi$ and it is logically 
equivalent to $\vi$. 
The problem with {\em cnf()} is the exponential size growth of {\em cnf($\vi$)\/}, that is, $|cnf(\varphi)| = O(2^{|\varphi|})$.
Definition \ref{scoredef} overcomes such a problem, for it is possible to
 introduce a linear-time computable function $\sco{\varphi}$ which gives 
the score of $T$ for a formula $\vi$. This is done  {\em directly}, i.e., without
converting $\varphi$ into clausal form.
We define $\I{\varphi}$  recursively as follows:
\footnote{Notice that the definition of $\I{\vi}$ can be easily extended 
to formulas 
involving other connectives (e.g.,  {\em nand\/}, 
{\em nor\/}, {\em xor\/}, {\em if-then-else\/}, \ldots) or more complicate
 boolean functions.}   

\begin{center}
\begin{tabular}{|l|l|l|} \hline
\label{fundef}
$\varphi $ & $ \I{\varphi} $ & $ \NI{\varphi} $ \\ \hline
$\varphi \ literal $ & 
 $\left\{
\begin{array}{c}
 0 \hspace{.7cm} if\ T \models  \varphi\\    
 1 \hspace{.7cm} {\em otherwise\/}
\end{array}\right. $ & 
 $\left\{
\begin{array}{c}
 1 \hspace{.7cm} if\ T \models  \varphi\\    
 0 \hspace{.7cm} {\em otherwise\/}
\end{array}\right. $ \\ 
$\neg \varphi_{1}$ & $\NI{\varphi_{1}}$ & $\I{\varphi_{1}} $\\
$ \bigwedge_k \varphi_{k} $ & $  \sum_{k} \I{\varphi_{k}} $ & $ \prod_{k} \NI{\varphi_{k}} $ \\
$ \bigvee_k \varphi_{k} $ & $ \prod_{k} \I{\varphi_{k}} $ & $ \sum_{k} \NI{\varphi_{k}} $ \\
$\varphi_{1} \supset \varphi_{2}$ & $ \NI{\varphi_{1}} \cdot \I{\varphi_{2}} $ & $ \I{\varphi_{1}} + \NI{\varphi_{2}}$ \\
$\varphi_{1} \equiv \varphi_{2} $ & 
$\begin{array}{c}
\NI{\varphi_{1}} \cdot \I{\varphi_{2}} + \\
\I{\varphi_{1}} \cdot \NI{\varphi_{2}}
\end{array} $ &
 $ \begin{array}{c}
(\I{\varphi_{1}} + \NI{\varphi_{2}}) \cdot \\
 (\NI{\varphi_{1}} + \I{\varphi_{2}}) 
\end{array} $\\ 
\hline
\end{tabular}

\end{center}


\noindent $\NI{\varphi_k}$ is $\I{\neg \varphi_k}$. 
The distinction between $\I{\varphi_k}$ and $\NI{\varphi_k}$ is due to the {\em
polarity\/}   of the current subformula $\vk$.
During the computation of $\I{\varphi}$,  a call to the function $\I{\varphi_j}$
[$\NI{\varphi_j}$] is invoked  iff  $\varphi_j$ is a positive
[negative] subformula  of $\varphi$. 

%\input{figures/wff}
%\vspace{-.5cm}
\begin{figure}[t]
\vspace{-.5cm}
\begin{center}
\setlength{\unitlength}{0.0081in}%
\begin{picture}(624,312)(21,240)
\thicklines
\multiput( 69,346)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput( 69,346)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(159,346)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(159,346)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(249,347)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(249,347)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(340,349)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(340,349)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\put(288,411){\line( 1, 0){ 10}}
\put(288,408){\line( 1, 0){ 10}}
\put(298,408){\line( 0, 1){  0}}
\put(288,405){\line( 1, 0){ 10}}
\multiput(207,467)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(207,467)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(414,350)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(414,350)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(489,347)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(489,347)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(558,470)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(558,470)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(595,347)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(595,347)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\put(594,342){\circle{24}}
\put(594,329){\line( 0,-1){ 44}}
\put(588,332){\line(-1,-2){ 23.600}}
\put(602,332){\line( 1,-2){ 23.200}}
\put(570,357){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(559,265){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf E}}}
\put(581,266){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -C}}}
\put(621,266){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf F}}}
\put(581,253){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(549,253){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,-]}}}
\put(615,253){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,-]}}}
\multiput(382,473)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(382,473)(-0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\put( 69,342){\circle{24}}
\put(159,342){\circle{24}}
\put(249,342){\circle{24}}
\put(339,345){\circle{24}}
\put(114,405){\circle{24}}
\put(294,408){\circle{24}}
\put(207,462){\circle{24}}
\put(381,525){\circle{24}}
\put(558,465){\circle{24}}
\put(483,405){\circle{24}}
\put(414,345){\circle{24}}
\put(489,342){\circle{24}}
\put(615,405){\circle{24}}
\put(381,468){\circle{24}}
\put( 63,333){\line(-1,-2){ 25.200}}
\put( 69,330){\line( 0,-1){ 48}}
\put( 75,333){\line( 1,-2){ 25.800}}
\put(123,396){\line( 3,-4){ 30.960}}
\put(105,396){\line(-2,-3){ 30}}
\put(155,330){\line(-1,-3){ 14.600}}
\put(164,330){\line( 1,-4){ 11.353}}
\put(123,414){\line( 5, 3){ 73.088}}
\put(249,330){\makebox(0.6838,1.0256){\tenrm .}}
\put(249,329){\line( 0,-1){ 44}}
\put(287,398){\line(-3,-4){ 33.960}}
\put(336,334){\line(-1,-3){ 16.300}}
\put(343,333){\line( 1,-3){ 15.500}}
\put(243,332){\line(-1,-2){ 23.600}}
\put(301,399){\line( 2,-3){ 29.846}}
\put(257,332){\line( 1,-2){ 23.200}}
\put(412,333){\line(-1,-3){ 16.500}}
\put(417,333){\line( 1,-3){ 15.800}}
\put(219,457){\line( 5,-3){ 66.618}}
\put(474,398){\line(-6,-5){ 52.721}}
\put(484,393){\line( 1,-6){  6.270}}
\put(484,331){\line(-1,-2){ 23}}
\put(489,330){\line( 0,-1){ 44}}
\put(494,331){\line( 1,-2){ 23}}
\put(549,457){\line(-5,-4){ 55.610}}
\put(492,398){\line( 3,-4){ 40.200}}
\put(558,453){\line( 0,-1){ 44}}
\put(566,456){\line( 1,-1){ 41.500}}
\put(611,394){\line(-1,-3){ 13.400}}
\put(620,394){\line( 1,-2){ 24.200}}
\put(207,449){\line( 0,-1){ 50}}
\put(218,468){\line( 3, 1){152.700}}
\put(393,521){\line( 3,-1){154.200}}
\multiput(108,409)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(114,400)(0.50000,0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(376,528)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(382,519)(0.50000,0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(477,408)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(483,399)(0.50000,0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(609,407)(0.50000,-0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\multiput(615,398)(0.50000,0.75000){13}{\makebox(0.6838,1.0256){\sevrm .}}
\put(115,391){\line( 0,-1){ 47}}
\put(381,455){\line( 0,-1){ 44}}
\put(375,458){\line(-1,-2){ 23.600}}
\put(389,458){\line( 1,-2){ 23.200}}
\put(381,513){\line( 0,-1){ 33}}
\multiput( 75,435)(5.76923,0.00000){14}{\makebox(0.6838,1.0256){\tenrm .}}
\multiput(150,435)(2.64706,-5.29412){18}{\makebox(0.6838,1.0256){\tenrm .}}
\multiput(195,345)(0.00000,-5.83333){19}{\makebox(0.6838,1.0256){\tenrm .}}
\multiput(195,240)(-6.00000,0.00000){30}{\makebox(0.6838,1.0256){\tenrm .}}
\multiput( 21,240)(0.00000,5.83333){19}{\makebox(0.6838,1.0256){\tenrm .}}
\multiput( 21,345)(3.12976,5.21626){18}{\makebox(0.6838,1.0256){\tenrm .}}
\multiput( 72,435)(3.00000,0.00000){2}{\makebox(0.6838,1.0256){\tenrm .}}
\put(102,327){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -D}}}
\put(633,324){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -B}}}
\put( 57,246){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put( 24,246){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(522,312){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put( 90,246){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,-]}}}
\put(123,246){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(159,246){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(204,246){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1 , 0]}}}
\put(237,246){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,1]}}}
\put(264,246){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1 , 0]}}}
\put(309,246){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,1]}}}
\put(345,249){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,1]}}}
\put(378,249){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,-]}}}
\put(414,249){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put( 42,357){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [2,-]}}}
\put( 99,420){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [4,-]}}}
\put(195,480){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [7,-]}}}
\put(363,540){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [14,-]}}}
\put(282,423){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [2,-]}}}
\put(231,357){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [2,0]}}}
\put(468,420){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [2,-]}}}
\put(459,357){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [2,-]}}}
\put(543,480){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [2,-]}}}
\put(606,420){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(156,357){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [2,-]}}}
\put(192,387){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -C}}}
\put(192,375){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(102,315){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(554,390){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf A}}}
\put(549,378){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(630,309){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put( 27,264){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -A}}}
\put( 56,264){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -B}}}
\put( 97,264){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf C}}}
\put(126,263){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -E}}}
\put(164,262){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -F}}}
\put(206,263){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -D}}}
\put(245,264){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf A}}}
\put(267,263){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -E}}}
\put(313,266){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf C}}}
\put(354,267){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf F}}}
\put(389,264){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf D}}}
\put(418,266){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -A}}}
\put(448,266){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -F}}}
\put(486,268){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf D}}}
\put(507,267){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -B}}}
\put(448,250){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(475,252){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,-]}}}
\put(506,252){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(303,339){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,1]}}}
\put(375,342){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(368,379){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(336,379){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,-]}}}
\put(402,379){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [0,-]}}}
\put(348,480){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\egtrm [1,-]}}}
\put(368,392){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -E}}}
\put(408,392){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf B}}}
\put(525,324){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf -F}}}
\put(346,391){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\elvsf D}}}
\end{picture}
\caption{The computation tree of $\I{\vi}$.}
\label{wff_example}
\end{center}
\vspace{-.8cm}
\end{figure}


\begin{example}
\label{score_example}



Figure \ref{wff_example} represents the computation tree of the score
of a truth assignment $T$ for the 
formula $\varphi$ :

\footnotesize
%\input{figures/wff1}
\begin{center}
%\begin{tabular}{l}
$
(
 (
  (
   \neg  A
   \wedge
   \neg  B
   \wedge
   C
  )
  \vee
  \neg  D
  \vee
  (
   \neg  E
   \wedge
   \neg  F
  )
 )
 \wedge
 \neg  C
 \wedge
 (
  (
   \neg  D
   \wedge
   A
   \wedge
   \neg  E
  )
  \equiv
  (
   C
   \wedge
   F
  )
 )
)
\vee $ \\
$(
 D
 \wedge
 \neg  E
 \wedge
 B
)
\vee 
(
 (
  (
   D
   \wedge
   \neg  A
  )
  \vee
  (
   \neg F
   \wedge
   D
   \wedge
   \neg B
  )
  \vee
  \neg  F
 )
 \wedge
 A
 \wedge
 (
  (
   E
   \wedge
   \neg C
   \wedge
   F
  )
  \vee
  \neg  B
 )
).
$

%\end{tabular}
\end{center}

\normalsize




\noindent $T$ assigns ``true'' to all the variables of $\varphi$. 
The information in  square brackets  
 associated to any subformula $\varphi_j$ represents
[$\I{\varphi_j},\NI{\varphi_j}$]. 
For instance, if we consider the small subtree in the left of
Figure~\ref{wff_example}, then the score is computed in the following way:

\footnotesize
%\vspace{-.5cm}
\begin{center}
\begin{tabular}{ll} 
%& 
$\I{\ ( \neg  A \wedge
\neg  B \wedge  C ) \vee \neg  D 
\vee ( \neg  E \wedge \neg  F)\ } = $ \hspace{2.5cm}& 
\ \ \ \ ; $\I{\bigvee_k \varphi_{k}}= \prod_{k} \I{\varphi_{k}} $\\
%$=$ &
 $\I{ \neg  A \wedge \neg  B \wedge C} \cdot \I{\neg  D} \cdot
\I{\neg  E \wedge \neg  F}$  = &
\ \ \ \ ; $\I{\bigwedge_k \varphi_{k}}= \sum_{k} \I{\varphi_{k}} $\\
%$=$ &
 $(\I{\neg A} + \I{\neg B} + \I{C}) \cdot \I{\neg D} \cdot  (\I{\neg E}
+  \I{\neg F}) %\ldots
= $\hspace{-.3cm} & \ \ \ \ ; {\em literals} \\%$\I{\neg \vi} = \NI{\vi}$
%$=$ & $(\NI{ A} + \NI{ B} + \I{C}) \cdot \NI{D} \cdot (\NI{E} + \NI{F}) %\ldots
%= $ & \\
%$=$ &
 $(1 + 1 + 0) \cdot 1 \cdot (1 + 1) = 4.$ &%\hfill $\Box$
\\
\end{tabular}
\end{center}

\normalsize
\noi Notice that $cnf(\vi)$ is 360 clauses long.
\hfill $\Box$

\end{example}

\vspace{-.2cm}
\begin{theorem}
\label{works}
Let $\varphi$ be a propositional formula and $T$ a truth
assignment for the  variables of $\varphi$. Then the function
$\I{\varphi}$ gives the score of  $T$ for $\varphi$. 
\end{theorem}

\vspace{-.2cm}
\noindent The proof
%\footnote{The proofs of the theorems
%are quite easy and are therefore only hinted. 
%They are fully reported in \cite{sebastiani3}.}
 follows  from the consideration that, for any truth assignment
$T$, the set of the
false clauses of {\em cnf($\vi_1 \vee
\vi_2$)\/} is  the cross product between the two sets of the false clauses
of {\em cnf($\vi_1$)\/} and {\em
cnf($\vi_2$)\/}.


\vspace{-.1cm}
\begin{theorem}
Let $\varphi$ be a  propositional formula and $T$ a truth
assignment for the variables of $\varphi$. Then the
number of operations required for  
calculating $\I{\varphi}$ grows linearly with the size of $\vi$.   
\label{linearth}
\end{theorem}

\vspace{-.2cm}
\noi The proof follows  from the fact that, if $\PNti{\varphi_i}$ is the number 
of operations required for computing both 
$\I{\vi_i}$ and $\NI{\vi_i}$, and
if $\PNti{\varphi_i} \leq a_i
\cdot |\varphi_i| + b_i$, then $\PNti{\vi_1
\diamond \vi_2}
\leq  max_i(a_i)\cdot |\vi_1~\diamond~\vi_2|\ + 2 \cdot
max_i(b_i)\ + 6$, for any $\diamond \in \{\wedge,\vee,\supset,\equiv~\}$.

\gap\gap
The number of operations required  for computing the
score of an assignment $T$ for a clausal formula $\phi$ is $O(|\phi|)$. 
If $\phi = cnf(\vi)$, 
then $|\phi| = O(2^{|\vi|})$.
Thus the standard computation of the
score of $T$ for $\phi$  requires $O(2^{|\vi|})$ operations, while $\I{\vi}$
performs the same result directly in linear time. 



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% NC-GSAT                                                                 %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{GSAT for non-clausal formulas}


It follows from Sections \ref{gsat}, \ref{algorithm} that we can extend 
GSAT to non-clausal formulas $\vi$ by simply using the extended 
notion of score of Definition \ref{scoredef}.
Let NC-GSAT (non-clausal GSAT) be a new version 
of GSAT %for non-clausal formulas $\vi$
 in which the scores are computed
by some implementation of the function {\em s()\/}.
Then it follows from  Theorem \ref{works} that in
{\em NC-GSAT($\vi$)\/} the function {\em hill-climb()\/} always returns the 
same sets of variables
as  in {\em GSAT(cnf($\vi$))\/}, so that {\em NC-GSAT($\vi$)\/} 
performs the same flips and returns the same result as {\em GSAT(cnf($\vi$))\/}.
Theorem \ref{linearth} 
ensures that  every score computation is performed in 
linear time.  


The current implementation of GSAT \cite{selman2} 
provides a highly-optimized implementation of {\em Updatescores($\phi,V$)\/}, which
analyzes only the clauses   which the last-flipped variable $V$ 
occurs in. 
This allows a strong reduction in computational cost.
In \cite{sebastiani3} we describe in detail an analogous optimized version of the 
updating procedure for NC-GSAT, called {\em NC-Updatescores($\vi,V$)\/}, 
%which works recursively  on the tree structure of $\vi$.  We 
and
prove the following properties:

\vspace{-.2cm}
\begin{renumerate}
\item if $\vi$ is in clausal  form, i.e., $\vi  = cnf(\vi)$,  then
{\em NC-UpdateScores($\vi,V$)\/} has  the same complexity as
{\em UpdateScores($\vi,V$)\/};

\item  if $\phi  =  cnf(\vi)$,
then   {\em NC-UpdateScores($\vi,V$)\/} is $O(|\vi|)$.
{\em UpdateScores($\phi,V$)\/} is $O(2^{|\vi|})$.

\end{renumerate}
\vspace{-.1cm}
\noindent
The latter mirrors  the complexity issues 
presented in Section \ref{algorithm}. 

\newpage
The idea introduced in this paper can be applied to   
most % of the 
variants of GSAT. % proposed so far.   
In ``CSAT''
(Cautious SAT)  {\em hill-climb()\/} returns all
the variables which cause a decrease of the score; 
in ``DSAT''
(Deterministic SAT)  the function {\em pick()\/} performs a
deterministic choice; in ``RSAT'' (Random walk SAT) the variable is
picked randomly among {\em all} the
variables; in ``MSAT'' (Memory SAT) {\em pick()\/} remembers the last
flipped variable and avoids picking it.
All these variants, proposed in \cite{gent1,gent2}, can be  transposed into NC-GSAT as well, as they
are independent of the structure of the input formula.
\citeA{selman2} suggest some variants % to the original GSAT algorithm
which improve the performance and overcome some problems, 
such as that of escaping local minima.
%like, for instance, escaping local minima. 
The strategy ``{\em Averaging in\/}''   
suggests a different implementation of the function {\em initial()\/}:
instead of a random assignment, {\em initial()\/} returns a bitwise
average of the best assignments of the two latest cycles. This is
independent of the form of the input formula.
In the strategy ``{\em random walk\/}''  the sequence
{\em hill-climb() - 
pick()\/} is substituted with  probability $p$ by a simpler 
choice function: 
``choose randomly a variable occurring in some
unsatisfied clause''. This idea can be transposed into NC-GSAT as well: 
``choose randomly
a branch passing only for nodes whose score is different from zero, and
pick the variable at the leaf''.


One final observation is worth making. 
In order to overcome the exponential growth of CNF formulas, 
 some  algorithms have been 
proposed \cite{plaisted6,boy1} which convert propositional formulas $\vi$  into 
polynomial-size clausal formulas $\psi$. 
Such methods are  based on the  introduction of new  variables,   each
representing  a  subformula of  the original input \vim. 
Unfortunately, the issue of size-polynomiality is valid  only if no 
``$\equiv$'' occurs  in  $\vi$, as the number of clauses of $\psi$  grows
exponentially  with  the number of ``$\equiv$''  in \vim. 
Even worse, 
the introduction of $k$ new variables enlarges the
search space by a $2^k$ factor and reduces strongly the solution ratio.
In fact, any model  for $\psi$ is also a model for $\vi$,
but for any model of $\vi$ we only know that {\em one\/} of its $2^k$ extensions 
is a model of $\psi$ \cite{plaisted6}. 
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%  thanks
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\acks{Fausto Giunchiglia and Enrico Giunchiglia have given
substantial and continuous feedback during the whole development of
this paper. Toby Walsh provided important feedback about a previous
version of this paper. Aaron Noble, Paolo Pecchiari, and Luciano Serafini 
helped with the final revision.
%provided useful commments.
Bart Selman and  Henry Kautz  are   thanked
for assistance with  the GSAT code.}
	



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% bibliografia
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\bibliographystyle{theapa}
%\bibliography{a-l,m-z,myref}

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Artosi \BBA\ Governatori}{Artosi \BBA\
  Governatori}{1994}]{artosi1}
Artosi, A.\BBACOMMA\  \BBA\ Governatori, G. \BBOP1994\BBCP.
\newblock \BBOQ {L}abelled {M}odel {M}odal {L}ogic\BBCQ\
\newblock In {\Bem Proc. of {CADE12} {W}orkshop on {A}utomated {M}odel
  {B}uilding.}

\bibitem[\protect\BCAY{Ballantyne \BBA\ Bledsoe}{Ballantyne \BBA\
  Bledsoe}{1982}]{ballantyne1}
Ballantyne, M.\BBACOMMA\  \BBA\ Bledsoe, W. \BBOP1982\BBCP.
\newblock \BBOQ {O}n {G}enerating and {U}sing {E}xamples in {P}roof
  {D}iscovery\BBCQ\
\newblock In Michie, D.\BED, {\Bem Machines intelligence},
  \lowercase{\BVOL}~10, \BPGS\ 3--39. {H}alsted {P}ress.

\bibitem[\protect\BCAY{Davis \BBA\ Putnam}{Davis \BBA\ Putnam}{1960}]{davis2}
Davis, M.\BBACOMMA\  \BBA\ Putnam, H. \BBOP1960\BBCP.
\newblock \BBOQ A computing procedure for quantification theory\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 7}, 201--215.

\bibitem[\protect\BCAY{de~la Tour}{de~la Tour}{1990}]{boy1}
de~la Tour, T.~B. \BBOP1990\BBCP.
\newblock \BBOQ {M}inimizing the {N}umber of {C}lauses by {R}enaming\BBCQ\
\newblock In {\Bem Proc. of the 10th {C}onference on {A}utomated {D}eduction},
  \BPGS\ 558--572. Springer-Verlag.

\bibitem[\protect\BCAY{Gent \BBA\ Walsh}{Gent \BBA\ Walsh}{1992}]{gent1}
Gent, I.~P.\BBACOMMA\  \BBA\ Walsh, T. \BBOP1992\BBCP.
\newblock \BBOQ {T}he {E}nigma of {SAT} {H}ill-climbing {P}rocedures\BBCQ\
\newblock \BTR\ 605, University of Edinburgh, Dept. of Artificial Intelligence.

\bibitem[\protect\BCAY{Gent \BBA\ Walsh}{Gent \BBA\ Walsh}{1993}]{gent2}
Gent, I.~P.\BBACOMMA\  \BBA\ Walsh, T. \BBOP1993\BBCP.
\newblock \BBOQ {T}owards an {U}nderstanding of {H}ill-climbing {P}rocedures
  for {SAT}\BBCQ\
\newblock In {\Bem Proc. of the 11th National Conference on Artificial
  Intelligence}, \BPGS\ 28--33.

\bibitem[\protect\BCAY{Jeroslow}{Jeroslow}{1988}]{jeroslow2}
Jeroslow, R. \BBOP1988\BBCP.
\newblock \BBOQ {C}omputation-{O}riented {R}eduction of {P}redicate to
  {P}ropositional {L}ogic\BBCQ\
\newblock {\Bem Decision Support System}, {\Bem 4}, 183--197.

\bibitem[\protect\BCAY{Kautz \BBA\ Selman}{Kautz \BBA\ Selman}{1992}]{kautz2}
Kautz, H.\BBACOMMA\  \BBA\ Selman, B. \BBOP1992\BBCP.
\newblock \BBOQ {P}lanning as {S}atisfiability\BBCQ\
\newblock In {\Bem Proc. 10th European Conference on Artificial Intelligence},
  \BPGS\ 359--363.

\bibitem[\protect\BCAY{Klingerbeck}{Klingerbeck}{1994}]{klingerbeck1}
Klingerbeck, S. \BBOP1994\BBCP.
\newblock \BBOQ {G}enerating {F}inite {C}ounter {E}xamples with {S}emantic
  {T}ableaux and {I}nterpretation {R}evision\BBCQ\
\newblock In {\Bem Proc. of {CADE12} {W}orkshop on {A}utomated {M}odel
  {B}uilding.}

\bibitem[\protect\BCAY{Levesque}{Levesque}{1986}]{levesque3}
Levesque, H. \BBOP1986\BBCP.
\newblock \BBOQ Making believers out of computers\BBCQ\
\newblock {\Bem Artificial Intelligence.}, {\Bem 30}, 81--108.

\bibitem[\protect\BCAY{Plaisted \BBA\ Greenbaum}{Plaisted \BBA\
  Greenbaum}{1986}]{plaisted6}
Plaisted, D.\BBACOMMA\  \BBA\ Greenbaum, S. \BBOP1986\BBCP.
\newblock \BBOQ {A} {S}tructure-preserving {C}lause {F}orm {T}ranslation\BBCQ\
\newblock {\Bem Journal of Symbolic Computation}, {\Bem 2}, 293--304.

\bibitem[\protect\BCAY{Reiter \BBA\ Mackworth}{Reiter \BBA\
  Mackworth}{1989}]{reiter6}
Reiter, R.\BBACOMMA\  \BBA\ Mackworth, A. \BBOP1989\BBCP.
\newblock \BBOQ A logical framework for depiction and image
  interpretation\BBCQ\
\newblock {\Bem Artificial Intelligence.}, {\Bem 41\/}(2), 125--155.

\bibitem[\protect\BCAY{Sebastiani}{Sebastiani}{1994}]{sebastiani3}
Sebastiani, R. \BBOP1994\BBCP.
\newblock \BBOQ Applying {GSAT} to {Non-Clausal} {Formulas}\BBCQ\
\newblock \BTR\ 94-0018, DIST, University of Genova, Italy.
\newblock Available via anonimous ftp from mrg.dist.unige.it, /pub/mrg-ftp/.

\bibitem[\protect\BCAY{Selman \BBA\ Kautz}{Selman \BBA\ Kautz}{1993}]{selman2}
Selman, B.\BBACOMMA\  \BBA\ Kautz, H. \BBOP1993\BBCP.
\newblock \BBOQ {D}omain-{I}ndependent {E}xtension to {GSAT}: {S}olving {L}arge
  {S}tructured {S}atisfiability {P}roblems\BBCQ\
\newblock In {\Bem Proc. of the 13th International Joint Conference on
  Artificial Intelligence}, \BPGS\ 290--295.

\bibitem[\protect\BCAY{Selman, Levesque, \BBA\ Mitchell}{Selman
  et~al.}{1992}]{selman1}
Selman, B., Levesque, H., \BBA\ Mitchell, D. \BBOP1992\BBCP.
\newblock \BBOQ {A} {N}ew {M}ethod for {S}olving {H}ard {S}atisfiability
  {P}roblems\BBCQ\
\newblock In {\Bem Proc. of the 10th National Conference on Artificial
  Intelligence}, \BPGS\ 440--446.

\bibitem[\protect\BCAY{Slaney}{Slaney}{1993}]{slaney1}
Slaney, J. \BBOP1993\BBCP.
\newblock \BBOQ {SCOTT}: {A} {M}odel-{G}uided {T}heorem {P}rover\BBCQ\
\newblock In {\Bem Proc. of the 13th International Joint Conference on
  Artificial Intelligence}, \BPGS\ 109--114. Morgan Kaufmann.

\end{thebibliography}

\end{document}








