\documentclass[twoside,11pt]{article} 
\usepackage{jair}
\usepackage{theapa}
\usepackage{psfig}
\usepackage{graphicx}
\usepackage{latexsym}
\usepackage{rotate}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% END ROTATE PACKAGE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%\usepackage{dl}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% DL PACKAGE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
%% Style file for creating Grail/description logic documents

% Necessary Packages

\usepackage{xspace}
\usepackage{amssymb}
\usepackage{euscript}

% Hyphenation

\hyphenation{data-base tab-leaux tab-leau}

% Acronyms

\newcommand{\scname}[1]{\textsc{#1}}%   a (small) capitalised name
\newcommand{\calig}[1]{%                caligraphic text
        \ensuremath{\mathcal{#1}}}
\newcommand{\grail}{\scname{Grail}\xspace}%     GRAIL
\newcommand{\galen}{\scname{Galen}\xspace}%     GALEN
\newcommand{\alc}{%                             ALC
  \ensuremath{\mathcal{ALC}}\xspace}
\newcommand{\alcx}[1]{\calig{ALC#1}}%           ALCx
\newcommand{\alctrans}{%                        ALC_+
        \ensuremath{\alc_{+}}\xspace}
\newcommand{\alcRtrans}{%                       ALC_R+
        \ensuremath{\alc_{R^{+}}}\xspace}
\newcommand{\alcOtrans}{%                       ALC_o+
        \ensuremath{\alc_{\oplus}}\xspace}
\newcommand{\alcXtrans}[1]{%                    ALCx_+
        \ensuremath{\alcx{#1}_{+}}}
\newcommand{\alchrp}{%                          ALCH_R+
  \ensuremath{\mathcal{ALCH}_{R^{+}}}\xspace}
\newcommand{\alchfrp}{%                         ALCHf_R+
  \ensuremath{\mathcal{ALCH}\textbf{\textit{f}}_{R^{+}}}\xspace}
\newcommand{\Fact}{{\sc FaCT\xspace}}%                FaCT
\newcommand{\Classifier}{\FaCT}%
\newcommand{\Dlp}{{\sc DLP\xspace}}%                  DLP
\newcommand{\Racer}{{\sc RACER\xspace}}%              RACER
\newcommand{\Tsl}{\calig{TSL}\xspace}%          TSL
\newcommand{\Ciq}{\calig{CIQ}\xspace}%          QIC
\newcommand{\Back}{\scname{{\sc Back}\}xspace}}%       BACK
\newcommand{\Classic}{\scname{\sc Classic}\xspace}% CLASSIC
\newcommand{\Loom}{\scname{{\sc Loom}}\xspace}%       LOOM
\newcommand{\Kris}{\scname{{\sc Kris}}\xspace}%       KRIS
\newcommand{\Ksat}{\scname{{\sc Ksat}}\xspace}%       KSAT
\newcommand{\Ksatc}{\scname{{\sc KSatC}}\xspace}%       KSATC
\newcommand{\Crack}{\scname{{\sc Crack}}\xspace}%     CRACK
\newcommand{\Ssat}{\scname{{\sc *SAT}}\xspace}%     *SAT
\newcommand{\Ta}{\scname{{\sc TA}}\xspace}%     TA
\newcommand{\Mspass}{\scname{{\sc MSPASS}}\xspace}%     TA


\newcommand{\PDL}%                              PDL
        {PDL\xspace}
\newcommand{\CPDL}%                             converse-PDL
        {\emph{converse}-PDL\xspace}

% Semantics etc.

\newcommand{\I}{%                               I (caligraphic)
        \ensuremath{\mathcal{I}}\xspace}
\newcommand{\Tau}{%                             Tau
        \calig{T}\xspace}
\newcommand{\Tree}{%                            Tree
        \ensuremath{\mathbf{T}}\xspace}
\newcommand{\ifunc}{%                           ^I (caligraphic)
        \ensuremath{^\mathcal{I}}\xspace}
\newcommand{\deltai}{%                          Delta^I
        \ensuremath{\Delta\ifunc}\xspace}
\newcommand{\Exptime}{\textsc{Exptime}-complete\xspace}
\newcommand{\Pspace}{\textsc{Pspace}-complete\xspace}


% Algorithms
\newcommand{\Concepts}{\ensuremath{\mathbf{C}}\xspace}
\newcommand{\Roles}{\ensuremath{\mathbf{R}}\xspace}
\newcommand{\Rplus}{\ensuremath{\mathbf{R}_+}\xspace}
\newcommand{\Rfunc}{\ensuremath{\mathbf{F}}\xspace}
\newcommand{\Lab}{\ensuremath{\EuScript{L}}\xspace}
\newcommand{\Edges}{\ensuremath{\EuScript{E}}\xspace}


% Modal Logics

\newcommand{\K}%                                Modal K
        {\ensuremath{\mathbf{K}}\xspace}
\newcommand{\KT}%                               Modal KT
        {\ensuremath{\mathbf{KT}}\xspace}
\newcommand{\Kfour}%                            Modal K4
        {\ensuremath{\mathbf{K4}}\xspace}
\newcommand{\Sfour}%                            Modal S4
        {\ensuremath{\mathbf{S4}}\xspace}
\newcommand{\Km}%                               Modal Km
        {\ensuremath{\K_{(\mathbf{m})}}\xspace}
\newcommand{\KTm}%                              Modal KTm
        {\ensuremath{\KT_{(\mathbf{m})}}\xspace}
\newcommand{\Kfourm}%                           Modal K4m
        {\ensuremath{\mathbf{K4}_{(\mathbf{m})}}\xspace}
\newcommand{\Sfourm}%                           Modal S4m
        {\ensuremath{\mathbf{S4}_{(\mathbf{m})}}\xspace}


% Concept names etc.

\newcommand{\key}[1]{%                  a key word
        \ensuremath{\texttt{#1}}}
\newcommand{\con}[1]{%                  a concept
        \ensuremath{\textsf{#1}}}
\newcommand{\role}[1]{%                 a role
        \ensuremath{\textsf{\textsl{#1}}}}
\newcommand{\attr}[1]{%                 an attribute/feature/functional role
        \role{#1}}
\newcommand{\ind}[1]{%                  an individual
        \con{#1}}
\newcommand{\coneqn}[1]{%               a concept equation
        \con{#1}}
\newcommand{\cname}[1]{\con{#1}}%       a concept name e.g. human
\newcommand{\rname}[1]{\role{#1}}%      a role name
\newcommand{\aname}[1]{%                an attribute name
        \cname{#1}}


% DL syntax & notation

\newcommand{\Subs}{\ensuremath{\sqsupseteq}}
\newcommand{\Issub}{\ensuremath{\sqsubseteq}}
\newcommand{\nSubs}{\ensuremath{\not\sqsupseteq}}
\newcommand{\nIssub}{\ensuremath{\not\sqsubseteq}}

%\newcommand{\subs}[2]{%
%        \ensuremath{#1 \succeq #2}}
\newcommand{\some}[2]{%
        \ensuremath{\exists #1 . #2}}
\newcommand{\all}[2]{%
        \ensuremath{\forall #1 . #2}}
\newcommand{\atleast}[2]{%
        \ensuremath{\mbox{$\geqslant$}#1 #2}}
\newcommand{\atmost}[2]{%
        \ensuremath{\mbox{$\leqslant$}#1 #2}}
\newcommand{\atleastq}[3]{%
        \ensuremath{\mbox{$\geqslant$}#1 #2 . #3}}
\newcommand{\atmostq}[3]{%
        \ensuremath{\mbox{$\leqslant$}#1 #2 . #3}}
\newcommand{\ain}[2]{%
        \ensuremath{#1 . #2}}
\newcommand{\aeq}[2]{%
        \ensuremath{#1 = #2}}
\newcommand{\aneq}[2]{%
        \ensuremath{#1 \neq #2}}
\newcommand{\aeqd}[2]{%                                 attributes eq and defined
        \ensuremath{#1 \stackrel{\downarrow}{=} #2}}
\newcommand{\aneqd}[2]{%                                attributes neq and defined
        \ensuremath{#1 \stackrel{\downarrow}{\neq} #2}}
\newcommand{\domain}[1]{%                               domain of a function
        \ensuremath{\mathit{dom}~#1}}
\newcommand{\id}[1]{%                                   identity relation
        \ensuremath{\mathit{id}(#1)}}
\newcommand{\trans}[1]{%                                transitive role operator
        \ensuremath{#1^{+}}}
\newcommand{\transref}[1]{%                             transitive-reflexive role operator
        \ensuremath{#1^{*}}}
\newcommand{\restr}[2]{%                                role restriction
        \ensuremath{#1\!\mid_{#2}}}
\newcommand{\tuple}[2]{%                                binary tuple
        \ensuremath{\langle #1 , #2 \rangle}}
\newcommand{\constraint}[2]{%                           constraint x:C
        \ensuremath{#1\textrm{:}#2}}
\newcommand{\Card}[1]{%                                 set cardinality
        \ensuremath{\vert#1\vert}}
\newcommand{\Trole}{%                                   transitive role
        \ensuremath{^{(+)}}\xspace}


% non-LaTex composed symbols

\newcommand{\dotin}{%
        \ensuremath{\dot{\in}}}
\newcommand{\dotneq}{%
        \ensuremath{\dot{\neq}}}


% GRAIL syntax & notation

\newcommand{\gnewsub}[2]{%
        \ensuremath{#1\  \key{newSub}\  #2}}
\newcommand{\gcrit}[2]{%
        \ensuremath{#1\ #2}}
\newcommand{\gwhich}[2]{%
        \ensuremath{#1~\key{which}~#2}}
\newcommand{\gname}[2]{%
        \ensuremath{#1\  \key{name}\  #2}}
\newcommand{\gtnecc}[2]{%
        \ensuremath{#1\  \key{topicNecessarilly}\  #2}}
\newcommand{\gnewind}[2]{%
        \ensuremath{#1\  \key{newIndividual}\  #2}}
\newcommand{\greally}[2]{%
        \ensuremath{#1\  \key{really}\  #2}}


% Other stuff

\newcommand{\Eg}{\textrm{e.g.}\@\xspace}
\newcommand{\Ie}{\textrm{i.e.}\@\xspace}
 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% END DL PACKAGE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 




\jairheading{18}{2003}{351-389}{10/02}{5/03}
\ShortHeadings{A New General Method to Generate Random Modal Formulae}
{Patel-Schneider \& Sebastiani}
\firstpageno{351}



%% FIX
\newcommand{\todo}[1]{}
\newcommand{\new}[2]{}

\renewcommand{\rmdefault}{ptm}
\renewcommand{\sfdefault}{phv}
\renewcommand{\ttdefault}{pcr}

\newcommand{\tableau}[1]{{\sc Tableau}}
\newcommand{\ksat}{{\sc Ksat}}
\newcommand{\ksatw}{{\sc Ksat$_{W}$}}
\newcommand{\ksata}{{\sc Ksat$_{A}$}}
\newcommand{\ksatar}{{\sc Ksat$_{RA}$}}
\newcommand{\nvar}{N} 
\newcommand{\ncl}{L} 
\newcommand{\kris}{{\sc Kris}}
\newcommand{\ta}{{\sc TA}}
\newcommand{\lwb}{{\sc LWB}}
\newcommand{\flotter}{{\sc Flotter}}
\newcommand{\spass}{{\sc Spass}}
\newcommand{\bsat}{{\sc Dpll}}
\newcommand{\crack}{{\sc Crack}}
\newcommand{\ksatc}{{\sc KsatC}}
\newcommand{\ksatl}{{\sc KsatLisp}}
\newcommand{\ksatnl}{{\sc KsatLisp\-(unsorted)}}
\newcommand{\kcnf}{3CNF$_{\Box_{m}}$}
\newcommand{\kkcnf}{K-CNF$_{\Box_{m}}$}
\newcommand{\mcnf}{CNF$_{\Box_{m}}$}
\newcommand{\nkcnf}{New\_3CNF$_{\Box_{m}}$}
\newcommand{\ksatwl}{{\sc Ksat$_{W}$Lisp}}
\newcommand{\ksatal}{{\sc Ksat$_{A}$Lisp}}
\newcommand{\matom}[1]{\neg \Box (A_0 \vee \Box^{#1} \neg A_0)}
\newcommand{\nmatom}[1]{\Box (A_0 \vee \Box^{#1} \neg A_0)}
\newcommand{\mmatom}[1]{\neg A_0 \wedge \neg \Box^{#1} \neg A_0}
\newcommand{\nmmatom}[1]{(A_0 \vee \Box^{#1} \neg A_0)}
\newcommand{\ummatom}[1]{\neg \Box^{#1} \neg A_0}
\newcommand{\unmmatom}[1]{\Box^{#1} \neg A_0}
\def\i#1{\hbox{\it #1\/}}

\newcommand{\Sall}{${\scriptstyle >}$20}

\newcommand{\vi}{\varphi}

\newcommand{\KD}%                               Modal KD
        {\ensuremath{\mathbf{KD}}\xspace}
\newcommand{\Kfourfivem}%                               Modal K45m
        {\ensuremath{\K45_{(\mathbf{m})}}\xspace}
\newcommand{\KDfourfivem}%                            Modal KD45m
        {\ensuremath{\KD45_{(\mathbf{m})}}\xspace}
\newcommand{\Sfivem}%                           Modal S5m
        {\ensuremath{\mathbf{S5}_{(\mathbf{m})}}\xspace}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                   %
%%% 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}
\newplaintheorem{cexample}{Counter-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}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%                                                                   %
%%% \labelledequation allows to write an equation with a specified label %
%%%                                                                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newenvironment{labelledequation}[1]%
 {\begin{equation}\def\theequation{#1}}%
 {\end{equation} \addtocounter{equation}{-1}}%



\renewcommand{\topfraction}{1}
\renewcommand{\bottomfraction}{1}
\renewcommand{\textfraction}{0}
\setcounter{topnumber}{3}
\setcounter{totalnumber}{3}
\setcounter{bottomnumber}{3}

\newcommand{\TA}{\scname{TA}\xspace}%       TA


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% TITLE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}


\title{A New General Method to Generate Random Modal Formulae for Testing 
        Decision Procedures}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Authors
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\author{%
\name Peter F. Patel-Schneider \email pfps@research.bell-labs.com\\
\addr Bell Labs Research\\
600 Mountain Ave.
Murray Hill, NJ 07974, USA
\AND
\name Roberto Sebastiani \email rseba@dit.unitn.it\\
\addr Dip. di Informatica e Telecomunicazioni\\  Universit\`{a}
di Trento \\via Sommarive 14, I-38050,
 Trento, Italy
}

\maketitle


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% abstract
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{abstract} 
The recent emergence of heavily-optimized modal decision procedures
has highlighted the key role of empirical testing in this domain. 
Unfortunately, the introduction of extensive empirical tests 
for modal logics is  recent, 
and so far none of the proposed test generators is  very satisfactory.
To cope with this fact, we present a new random generation method that provides benefits
over previous methods for generating empirical tests.
It fixes and much generalizes 
one of the best-known methods, the random \mcnf{} test, 
allowing for  generating a
much wider variety of problems, covering 
in principle the whole input space.
Our new method produces much more suitable test sets for the current generation of
modal decision procedures.  
We analyze the features of the new method by means of an extensive
collection of empirical tests. 
\end{abstract}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Motivations for empirical testing
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Motivation and Goals}
\label{motivation_sec}  

Heavily-optimized systems for determining satisfiability of formulae in
propositional modal logics are now available. 
These systems, including \Dlp~\cite{patel-schneider:dlp-description},
\Fact~\cite{Horrocks98c},
%\Ksatc~\cite{giunchiglia108},
\Ssat~\cite{giunchiglia-sat2000},
\Mspass~\cite{Hustadt99-mspass},
and \Racer~\cite{haarslev1},
have more optimizations and are much faster than the previous generation of modal
decision procedures,
 such as 
 {\sc leanK}~\cite{Beckert97a},
 {\sc Logics Workbench}~\cite{Heuerding95a},
 $\Box${\sc KE}~\cite{Pitt96a}
 and \Ksat \cite{giunchiglia97}.%
\footnote{For a more complete list see Renate Schmidt's Web page listing
  theorem provers for modal logics at 
  {\sf http://www.cs.man.ac.uk/\/}\~{\sf schmidt/tools/}.} 

As with most theorem proving problems, neither computational complexity nor
asymptotic algorithmic complexity is  very useful in determining the effectiveness of
optimizations, 
so that their effectiveness has to be determined by
empirical testing  \cite{Horrocks-IGPL}.
Empirical testing directly gives resource consumption in terms
of compute time and memory use;  it factors in all the pieces of the
system, not just the basic algorithm itself.
Empirical testing can be used not only to compare different systems, but also
to tune a system with parameters that can be used to modify
its performance;  moreover, it can be used to show what sort of inputs the
system handles well, and what sort of inputs the system handles poorly.

Unfortunately, the introduction of extensive empirical tests 
for modal logics is  recent,
and so far none of the proposed test methodologies are very satisfactory.
Some methods contain many formulae that are too easy for current
heavily-optimized procedures.
Some contain high rates of trivial or insignificant tests.
Some generate problems that are too artificial and/or are not a
significant sample of the input space.
Finally, some methods generate formulae that are too big to be parsed and/or handled.


\smallskip

For the reasons described above, 
we presented \cite{Horrocks-IGPL} an analytical survey of the state-of-the art of empirical
testing for modal decision procedures. 
Here instead 
we present a new random generation method that provides benefits
over previous methods for generating empirical tests, 
built on some preliminary work \cite{Horrocks-IGPL}.
Our new method fixes and much generalizes the \kcnf{}  methodology
for randomly generating clausal formulae in modal logics
\cite{giunchiglia93,hustadt3,giunchiglia108} 
used in many previous empirical tests of modal decision procedures.
It eliminates or
 drastically reduces the influence of a major 
flaw of the previous method\new{1}{footnote added},%
\footnote{That is, a significant amount of inadvertently trivial  
  problems are generated unless the parameter p is set to 0
  \cite{Horrocks-IGPL}. 
See Section~\ref{p_subsec} for a full discussion of this point.} 
and allows for  generating a much wider variety of problems. 


In Section~\ref{features_sec} we recall
a list of desirable features for good test sets. 
In Section~\ref{past_testing_sec} we briefly survey
the state-of-the-art test methods.  
 In Sections~\ref{new_testing_sec} and \ref{new_testing2_sec} 
we present and discuss the basic and the advanced versions of our new test
method respectively, and evaluate their features by presenting a large
amount of empirical results.
In Section~\ref{generality_sec} we provide a theoretical result 
showing how the advanced version of our method, in principle, can cover
the whole input space.
In Section~\ref{discussion_sec} we discuss the features 
of our new method, and compare it wrt. the state-of-the-art
methods. 
In Section~\ref{conclusion_sec} we conclude and
 indicate possible future research directions.

A 5-page system description of our random generator has been
presented at IJCAR'2001~\cite{pfps-ijcar2001}.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Good and bad empirical test sets
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Desirable Features for Good Test Sets}
\label{features_sec}

The benefits of empirical testing depend on the characteristics of the
inputs provided for the testing, as empirical testing only provides data on
these particular inputs.
If the inputs are not typical or suitable, then the results of the
empirical testing will not be useful.
This means that the inputs for empirical testing must be carefully chosen.
With Horrocks \cite{Horrocks-IGPL} we have previously
proposed and motivated the following  key criteria 
for creating good test sets.

\begin{description}
\item[Representativeness:] 
The ideal  test set should represent a significant sample of the whole \new{1}{``significance'' substituted}
input space. 
A good empirical test set should at least cover a large area of inputs.  

\item[Difficulty:]
A good empirical test set should provide a sufficient level of difficulty
for the system(s) being tested. 
(Some problems should be too hard even for state-of-the-art systems,
so as to be a good benchmark for forthcoming systems.) 
% If the inputs are too easy, then the resulting resource consumption may be
% too small to easily measure, and the resource consumption may be dominated
% by start-up costs that do not grow as the difficulty of the inputs grow.
%This can result in favoring systems with small start-up costs but much
%worse growth in costs.

\item[Termination:]
To be of practical use, the tests should terminate and provide
information within a reasonable amount of time. 
If the inputs are too hard, then the system may not be able to provide
answers within the established time. 
 This inability of the system is of interest, but can make system comparison
 impossible or insignificant.


\item[Scalability:]
The difficulty of problems should scale up, as 
 comparing absolute performances
  may be less  significant than comparing how performances scale up with problems of increasing
   difficulty. 

\item[Valid vs.\ not-valid balance:] 
In a good test set, valid and not-valid 
problems should be more or less equal both in number and in difficulty. 
Moreover, 
% to prevent the usage of routines/heuristics which are explicitly aimed 
% at detecting either solvability or unsolvability, the testbed should provide 
% no {\em a priori\/} information which could help in guessing the result
% ---that is, 
the {\em maximum uncertainty\/} regarding the solution of the problems is desirable.
% (Notice that, in the real world, the solvability of a problem is not
%   known a priori.) 

\item[Reproducibility:] 
A good test set should allow for easily
  reproducing the results. 


\end{description}

\noindent
The following criteria derive from or are significant sub-cases of the main
criteria above. 

\begin{description}
\item[Parameterization:] 
Parameterized inputs with 
sufficient parameters and degrees of freedom allow the inputs to
range over a large portion of the input space. 
% On the other hand, the number of parameters and their degrees of freedom should not be too large, 
% otherwise the number of tests required to cover a significant subspace might blow up.
% (Ideally, the parameter set should work as much as possible as a ``base'' 
% for the input space.) 

\item[Control:]
In particular, it is very useful to have parameters that control 
{\em monotonically\/} the key features of the input test set, like the average
difficulty  and the ``valid vs.\ non-valid'' rate.  
% Monotonicity is a key point, as it allows for controlling one feature
% independently of the values of the other parameters, and for
% eliminating uninteresting areas of the input space. 

\item[Modal vs.\ propositional balance:]
Reasoning in modal logics involves alternating between two orthogonal
search efforts:
pure modal reasoning
%---that is, spanning the candidate Kripke models---
and pure propositional reasoning.
% ---that is, assigning truth values to 
% sub-formulae within each Kripke state. 
A good test set should be challenging from both viewpoints.
% of pure modal reasoning and pure propositional reasoning.

\item[Data organization:] The data should be summarizable ---so
  as to make a comparison possible with a limited effort--- and
  plottable ---so as to enable the qualitative behavior of the 
 system(s) to be highlighted.   
% For instance, a list of hundreds of uncorrelated numbers is
%   not a well-organised data set, since it makes a comparison
%   impractical, and makes it very hard to produce any qualitative
%   information from it. 

% \item[Focus on single problems:]
% As an alternative to wide-ranging tests, small ``ad hoc'' test sets may be
% used  for testing  systems on one particular 
% source of difficulty, or for revealing one particular possible  weakness. 
% For instance, formulae which are satisfied only by exponentially-large
% Kripke models (see, e.g.,  \cite{halpern4}) might 
% cause the system under test to blow up in space, thus revealing its
% non-PSPACEness. 

\end{description}

 
\noindent
Finally, particular care must be taken to avoid the
following problems. 

\begin{description}
\item[Redundancy:] 
Empirical test sets must be carefully chosen so as not to include inadvertent
redundancy.  
They should also be chosen so as not to include small
sub-inputs that dictate the result of the entire input.

\item[Triviality:]
A good test set should be flawless, that is, it  should not contain \new{1,3}{added ``inadvertent''}
significant subsets of 
inadvertent trivial problems. 

\item[Artificiality:] 
A good empirical test set should correspond closely to inputs from
applications.  
% If the test set does not resemble actual inputs, then the
% results from the empirical testing will not necessarily correspond with the
% behaviour of the system in real use. 


\item[Over-size:] 
  The single problems should not be too big w.r.t. their difficulty, so
  that the resources required for parsing and data managing do not seriously influence total performance.
\end{description}

\noindent
These criteria, which are described and motivated in detail by
\citeauthor{Horrocks-IGPL}~\citeyear{Horrocks-IGPL}, have been proposed
after  a five-year debate  
on empirical testing in modal logics 
\cite{giunchiglia93,heuerding2,hustadt3,giunchiglia108,Horrocks99f}. 
(Notice that some of these criteria are identical or similar to those
suggested by \citeR{heuerding2}.)
%\citeauthor{heuerding2}~\citeyear{heuerding2}.)
 
The above criteria are general, and in some cases 
they require some interpretation. 
First, some of them have to be implicitly interpreted as
``unless the user deliberately wants the contrary for some reason''.
For instance, 
it might be the case that one wants to {\em deliberately}
generate  {easy} problems, e.g., to
be sure that the tested procedure does not take too much time to solve
them,
or {redundant} problems, e.g., to test the effectiveness of some redundancy
elimination technique,
or  satisfiable problems only, e.g., 
to test incomplete procedures.
To this extent, the key issue here is having a reasonable form of
control over these features, so that one can address not only 
general-purpose criteria, but also specific desiderata.

Second, in some cases, there may be a tradeoff
between two distinct criteria, so that it may be necessary to choose
only one of them, or to make a 
compromise.
One example is given by 
redundancy and artificiality: 
 in some  real-world problems large parts of the knowledge base are 
 irrelevant
for the query, whose result  is determined by a small
 subpart of the input; in this sense eliminating such ``redundancies''  
may make problems more ``artificial''. 

 
\medskip
Particular attention must be paid to 
the problem of  triviality, as it has claimed victims in 
many areas of AI. In fact,  flaws (i.e., inadvertent trivial
problems) have been detected in random generators for  SAT
\cite{mitchell1}, CSP  \cite{achlioptas1,gent4}, modal
reasoning~\cite{hustadt3}  and QBF \cite{gent3}. 
Thus, the notion of ``trivial'' (and thus ``flawed'') deserves more 
comment.

In the work by \citeauthor{achlioptas1}~\citeyear{achlioptas1} flawed
problems are those  solvable in 
linear time by standard  CSP procedures, due 
to the undesired
presence of implicit unary constraints causing some variable's value 
to be inadmissible. A similar notion  holds for 
SAT \cite{mitchell1} and 
QBF \cite{gent3}. 
In the literature of modal reasoning, instead, 
the typical flawed problems are those whose (un)satisfiability can be
 verified directly at propositional level, that is, without
investigating any modal successors;
this kind of problems are typically solved in negligible time w.r.t. 
other problems of similar size and depth
\cite{hustadt3,giunchiglia108,Horrocks-IGPL}.%
\footnote{Of course here by ``modal'' we implicitly  assume the modal
  depth be strictly greater than zero, that is, we
do not consider purely  propositional formulas.
}
Thus, with a little abuse of notation and when not otherwise
specified, in this paper we will call {\em trivially (un)satisfiable}
the problems of this kind.%
\footnote{%
Notice that we do not use the more suitable expression  ``propositionally
   (un)satisfiable''  because the latter has been used with a
   different meaning in the literature of modal reasoning (see, e.g.,
   \citeR{giunchiglia93,giunchiglia97}).  
 } 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Past Empirical Testing
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% An analysis of the main  test methods
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{An Overview of the State-of-the-art}
\label{past_testing_sec}

Previous empirical tests have mostly been generated by three methods:
hand-generated formulae \cite{heuerding2},
randomly-generated clausal modal formulae
\cite{giunchiglia93,hustadt3,giunchiglia108},
and randomly-generated quantified boolean formulae that are then translated
into modal formulae \cite{massacci_TANCS99}.

We have already presented a detailed analysis of these three methods 
\cite{Horrocks-IGPL}. 
% The first method \cite{heuerding2} is obsolete,
% as the formulae generated are trivial for current state-of-the-art
% deciders.
Here we present only a quick overview of the 
latter two methods, as we will refer to them in following sections.% 
\footnote{The first method \cite{heuerding2} is obsolete,
 as the formulae generated are too easy for current state-of-the-art
 deciders \cite{Horrocks-IGPL}.}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% The \kcnf{} Random Tests
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{The \kcnf{} Random Tests}
\label{old_kcnf_met_sec}

In the \kcnf{} test methodology
\cite{giunchiglia93,hustadt3,giunchiglia108}, the performance of a
system is 
evaluated on sets of randomly generated \kcnf{} formulae. 
A \mcnf{} formula is a conjunction of \mcnf{} clauses, where
each clause is a disjunction of either propositional
or modal literals. A literal is either an atom or its negation. 
Modal atoms are formulae of the form $\Box_i C$, where $C$ is a
\mcnf{} clause. 
A \kcnf{} formula is a \mcnf{} formula where 
all clauses have exactly 3 literals. 

\subsubsection{The Random Generator}\new{2}{generator and method decoupled}

A \kcnf{} formula is randomly generated according to five 
parameters: 
the (maximum) modal depth $d$; 
  the number of clauses in the top-level conjunction $\ncl$;  
  the number of propositional variables $\nvar$;
 the number of distinct box symbols $m$;
and   the probability $p$ of an atom occurring in a clause 
at depth $< d$ being purely propositional. 

The random \kcnf{} generator, in its final version
\new{1}{paragraph added}
\cite{giunchiglia108}, works as follows:
\begin{itemize}
\item 
a \kcnf{} formula of  depth $d$ is produced by 
randomly generating $L$   \kcnf{}  clauses of depth $d$, and forming their
conjunction; 
\item 
a \kcnf{}   clause of  depth $d$ is produced by 
randomly generating three distinct, under commutativity of disjunction,
\kcnf{} atoms of depth $d$,  
negating each of them with probability 0.5,
and forming their
disjunction; 
\item 
a propositional atom is produced by picking randomly an element of
$\{A_1,\ldots,A_N\}$ with uniform probability;
\item
a \kcnf{}  atom of depth $d>0$ is produced by generating  with probability $p$
a random propositional atom, 
and with probability $1-p$ a \kcnf{} atom $\Box_r C$,
where $\Box_r$ is picked randomly in $\{\Box_1,\ldots,\Box_m\}$ and 
$C$ is a randomly generated  \kcnf{} clause of depth $d-1$.
\end{itemize}

Recently \citeauthor{Horrocks99f}~\citeyear{Horrocks99f} have proposed a variant of
\new{1}{paragraph added} 
the \kcnf{} random generator of
\citeauthor{giunchiglia108}~\citeyear{giunchiglia108}.  
They added four extra parameters: $n_p$ and $n_m$, representing
respectively the
probability that a propositional and modal atom is negated, 
and $c_{min}$ and $c_{max}$, representing respectively  the minimum and maximum number
of modal literals in a clause, with equal probability for each number
in the range. 
For their experiments, they always set $n_p=0.5$ and $c_{min}=c_{max}=3$.
To this extent,  \kcnf{} formulas
can be generated as in the generator of
\citeauthor{giunchiglia108}~\citeyear{giunchiglia108}  
by setting $n_p=n_m=0.5$ and $c_{min}=c_{max}=3$.


\subsubsection{Test  Method \& Data Analysis}


The \kcnf{} test method works as follows. 
A typical problem set is characterized by a fixed $\nvar$, $m$, 
$d$ and $p$: $\ncl$ is varied in such a way as to empirically cover the 
``100\% satisfiable---100\% unsatisfiable'' transition. 
Then, for each tuple of the parameters' values ({\em data point\/} from now
on) in a problem set, 
a certain number of \kcnf{}  formulae are randomly generated, and the resulting
formulae are given in input to the procedure under test, 
with a maximum time bound.
Satisfiability rates, median/percentile values of the CPU
times, and median/percentile values of other parameters, e.g., number of
steps, memory, etc., are plotted 
against the number of clauses $\ncl$
or the ratio of clauses to propositional variables $\ncl/\nvar$.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% The Random QBF Tests
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{The Random QBF Tests}

In QBF-based benchmarks (such as part of the TANCS'99 benchmarks
\cite{massacci_TANCS99}), 
system performances are evaluated on sets of
random quantified boolean formulae, which are generated according to the method 
described by
\citeauthor{cadoli2}~\citeyear{cadoli2} and
\citeauthor{gent3}~\citeyear{gent3} and then 
converted into modal logic  
by using a variant of the conversion by
\citeauthor{halpern4}~\citeyear{halpern4}. 

\subsubsection{The Random Generator}\new{2}{generator and method decoupled}


Random QBF formulae are generated 
with  alternation depth $D$ and at most $V$ variables at
each alternation. The matrix is a random propositional CNF formula with
$C$ clauses of length $K$, 
with some constraints on the number of  universally and existentially
quantified variables within each clause. 
(This avoids the problem of generating flawed  random QBF 
formulae highlighted by \citeR{gent3}.)
%\citeauthor{gent3}~\citeyear{gent3}.)
%
For instance, a random QBF formula with $D=3$, $V=2$ looks like:
\begin{equation}
  \label{qbf_wff_equ}
  \forall v_{32}v_{31}.\exists v_{22}v_{21}. \forall v_{12}v_{11}.\exists v_{02}v_{01}. \psi[v_{32},...,v_{01}].
\end{equation}
\noindent
Here
$\psi$ is a random CNF formula with parameters $C$, $V$ and $D$.
We will denote with $U$ and $E$ the total number of universally and
existentially quantified variables respectively.
Clearly, both $U$ and $E$ are $O(D\cdot V)$.
Moreover, $\vi$ is the  modal formula resulting from
\citeauthor{halpern4}' \K{} conversion, 
so both the depth $d$ and the  number of propositional
variables $N$ of $\vi$ are also $O(D\cdot V)$. 

\subsubsection{Test  Method \& Data Analysis}

The test method, as it was used in the TANCS competition(s)
\cite{massacci_TANCS99}, 
works as follows.
The tests are performed on single data points.
For each data point, \new{1}{modified} 
a certain number of QBF  formulae are randomly generated, converted
into modal logics and the resulting
formulae are given as input to the procedure being tested, 
with a maximum time bound.
The number of tests which have been solved within the
time-limit and the geometrical mean time for successful solutions
are then reported.
% For each data point,
% it is produced the number of tests which have been solved within the
% timeout and the geometrical mean time for successful solutions.
Data are rescaled to abstract away machine and run-dependent 
characteristics. 
This results typically in a collection of 
tables presenting a data pair for each system under test, one 
data point per row. 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% New Empirical Testing
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% A new method
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{A New \mcnf{} Generation Method: Basic Version}
\label{new_testing_sec}

From our previous analysis \cite{Horrocks-IGPL} we have that none of the
current methods are 
completely satisfactory. 
To cope with this fact, we propose here what we believe is 
a much more satisfactory method for randomly generating 
modal formulae. The new method can be seen as an improved and much
more general version of the random \kcnf{} generation method by
\citeauthor{giunchiglia108}~\citeyear{giunchiglia108}. 

We present our new method 
by introducing incrementally its new features in two main steps.
In this section we introduce a {\em basic version} of the method, wherein
\begin{itemize}
\item  we provide a new interpretation for the parameter $p$
  (Section~\ref{p_subsec}) that allows
  for varying $p$ without causing the flaws
  described in \citeauthor{Horrocks-IGPL}~\citeyear{Horrocks-IGPL}; and
\item we extend the interpretation for the parameter $C$
  (Section~\ref{c_subsec}), providing a more fine-grained  way
  for tuning the difficulty of the generated formulae.
\end{itemize}
\noindent
In Section~\ref{new_testing2_sec}, we present the full, {\em advanced
  version} of the method, wherein
\begin{itemize}
\item we further extend the parameters $p$ and
  $C$, allowing for shaping explicitly the
  probability distribution of the propositional/modal rate and the
  clause length respectively  (Section~\ref{shape_subsec}); and
\item we allow $p$ and $C$ vary with the nesting depth
 of the subformulae (Section~\ref{vary_depth_subsec}), 
 allowing for different distributions at different depths. 
\end{itemize}
To investigate the properties of our \mcnf{} generator we also present a
series of 
experiments  with appropriate settings
either to mimic previous generation methodologies or to produce improved or
new kinds of tests.  


\smallskip 

In all tests  we have adopted the testing criteria of the \kcnf{} method. 
For each test set, we fixed all parameters except $L$, which was varied to
span at least the satisfiability transition area. 
(Because of the ``Valid vs. non-valid balance'' feature 
of Section~\ref{features_sec}, we consider the transition area to be the 
interesting portion of the test set.)
For almost all test sets we varied $L$ from $N$ to $120N$, $150N$, or $200N$,
resulting in integral values for $L/N$ ranging from $1$ to $120$, $150$, or $200$.
For each value of $L$ we generated
100 formulae, a sufficient number to produce reasonably reliable data.
A time limit of 1000 seconds was imposed on each attempt to determine the
satisfiability status of a formula.  
As it is common practice, we set the number of boxes $m$ to
$1$ throughout our testing. 
This setting for $m$ produces the hardest formulae
\cite{giunchiglia93,hustadt3,giunchiglia108}.
We performed several test sets with similar parameters, often, but not
always, varying only $N$.

We tested our formulae against two systems,
\Dlp{} version 4.1 \cite{patel-schneider:dlp-description}
and
\Ssat{} version 1.3 \cite{Tacchella99a}, two of the fastest
modal decision procedures. 
They %can be downloaded at
are available at %under
{\sf http://www.bell-labs.com/usr/pfps/dlp}
and
{\sf http://www.mrg.dist.unige.it/\/}\~{\sf tac\/} respectively.
All the code used to
generate the tests 
%can be downloaded at
is available at %under 
{\sf
http://www.bell-labs.com/usr/pfps/dlp}. 

We plotted the results of our test groups (test sets with similar
parameters) on six or four plots.
Two plots were devoted to the performance of \Dlp{}, one showing
the median and one showing the 90th percentile time taken to
solve the formulae at each value of $L$, plotted against $L/N$.
For those test groups were we ran \Ssat{} we also plotted the median and
90th percentile for \Ssat{}.

We also plotted the fraction of the formulae that are determined to be
satisfiable or unsatisfiable by \Dlp{} within the time
\new{1}{footnote added} limit.%
\footnote{%
Notice that the two curves are symmetric with respect to 0.5 if and only if no test
exceeds the time limit.
E.g., if at some point
40\% of the tests are determined  to be
satisfiable by \Dlp{}, 10\% are determined  to be
unsatisfiable and 50\% are not solved within the time limit, 
then the two curves are not symmetric at that point, as $0.40\neq 1-0.10$. 
\label{symmetry_footnote}
}  
To save space, satisfiability and unsatisfiability fractions are 
plotted together on a single plot.  Satisfiability fractions are higher on
the left side of the plot while unsatisfiability fractions are higher on
the right.
This multiple plotting does obscure some of the details, but the
only information that we are interested in here is the general behavior of
the fractions, which is not obscured.  In fact, the multiple plotting
serves to highlight the crossover regions, where the satisfiability and
unsatisfiability fractions are roughly equal.

Finally, we plotted the fraction of the formulae where \Dlp{} finds a model or
determines that the formula is unsatisfiable without
investigating any modal successors.  We call these fractions the trivial
satisfiability and trivial unsatisfiability fractions.
\new{1}{examples added}
These last fractions are an estimate of
the number of formulae that are satisfiable in a Kripke structure with no
successors ---like, e.g., $(A_1\vee\Box_1A_2)$--- and that have no
propositional valuations
---like, e.g., $(\Box_1 A_1 \wedge \neg \Box_1 A_1)$--- respectively.
For various reasons, discussed below, they are better indicators
of triviality than the more formal measures used in previous papers.
Again, trivial satisfiability and unsatisfiability fractions are 
plotted together on a single plot.

To reduce clutter on the plots, we used a line to show the results for
each value of $L$ we tested.  To distinguish between the various lines on a
plot, we plotted every five or 10 data points with a symbol, identified in
the legend of the plot. 

Running the tests presented in this paper required some months 
of CPU time. 
Because of this, we ran our tests on a variety of machines.  
These machines range in speed 
from a 296MHz SPARC Ultra 2 
to a 400MHz SPARC Ultra 4 
and had between 256MB and 512MB of main memory.  
No machines were completely dedicated to our tests,
but they were otherwise lightly loaded.
Each test set was run on
machines with the same speed and memory. 
Direct comparison between different groups of tests thus has to take into
account the differences between the various test machines.

\subsection{Reinterpreting the Parameter $p$}
\label{p_subsec}

%\todo{SHORTEN?}
One problem with the previous methods for generating \mcnf{} formulae is
that the generated formulae can contain pieces that make the entire formula
easy to solve.  This mostly results from the presence of
strictly-propositional top-level clauses.  With the small number of
propositional variables in most tests (required to produce reasonable
difficulty levels for current systems), only a few strictly-propositional
top-level clauses are 
needed to cover all the combinations of the propositional literals and make
the entire formula unsatisfiable.  
\new{1}{references added} Previous attempts to eliminate this
``trivial unsatisfiability'' have concentrated on eliminating
top-level propositional literals by setting $p=0$ \cite{hustadt3,giunchiglia108}. 
(Unfortunately this choice  forces 
 $d\le 1$, as for $d>1$ such formulae are too hard 
for all state-of-the-art systems.)
%
When each atom in a
clause is generated independently 
from the other atoms of the clause an
approach that modifies the probability of propositional atoms is
necessary to eliminate these problematic clauses.

The first new idea of our approach, suggested previously 
\cite{Horrocks-IGPL}, works as follows. 
Instead of forbidding strictly-propositional clauses except at the maximum
modal depth, $d$, by setting $p=0$, we instead require that the ratio
between propositional atoms in a clause and the clause size be as close as
possible to the propositional probability $p$
for clauses not at the maximum modal depth $d$.%
\new{2}{footnote: sentence added}
\footnote{Other approaches
to eliminating propositional unsatisfiability are possible.  For example,
it would be possible to simply remove any strictly-propositional clauses
after generation.  However, this technique would alter 
the meaning of the parameter $p$, that is,  
the actual  probability for a literal to be propositional
would become  strictly smaller than $p$, 
and it will be out of the control of the user.
} 

For clauses of size $C$, if $p$ is $k/C$ for some integral $k$, this
results in all clauses not at modal depth $d$ having $k$ propositional atoms and
$C-k$ modal atoms. 
For other values of $p$, we allow either $\lfloor pC \rfloor$ 
or $\lceil pC \rceil$ propositional atoms in each clause not at modal depth
$d$, with probability $\lceil pC \rceil - pC$ and 
$pC - \lfloor pC \rfloor$, respectively.\footnote{Remember that 
$\lfloor{x}\rfloor{} =_{def} max \{n\in{\cal N}|n\le X\}$ 
and 
$\lceil{x}\rceil{} =_{def} min \{n\in{\cal N}|n\ge X\}$.}
%
For instance, if $p=0.6$ and $C=3$, then each clause contains 1 propositional and
1 modal literal, and 
the third is propositional with probability 0.8, 
as $3 \cdot 0.6-\lfloor{3 \cdot 0.6}\rfloor{} =1.8-1=0.8$.
%
If $p \leq (C-1)/C$, this eliminates the possibility of strictly
propositional clauses, which are the main cause of trivial unsatisfiability,
except at modal depth $d$. 



\subsubsection{Modal Depth $1$}
Our first experiments were a direct comparison to previous tests.  We
generated \mcnf{} formulae with $C=3$, $m=1$, $d=1$, and 
$p=0.5$, a setting that has been used in the past, and one that
exhibits some problematic behavior. 
We used both our new method and the old \kcnf{} generation method 
by \citeauthor{giunchiglia108}~\citeyear{giunchiglia108} briefly described in
Section~\ref{old_kcnf_met_sec} \new{1}{sentence added}
(the ``old method'' from now on). 
We also generated \mcnf{} formulae with $C=3$, $m=1$, $d=1$, and $p=0$, the
standard method for eliminating trivially unsatisfiable formulae.  
(At $p=0$ our new method is the same as the old \kcnf{} generation method.)
The results of the tests are given in Figures 
\ref{results-d1-old}, \ref{results-d1-new}, and \ref{results-d1-p0}.


\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p1,3,3,1-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p1,3,3,1-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p1,3,3,1-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p1,3,3,1-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d1p1,3,3,1-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d1p1,3,3,1-90.ps}
\end{tabular}
\caption{Results for $C=3$, $m=1$, $d=1$, and $p=0.5$ (old method)}
\label{results-d1-old}
\end{figure}

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p0,3,3,0-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p0,3,3,0-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p0,3,3,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p0,3,3,0-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d1p0,3,3,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d1p0,3,3,0-90.ps}
\end{tabular}
\caption{Results for $C=3$, $m=1$, $d=1$, and $p=0.5$ (our new method)}
\label{results-d1-new}
\end{figure}

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p1,0,0,0-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p1,0,0,0-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p1,0,0,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd1p1,0,0,0-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d1p1,0,0,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d1p1,0,0,0-90.ps}
\end{tabular}
\caption{Results for $C=3$, $m=1$, $d=1$, and $p=0$ (either method).\label{results-d1-p0}}

\end{figure}

\medskip


One aspect of this set of tests is that 
all three collections have many trivially unsatisfiable
formulae out of the satisfiability transition area,
even the collection with no top-level propositional atoms.
The trivial unsatisfiability occurs in the collection with no top-level
propositional atoms because there are only a few top-level modal atoms 
(e.g., $8$ for $\nvar=3$) and both \Dlp{} and \Ssat{} detect clashes between complementary modal
literals without investigating any modal successors.

The presence of this large number of trivially unsatisfiable formulae is
not actually a serious problem with {\em these} tests.
The trivial unsatisfiability only shows up after the formulae are almost
all unsatisfiable already and easy to solve.
The only exception is for $\nvar=3$, which is trivial to solve anyway.
However, our new generation method considerably reduces the number of
trivially unsatisfiable formulae and almost %{ONLY ALMOST???}
entirely removes them from the
satisfiable/unsatisfiable transition area.
There are some trivially satisfiable formulae in this set of tests, but
only a few, and only for the smallest clause sizes.   Their presence does
not affect the difficulty of the generated formulae.

The two methods with $p=0.5$ are relatively close in maximum
difficulty, with our new method
generating somewhat harder formulae.
However, our method produces difficult formulae, for both \Dlp and
\Ssat, over a much broader range of $L/\nvar$ than does the original method.

Changing to $p=0$ results in formulae that are orders of magnitude harder.
This is not good, previous arguments to the contrary notwithstanding, as we
would like to have a significant number of 
reasonable test sets to work with, and $p=0$ allows only consideration of a
very few values for $\nvar$ before the formulae are totally impossible to solve
with current systems, resulting in very few reasonable test sets.

So, at a maximum modal depth of $d=1$ our method results in formulae that are
of similar difficulty to the previously-generated formulae and still have
 trivially unsatisfiable formulae, but ones that do not seriously affect the
difficulty of the test sets. 

\subsubsection{Modal Depth $2$}

Restricting attention to a maximum modal depth of $d=1$ is not very
useful.
Formulae with maximum modal depth of $1$ are not representative of modal
formulae in general, particularly as they have no nested modal operators.
Sticking to a maximum modal depth of $1$ seriously limits the
significance of the generated tests.   

We would thus like to be able to perform interesting experiments
with larger maximum modal depths.
So we performed a set of experiments with a maximum modal depth of $d=2$.
We started with a set of tests that corresponds to previously-performed experiments.

At depth $d=2$, in the old method for $p=0.5$ the time
curves are dominated by a ``half-dome'' shape, whose steep side shows up
where the number of trivially unsatisfiable formulae becomes large
before the formulae become otherwise easy to solve, as shown in
Figure~\ref{results-d2-old}. 
In fact, nearly all the unsatisfiable formulae here are trivially
unsatisfiable.

This is an extremely serious flaw, as the difficulty of the test set is
being drastically 
affected by these %very-easy-to-solve 
trivially unsatisfiable formulae.
Changing to $p=0$ is not a viable solution because at depth $d=2$ such
formulae are much too difficult to solve,
as shown in Figure~\ref{results-d2-p0},
where the median percentile exceeds the timeout before any formulae can be determined
to be unsatisfiable, even for 3 propositional variables.

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p1,3,3,1-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p1,3,3,1-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p1,3,3,1-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p1,3,3,1-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p1,3,3,1-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p1,3,3,1-90.ps}
\end{tabular}
\caption{Results for $C=3$, $m=1$, $d=2$, and $p=0.5$ (old method)}
\label{results-d2-old}
\end{figure}

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p1,0,0,0-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p1,0,0,0-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p1,0,0,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p1,0,0,0-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p1,0,0,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p1,0,0,0-90.ps}
\end{tabular}
\caption{Results for $C=3$, $m=1$, $d=2$, and $p=0$ (either method)}
\label{results-d2-p0}
\end{figure}

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p0,3,3,0-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p0,3,3,0-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p0,3,3,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p0,3,3,0-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p0,3,3,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p0,3,3,0-90.ps}
\end{tabular}
\caption{Results for $C=3$, $m=1$, $d=2$, and $p=0.5$ (our new method)}
\label{results-d2-new}
\end{figure}


With our new method, as shown in Figure~\ref{results-d2-new}, the formulae
are much more difficult to solve than the 
old method, because there is no abrupt drop-off from propositional
unsatisfiability, but they are much easier to solve than those generated
with $p=0$.
Further,  trivially unsatisfiable formulae do not appear at all in the 
interesting portion of the test sets.

% Nevertheless our method is not entirely suitable at modal depth
% $d=2$ with propositional probability $p=0.5$.  
Nevertheless this choice of parameters ($d=2$, $p=0.5$)
is not entirely suitable.  
The formulae are becoming
too hard much too early. %, similar to the situation for $d=1$ and $p=0$. 
In particular,
there are no unsatisfiable formulae that can be solved for $\nvar>3$,
\new{1}{sentence added} and thus the unsatisfiability plots cannot be distinguished 
from the x axis (recall Footnote~\ref{symmetry_footnote}).   
However, our new method does provide some advantages already, providing an
interesting new set of tests, albeit one of limited size.


\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p8,36,54,27-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p8,36,54,27-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p8,36,54,27-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p8,36,54,27-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p8,36,54,27-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p8,36,54,27-90.ps}
\end{tabular}
\caption{Results for $C=3$, $m=1$, $d=2$, and $p=0.6$ (old method)}
\label{results-d1-mp06-old}
\end{figure}

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p0,1,4,0-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p0,1,4,0-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p0,1,4,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2p0,1,4,0-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p0,1,4,0-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2p0,1,4,0-90.ps}
\end{tabular}
\caption{Results for $C=3$, $m=1$, $d=2$, and $p=0.6$ (our new method)}
\label{results-d1-mp06-new}
\end{figure}


\subsection{Increasing $p$}



We would like to be able to produce better test sets for depth $d=2$ and greater.
One way of doing this is to increase the propositional probability $p$ from
$0.5$ to something like $0.6$, increasing the 
number of propositional atoms and thus decreasing the difficulty of the
generated formulae.  This would be very problematic with previous
generation methods as it would result in the trivially unsatisfiable
formulae determining the results for even smaller numbers of clauses
$\ncl$, but with our method here it is not much of a problem.


To investigate the increasing of the the propositional probability,
we ran a collection of tests with maximum modal depth $d=2$ and
propositional probability $p=0.6$ with both the old method and our new
method. 
The results of these tests are given in 
Figures \ref{results-d1-mp06-old}~and~\ref{results-d1-mp06-new}.
\new{1}{sentence added} As before, the asymmetries between the satisfiability and unsatisfiability  
curves in Figure~\ref{results-d1-mp06-new} for $N=5,6$ are due to the 
fact that many tests are not solved by \Dlp{} within the time limit 
(c.f., Footnote~\ref{symmetry_footnote}). 

As expected, the old method produces large numbers of trivially
unsatisfiable formulae.  These trivially unsatisfiable formulae show up
much earlier than with $p=0.5$, making the tests considerably
easier, especially for \Ssat{}.

Our new method produces hard formulae, but ones that are quite a
bit easier than for $p=0.5$.
\new{1}{Modified}
In particular, \Dlp{} solved all instances within the time limit for  $\nvar=4$.
Trivially unsatisfiable formulae do show up, but only well after the
formulae are already unsatisfiable, and they do not significantly affect
the difficulty of the tests.

So our method allows the creation of more-interesting tests at modal
depths greater than $1$, simply by adjusting $p$ to a value where the level
of difficulty is appropriate.  Trivial unsatisfiability is not a problem,
whereas in the old method it was the most important feature of the test.


\subsection{Changing the Size of Clauses} 
\label{c_subsec}

A problem with increasing the propositional probability is that formulae
become ``too propositional'' ---that is, the source of difficulty becomes
more and more the propositional component of the problem, and not the modal
component.  As we are interested in {\em modal} decision procedures, we
do not want the main (or only) source of difficulty to be propositional
reasoning.

We decided, therefore, to investigate a different method for modifying the
difficulty of the generated formulae.
We instead allow the number of literals in a clause $C$ to vary in a manner similar to
the number of propositional atoms.
If $C$ is an integer then each clause has that many literals.
Otherwise, we allow either $\lfloor C \rfloor$ or
$\lceil C \rceil$ literals in each clause, 
with probability $\lceil C \rceil - C$ and $C - \lfloor C \rfloor$,
respectively.  
We then determine the number of propositional atoms in each clause based on
the number of literals in that clause.

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2c25-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2c25-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2c25-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2c25-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2c25-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2c25-90.ps}
\end{tabular}
\caption{Results for $C=2.5$, $m=1$, $d=2$, and $p=0.5$ (our new method)}
\label{results-d2-c25}
\end{figure}

We generated \mcnf{} formulae with $C=2.5$, $m=1$, $d=1$, and $p=0.5$.
The change from $C=3$ to $C=2.5$ produces fewer disjunctive choices and should
result in easier formulae.
The results of these tests are given in Figure~\ref{results-d2-c25}.

These formulae are much easier than those generated with $C=3$, although
they are still quite hard and form a reasonable %, but limited, 
source of testing data. 
Trivially unsatisfiable formulae appear in large
numbers only well after the formulae are all unsatisfiable and relatively
easy.

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2c225-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2c225-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2c225-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2c225-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2c225-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d2c225-90.ps}
\end{tabular}
\caption{Results for $C=2.25$, $m=1$, $d=2$, and $p=0.5$ (our new method)}
\label{results-d2-c225}
\end{figure}

To further illustrate the reduction in difficulty with smaller values of $C$
we generated formulae using $C=2.25$, $m=1$, $d=1$, and $p=0.5$.
As shown in Figure~\ref{results-d2-c225}, these formulae are even easier
than for $C=2.5$.  
Trivially unsatisfiable formulae do appear, but again only after the 
formulae become all unsatisfiable, and not until the formulae
become easy, particularly for \Ssat.

At $C=2.25$ we now have a reasonable set of formulae for maximum modal
depth $d=2$.  With a maximum modal depth of $2$, the formulae are much more
representative than formulae with maximum modal depth of $1$.  The formulae
are neither too easy nor too hard for current modal decision procedures so
the satisfiability transition can be investigated for significant numbers
of propositional variables.

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2v4cw-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2v4cw-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2v4cw-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd2v4cw-90.ps}
\end{tabular}
\caption{Results for $N=4$, $m=1$, $d=2$, and $p=0.5$ (our new method)}
\label{results-d2v4cw}
\end{figure}

Further, with this new method we can provide a collection of test
sets that vary in difficulty by varying $C$.  Most previous comparative
test sets varied $\nvar$, which is problematic because most interesting
parameter sets become too hard for small values of $\nvar$, in the range of
$6$ to $10$. 

To illustrate the effects of varying $C$ we generated formulae using 
$N=4$, $m=1$, $d=1$, and $p=0.5$, varying $C$ from $2.2$ to $2.8$.
As shown in Figure~\ref{results-d2v4cw}, this produces an interesting set
of tests.  The difficulty levels can be set appropriately.  Trivially
unsatisfiable formulae do appear, but only %dominate well 
after the formulae
become unsatisfiable anyway.  Trivially unsatisfiable formulae do not
influence the difficulty of the test.


\subsubsection{Modal Depth $3$}


\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd3c225-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd3c225-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd3c225-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-dd3c225-90.ps}
\\
\Ssat{} median times
&
\Ssat{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d3c225-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-s3d3c225-90.ps}
\end{tabular}
\caption{Results for $C=2.25$, $m=1$, $d=3$, and $p=0.5$}
\label{results-d3-c225}
\end{figure}


Our method can be used to generate interesting test sets with
modal depth $d=3$.  This depth is not at all interesting with previous
methods---either the formulae are immensely difficult, such as for $p=0$,
or the behavior is dominated by trivial unsatisfiability, such as for
$p=0.5$.

For interesting levels of difficulty, we do have to reduce $C$ to values below 
$2.5$.  If $C$ is much larger, the formulae are too hard.  
However, with $C \leq 2.5$ we can produce interesting test sets, as shown in
Figure~\ref{results-d3-c225}.  
(The relevant asymmetry between the satisfiable and unsatisfiable rates
curves for $\nvar \geq 5$ is due 
to the high amount of tests exceeding the time limit.)
Here the problems are hard
even for $\nvar \leq 5$ but doable, and there are no problems with
trivially (un)satisfiable formulas.

Our method now allows us fine control of the difficulty of tests.  To make
a test easier, we can just reduce the size of clauses by reducing the
value(s) of $C$, or increase the propositional probability $p$.
This control was missing with the previous method, 
as $C$ was restricted to integral value, and, anyway, was always set to $3$
and making $p$ much different from $0.0$ resulted in problems with trivial
unsatisfiability for maximum modal depths greater than 1.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% A new \mcnf{} generation method: advanced version
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{A New \mcnf{} Generation Method: Advanced Version}
\label{new_testing2_sec}

Actually, our generator is much more general than what we have
described so far. 
We allow direct specification of the probability distribution of
the number of propositional atoms in a clause, and allow the distribution
to be different for each modal depth from the top level to $d-1$.
We also allow direct specification
of the probability distribution for the number of literals in a clause at
each modal depth. Thus, the probability distribution for the
number of propositional atoms depends on both the modal depth and the number
of literals in the clause.

\subsection{Generalization: Shaping the Probability Distributions.}
\label{shape_subsec}


The generator has two parameters to control the shape of formulae.
%We illustrate the behavior by some examples. 
The first parameter, $C$, is a list of lists (e.g., {\tt [[0,0,1]]\/})
telling it how many disjuncts to put in each
disjunction at each modal level. 
%
Each internal list represents a finite discrete probability
distribution. 
%
For instance, the ``{\tt [0,0,1]\/}'' says ``$0/1$ of the disjunctions
have $1$ disjunct, $0/1$ have $2$ disjuncts, and $1/1$ have $3$
disjunctions'' (fixed length 3).
Because there is only one element of the list, this frequency is used at
each modal depth, until the last. Other possibilities are, e.g., 
{\tt [[1,1,1,1]]} (maximum length 4 with uniform distribution),
{\tt [[16,8,4,2,1]]} (maximum length 5 with exponential distribution),
and so on. 

The second parameter, $p$, is a list of lists of lists (e.g., {\tt
  [[[],[],[0,3,3,0]]]}) that controls the propositional/modal
rate.  The top-level elements are for each modal depth (here all the same).
The second-level elements are for disjunctions with 1,2,3,... disjunctions
(here only the third matters as all disjunctions have three disjuncts).  
For instance, the
``{\tt [0,3,3,0]}'' says ``$0/6$ of the disjunctions have $0$ propositional atoms, $3/6$
have $1$ propositional atom, $3/6$ have $2$ propositional atoms, and $0/6$ have $3$
propositional atoms'' (that is, our new scheme discussed in the
paper with $p=0.5$; the old scheme with $p=0.5$ is represented by {\tt [[[],[],[1,3,3,1]]]}).
Notice that the first element of the distributions in $C$ represents
the value $1$, whilst the first element of the distributions in $p$ represents
the value $0$.
Setting the last element of each distribution to zero 
{\tt [...,0]\/} eliminates all  strictly
propositional clauses, which are the main cause of trivial
unsatisfiability; this is the way we implement the constraint 
$p \leq (C-1)/C$ of Section \ref{p_subsec}.

\medskip

For instance, the plots of
Figures~\ref{results-d1-old}-\ref{results-d3-c225} can be obtained with
the following choices of {\tt C} and  {\tt p}: \\
\begin{tabular}{@{}|l|l|l|l|l|@{}}
\hline
Fig. & {\tt C} & {\tt p} & {\tt C} (advanced version) & {\tt p}  (advanced version)\\
\hline
\ref{results-d1-old},
\ref{results-d2-old} & 3 & 0.5 (old) & {\tt [[0,0,1]]} & {\tt [[[],[],[1,3,3,1]]}\\ %C=3,p=0.5, old
 \ref{results-d1-new}, \ref{results-d2-new} & 3 &  0.5 (new) & {\tt [[0,0,1]]} &  {\tt [[[],[],[0,3,3,0]]}\\ %C=3,p=0.5, new
 \ref{results-d1-p0}, \ref{results-d2-p0} & 3 & 0 & {\tt  [[0,0,1]]} &  {\tt [[[],[],[1,0,0,0]]}\\ %C=3,p=0, old&new
 \ref{results-d1-mp06-old} & 3 & 0.6 (old) & {\tt  [[0,0,1]]} &  {\tt [[[],[],[8,36,54,27]]}\\ %C=3,p=0.6, old
 \ref{results-d1-mp06-new} & 3 & 0.6 (new) & {\tt  [[0,0,1]]} &  {\tt [[[],[],[0,1,4,0]]}\\ %C=3,p=0.6, new
 \ref{results-d2-c25} & 2.5 & 0.5 (new) & {\tt  [[0,1,1]]} &  {\tt [[[],[0,3,0],[0,3,3,0]]}\\ %C=2.5,p=0.5
 \ref{results-d2-c225}, \ref{results-d3-c225} & 2.25& 0.5 (new) & {\tt  [[0,2,1]]} &  {\tt [[[],[0,3,0],[0,3,3,0]]}\\ 
 \ref{results-d2v4cw} & 2.2, 2.4, & 0.5 (new) & {\tt [[0,4,1]]}, {\tt [[0,3,2]]} &  {\tt [[[],[0,3,0],[0,3,3,0]]}\\ 
 & 2.6, 2.8 &  & {\tt  [[0,2,3]]}, {\tt [[0,1,4]]} &  \\ 
%% \ref{results-d2v4cw}: & {\tt  [[0,4,1]] } &  {\tt [[[],[0,3,0],[0,3,3,0]]}\\ 
%%  & {\tt  [[0,3,2]]} & \\ 
%%  & {\tt  [[0,2,3]]} & \\ 
%%  & {\tt  [[0,1,4]]} & \\ 
\hline
\end{tabular}

%\footnotesize
\begin{figure}[t]
\begin{tabbing}
\hspace{0.7cm}\= %to center the algorithm
\hspace{.5cm}\= \hspace{.5cm}\= \hspace{.5cm}\= \hspace{.5cm}\= \hspace{.5cm}\= \hspace{4.4cm}\= \hspace{1.1cm}\= \hspace{.7cm}\= \\
1\>{\bf function} {\em rnd\_\mcnf{}(d,m,L,N,p,C)\/} \\
2\>\>{\bf for\/} {\em i := 1\/} {\bf to\/} $L$ {\bf do\/}\>\>\>\>\>/* generate $L$ distinct random clauses */ \\
3\>\>\>{\bf repeat}\\
4\>\>\>\>$Cl_i$ := {\em rnd\_clause(d,m,N,p,C)\/}; \\
5\>\>\>{\bf until\/} {\em is\_new(Cl$_i$)\/};\>\>\>\>/* discards $Cl$ if it already occurs */\\
6\>\>{\bf return\/}  $\bigwedge_{i=1}^{L} Cl_i$; \\
\>\>\\
7\>{\bf function} {\em rnd\_clause(d,m,N,p,C)\/} \\
8\>\>$K$ := {\em rnd\_length(d,C)\/}; \>\>\>\>\>/* select randomly the clause length */ \\
9\>\>$P$ := {\em rnd\_propnum(d,p,K)\/};\>\>\>\>\>/* select randomly the prop/modal rate */ \\
10\>\>{\bf repeat}\\
11\>\>\>{\bf for\/} {\em j := 1\/} {\bf to\/} $P$ {\bf do\/} \>\>\>\>/* generate P distinct random prop. literals */ \\
12\>\>\>\>$l_j$ := {\em rnd\_sign()\/}$\cdot${\em rnd\_atom(0,m,N,p,C)\/};\\
13\>\>\>{\bf for\/} {\em j := P+1\/} {\bf to\/} $K$ {\bf do\/} \>\>\>\>/* generate K-P distinct random modal literals */ \\
14\>\>\>\>$l_j$ := {\em rnd\_sign()\/}$\cdot${\em rnd\_atom(d,m,N,p,C)\/};\\
15\>\>\>$Cl := \bigvee_{j=1}^{K} l_j$; \\
16\>\>{\bf until\/} {\em no\_repeated\_atoms\_in(Cl)\/};\>\>\>\>\>/*
discards Cl if contains repeated atoms */\\
17\>\>{\bf return\/}  $Sort(Cl)$; \\
\\
18\>{\bf function} {\em rnd\_atom(d,m,N,p,C)\/} \\
19\>\>{\bf if\/} {\em d=0\/} \\
20\>\>{\bf then  return\/} {\em rnd\_propositional\_atom(N)\/};\>\>\>\>\>/* select randomly a prop. atom */ \\
21\>\>{\bf else \/} \\
22\>\>\>$\Box_r$ {\em :=  rand\_box(m)\/};\>\>\>\>/* select randomly an indexed box */ \\
23\>\>\>$Cl$ {\em := rand\_clause(d-1,m,N,p,C);\/}\\
24\>\>\>{\bf return\/}  $\Box_r Cl$ ;
\end{tabbing}
\caption{Schema of the new \mcnf random generator.}
\label{randgen_fig} % ALGO RANDOM GENERATOR
\end{figure}

Our generator works as described in Figure~\ref{randgen_fig}.
The function {\em is\_new(Cl$_i$)\/} checks if $Cl_i\neq
Cl_j,\ \forall\ j<i$;
{\em rnd\_length(d,C)\/} selects randomly the clause length
according to the $d+1$-th distribution in $C$ (e.g, if $d$ is $1$ and $C$ is {\tt
[[0,1,1]\underline{[1,2]}[1]]\/}, it returns $1$ with probability 
$1/3$ and $2$ with probability $2/3$);
{\em rnd\_propnum(d,p,K)\/} selects randomly the number of propositional
atoms per clause $P$ 
according to the $[d+1,K]$-th distribution in  $p$ (e.g, if $d$ is
$1$,  $K$ is $2$ and $p$ is 
{\tt [[[],[0,1,0],[0,1,0,0]]\ [[1,0]\underline{[0,1,0]}]]\/}, 
it returns $1$ deterministically);
{\em rnd\_sign\/} selects randomly either the positive or negative
sign with equal probability;
{\em no\_repeated\_atoms\_in(Cl)\/} checks if the clause $Cl$ contains
no repeated atom;
{\em Sort(Cl)\/} returns the clause $Cl$ sorted according to some 
criterium;
{\em rnd\_propositional\_atom(N)\/} selects with uniform probability 
one of the $N$ propositional atoms $A_i$;
{\em rnd\_box(m)\/} selects with uniform probability 
one of the $m$ indexed boxes $\Box_r$.

When eliminating duplicated atoms in a clause,
we take care not to disturb these probabilities by first determining the
``shape'' of a clause (rows 8-9 in
Figure~\ref{randgen_fig}), and only 
then instantiating that with propositional variables (rows 10-16 in
Figure~\ref{randgen_fig}).   If a clause has
repeated atoms, either propositional or modal, the instantiation is
rejected and another instantiation of the shape is performed.
If we did not take care in this way we would generate too few ``small''
atoms because there are fewer small atoms than large atoms, resulting in a
greater chance of rejecting small atoms because of repetition.

The elimination of duplicated atoms in a clause is not only a matter
 \new{1}{paragraph added}
 of  elimination of redundancies, but also of elimination of a source
 of flaws. In fact, one might generate top-level clauses like 
$...\wedge (\neg\Box_1(A_1\vee\neg A_1)\vee \neg\Box_2(A_2\vee\neg A_2))\wedge ...$, 
which would make the whole formula inconsistent. 



%%%%%%%%%%%%%%%%%%%%%% EXAMPLE %%%%%%%%%%%%%%
\begin{example}
\label{shape_ex}
We try to guess a parameter set by which the new random generator
can potentially generate  the following \mcnf{}
formula $\vi$:
\begin{equation}
\begin{array}{lll} ( & 
\neg A_3 \vee 
\Box_1(\neg A_4 \vee \neg \Box_1 A_1    
  ) \vee
\Box_1(\neg A_1 \vee
   \neg \Box_1 A_2
  )
& )\ \wedge \\ ( & 
\neg A_1 \vee 
\Box_1( A_3 \vee \neg \Box_1 A_2 
  ) \vee  
\neg \Box_1(\Box_1 \neg A_4) 
& )\ \wedge \\ ( &  
\neg A_4 \vee
\neg \Box_1( A_2 \vee \Box_1 \neg A_1 ) 
& )\ \wedge \\ ( & 
A_1 \vee \neg \Box_1(\neg \Box_1 A_4) 
& ). \\
\end{array}
\label{wff_ex_equ}
\end{equation}
After a quick look  we  set
 $m=1$, $d=2$, $N=4$, $L=4$. 
%
At top level we have 0 unary, 2 binary  and 2 ternary clauses; 
at depth 1 we have 2 unary and 4 binary clauses;
at depth 2 we have only 6 unary  clauses.
Thus, we can set 
\begin{equation}
\mbox{{\tt C = [[0,2,2],[2,4],[6]].}}
\label{c_ex_eq}
\end{equation}
%
\new{1}{sentence added}\new{1,3}{fixed}
 At top level there are no unary clauses 
(we represent this fact by
the empty list  
``{\tt []}''),  the 2 binary clauses have 1 propositional
literal, and the 2 ternary clauses have 1 propositional literal;
at depth 1, the 2 unary clauses have 0 propositional literals,
while the 4 binary clauses have 1 propositional literal.
(There is no need to provide any information for depth 2,
as all clauses are purely propositional.)
Thus, we can set 
\begin{equation}
\mbox{{\tt p = [[[],[0,2,0],[0,2,0,0]]\ [[2,0],[0,4,0]]].}}
\label{p_ex_eq}
\end{equation}
The two expressions can then be normalized into:
\begin{equation}
\begin{array}{l}
\mbox{{\tt C = [[0,1,1],[1,2],[1]]}}\\
\mbox{{\tt p = [[[],[0,1,0],[0,1,0,0]]\ [[1,0],[0,1,0]]]}.}
\label{cp_ex_eq}
\end{array}
\end{equation}
Notice that any other setting of $C$, $p$ obtained by 
changing the non-zero values in (\ref{cp_ex_eq})
 into other non-zero values, or turning 
zeros into non-zeros (but not vice versa!), will 
do the work, just with a different probability.
For instance, turning the first list in $C$ into {\tt [1,1,1]\/}
allows for generating also  unary clauses at top level;
anyway, with probability $(2/3)^L$ the generator may still produce formulae with
only binary and ternary clauses at top level. \ \hfill \  $\Box$
\end{example}


\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-unusual-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-unusual-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-unusual-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-unusual-90.ps}
\end{tabular}
\caption{Results for \Dlp with $d=3,4$, $N=3,4$, $C = ${\tt [[1,8,1]]}, 
  \protect\\
  $p=${\tt [[[1,0],[0,1,0],[0,1,1,0]]]}.} 
\label{results-unusual}
\end{figure}


As an illustration of our general method, we present a set of tests with
$m=1$, $d=3,4$, $N=3,4,$, $C=${\tt [[1,8,1]]}, and  $p=${\tt [[[1,0],[0,1,0],[0,1,1,0]]]}.
This set of tests introduces a small fraction of single-literal clauses
that contain a modal literal (except at the greatest modal depth, where
they contain, of course, a single propositional literal).
The results of tests are given in Figure~\ref{results-unusual}.  
Again, trivial instances occur only  out the interesting zone. 
Here we can generate interesting test sets even with modal depth $4$.


\subsection{Varying the Probability Distributions with the Depth}
\label{vary_depth_subsec}

\begin{figure}[t]
\begin{tabular}{@{}c@{}c@{}}
Satisfiability and Unsatisfiability Fractions
&
Trivial Satisfiability and Unsatisfiability Fractions
\\
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-variable-sat.ps}
\hss}
&
\hbox to 0.5\linewidth{\hss
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-variable-triv.ps}
\hss}
\\
\Dlp{} median times
&
\Dlp{} 90th percentile times 
\\
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-variable-median.ps}
&
\includegraphics[width=0.5\linewidth,height=4.5cm]{Figures/plot-variable-90.ps}
\end{tabular}
\caption{Results  for \Dlp with $d=4,5$, $m=1$, $N=3,4,5$, $C = ${\tt [[1,8,1],[1,2]]}, 
  $p=${\tt [[[1,0],[0,1,0],[0,1,1,0]],[[1,0],[0,1,0]]]}.} 
\label{results-variable}
\end{figure}

Our new method provides the ability to fine-tune  the
distribution of both the size and the propositional/modal rate of the
clauses {\em at every depth\/}.
This fine tuning results in a very large number of parameters, and so far
in this paper we have only investigated distributions that conform to the
scheme described above or ones that correspond to the \kcnf{} generation
method previously used.

To give an example of how to vary the probability distributions
with the nesting depth of the clauses, 
 we consider the case with 
$d=4,5$, $m=1$, $N=3,4,5$, 
$C = ${\tt [[1,8,1],[1,2]]}, 
$p=${\tt [[[1,0],[0,1,0],[0,1,1,0]],[[1,0],[0,1,0]]]}.
The results of the tests are given in Figure~\ref{results-variable}.

The $C$ parameter says that the probability distributions of the
length of the  clauses occurring at nesting depth $0$ and  
$\ge 1$ are {\tt [1,8,1]}  and {\tt [1,2]} respectively. 
(When not explicitly specified, it is considered the last
distribution by default, as in the case of depth $>1$.)
Thus, the top-level clauses are on average $1/10$ unary, $8/10$ binary
$1/10$ ternary, while 
the clauses occurring at depth $\ge 1$ are on average $1/3$ unary and
$2/3$ binary. 

The $p$ parameter says that the lists of probability distributions of
the propositional/modal ratio at  nesting depth $0$ 
and  $\ge 1$ are {\tt [[1,0],[0,1,0],[0,1,1,0]]} and
{\tt [[1,0],[0,1,0]]} respectively.  
Thus, at every depth, unary clauses have no propositional literal and
binary clauses have $1$ propositional and $1$ modal literal. 
The top-level ternary clauses have either $1$ or $2$ propositional
literals, with equal probability. 


Notice that at top level the distributions are identical to those 
of Figure~\ref{results-unusual}, whilst at depth $\ge 1$ there are
no more ternary clauses and a higher fraction of unary clauses.
These slight modifications allow reasonable test sets with
$d=5$ and $N=5$.
Moreover,  trivial instances have nearly disappeared.



%%% Generality of the method
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Generality of the Method}
\label{generality_sec}


We have already observed \cite{Horrocks-IGPL} 
that for normal modal logics, from \Km{} upward, there is no loss 
in the restriction to \mcnf{}
formulae, as there is an equivalence between
arbitrary normal modal formulae and  \mcnf{}  formulae%
\footnote{This holds for all modal normal logics from \Km{} upward, as the 
conversion 
works recursively on the depth of the formula,
from the leaves to the root, each time applying to sub-formulae the
propositional CNF  conversion and the transformation
$$
 \Box_r\bigwedge_j \bigvee_{i}\varphi_{ij} \Longrightarrow 
 \bigwedge_j  \Box_r\bigvee_{i}\varphi_{ij},
 $$
which preserves validity in such logics.}.
We may wonder how well our generation technique covers the whole space 
of \mcnf{}  formulae, and how well  we can approximate a 
restricted subclass of this space. 
Example \ref{shape_ex} represents an instance of a very general
property of our random generation technique, which we present and
discuss below.

\smallskip 
 
Now we assume that the {\em rnd\_\mcnf{}\/} of
Figure~\ref{randgen_fig} is a ``purely random'' generator,
i.e., it performs all non-deterministic choices
independently and in a pure random way. 
(Of course pseudo-random generators only approximate 
this feature.)
Moreover, with no loss of generality, we restrict our discussion to \mcnf{}
formulae which have  no repeated clauses at top level and
no repeated atoms inside any clause at any level, and
in which atoms are   {\em sorted\/} within each clause,
according to the generic function {\em  Sort()\/} of Figure~\ref{randgen_fig}.
The former allows for considering only formulae which are already 
simplified out; the latter allows for considering only one
representative for each class of formulae which are equivalent
modulo order permutations. 
As discussed by
\citeauthor{giunchiglia108}~\citeyear{giunchiglia108}, the latter allows
for further simplifying  
subformulae like, e.g.,  $\Box(A_1\vee A_2)\vee \Box(A_2\vee A_1)$
or $\Box(A_1\vee A_2)\vee \neg\Box(A_2\vee A_1)$.

\smallskip


%%%%%%%%%%%%%%%%%%%% TECHNIQUE TO GENERATE C AND P %%%%%%%%%%%%%%
Let $\vi$ be a sorted \mcnf{} formula of depth $d$ and with $L$
top-level clauses
built on all the propositional atoms $\{A_1,...A_N\}$ 
and on all the modal boxes $\{\Box_1,...\Box_m\}$,
 which has no repeated clause at top level and
no repeated atoms inside any
clause at any level. 
Then we can construct $C$ and $p$ so that, for each $i$, $j$, $r$: 
\begin{aenumerate}
\item the $j$-th element of the $i$-th sublist in $C$ is
%\new{3}{} 
non-zero if and only if 
there is a clause of length $j$ occurring at depth $i$ in $\vi$, 
and 
\item the $r+1$-the element of the $j$-th sub-sublist of the $i$-th sublist in $p$ is
non-zero
if and only if
there is a clause of length $j$ occurring at depth $i$ which 
contains $r$ propositional literals.
\end{aenumerate}

%%%%%%%%%%%%%%%%%%%% OPERATIVE TECHNIQUE TO GENERATE C AND P %%%%%%%%%%%%%%
\noindent
One possible operative technique to build $C$ and $p$ works as
follows. 
Initialize $C$ as a list of $d+1$ sublists. 
Then, for every depth level $i \in \{0,...,d\}$, set the $i$-th 
sublist of $C$ as follows:
\begin{renumerate}
  \item set the size $K$ of the sublist as the maximum size of clauses
  occurring in $\vi$ at depth $i$;
  \item for all $j \in \{1,..,K\}$, count the number of clauses of
  length $j$ occurring in $\vi$ at depth $i$, and append the result to the sublist.
\end{renumerate}

\noindent
Initialize  $p$ as a list of $d$ sublists of sub-sublists. 
Then, for every depth level $i \in \{0,...,d-1\}$, set the $i$-th 
sublist of $p$ as follows:
\begin{renumerate}
  \item look at $C$: set the size $K$ of the sublist as the maximum size of clauses
  occurring in $\vi$ at depth $i$;
  \item for all $j \in \{1,..,K\}$, generate the $j$-th sub-sublist
  as follows:
    \begin{itemize}
    \item look at $C$: if the number of clauses of length
     $j$ occurring at depth $i$ is non-zero, then set the length $l$ of
  the sub-sublist to $j+1$,
else set $l$ to 0;
    \item for all $r \in \{0,..,l-1\}$, count the number of
  clauses of
  length $j$ occurring in $\vi$ at depth $i$ which have $r$
  propositional literals, and append the result to the sub-sublist.
    \end{itemize}
\end{renumerate}

\noindent
Example \ref{shape_ex} represents an instance of application of the
above technique for construction $C$ and $p$ from $\vi$.
Notice that the $C$ and $p$ parameters not only verify points $(a)$ and
$(b)$ above, but are such that the probability distributions mimic
the actual number of occurrences of the different kinds of clauses.  
% To match points $(a)$ and $(b)$ above it is not necessary to count 
% the occurrences of a certain kind of clause, rather it is enough to detect there is 
% at least one. 

%%%%%%%%%%%%%%%%%%%% THEOREM %%%%%%%%%%%%%%
\begin{theorem}
Let rnd\_\mcnf{} be a purely random generator as in Figure~\ref{randgen_fig}.
%
Let $\vi$ be a sorted \mcnf{} formula of depth $d$ and with $L$
top-level clauses
built on all the propositional atoms in $\{A_1,...A_N\}$ 
and on all the modal boxes in $\{\Box_1,...\Box_m\}$,
 which has no repeated clause at top level and
no repeated atoms inside any
clause at any level.
%
Let $C$ and $p$ be built from $\vi$  so that to verify points $(a)$ and
$(b)$ above. 
%
Let $C'$ and $p'$ be obtained from $C$ and $p$ respectively 
by substituting some zero-values with some non-zero values.
%
Then we have:
\begin{renumerate}
\item 
rnd\_\mcnf{}(d,m,L,N,p,C) returns $\vi$ with some non-zero
probability ${\cal P\/}$; 
\item 
rnd\_\mcnf{}(d,m,L,N,p',C') returns $\vi$ with some non-zero
probability ${\cal P'\/}\le{\cal P\/}$.
\end{renumerate}
\label{shape_theo}
\end{theorem}
 

%%%%%%%%%%%%%%%%%%%% PROOF %%%%%%%%%%%%%%
\noindent
\begin{proof}
\noindent
The fully-detailed proof is reported in Appendix. \new{3}{Proof
  \mbox{drastically} shortened, full proof moved to appendix}
Here we sketch the main steps.

The following facts come straightforwardly by induction on the
structure of $\vi$: 
\begin{enumerate}
\item 
every propositional atom  occurring in $\vi$ at some depth $i$ 
is returned with the same non-zero probability ${\cal P\/}_1$ by 
both {\em rnd\_atom(0,m,N,p,C)\/} and {\em rnd\_atom(0,m,N,p',C')\/};
\item 
every modal atom $\Box_v Cl$ occurring in $\vi$ at some depth $i$ 
is returned with some non-zero probability ${\cal P\/}_2$ by 
{\em rnd\_atom(d-i,m,N,p,C)\/}, and 
is returned with some non-zero probability ${\cal P'\/}_2\le {\cal P\/}_2$ by 
{\em rnd\_atom(d-i,m,N,p',C')\/};
\item 
every clause $Cl$ occurring in $\vi$ at some depth $i$ 
is returned with some non-zero probability ${\cal P\/}_3$ by 
{\em rnd\_clause(d-i,m,N,p,C)\/}, and
is returned with some non-zero probability ${\cal P'\/}_3\le {\cal P\/}_3$ by 
{\em rnd\_clause(d-i,m,N,p',C')\/}.
\end{enumerate}

\noindent
Thus, every top level clause $Cl_k$ 
is  returned by {\em rnd\_clause(d,m,N,p,C)\/} 
and {\em rnd\_clause(d,m,N,p',C')\/} with some non-zero probabilities
 ${\cal P\/}_{k}$ and ${\cal P'\/}_{k}$ respectively, being
${\cal P'\/}_{k} \le {\cal P\/}_{k}$.
From this fact, it comes straightforwardly that $\vi$ is returned 
by {\em rnd\_\mcnf{}(d,m,L,N,p,C)} and {\em rnd\_\mcnf{}(d,m,L,N,p',C')} with some non-zero probabilities
 ${\cal P\/}$ and ${\cal P'\/}$ respectively, being
${\cal P'\/} \le {\cal P\/}$.
\hfill Q.E.D.\\
%$\Box$
\end{proof}

From a theoretical viewpoint, 
Theorem~\ref{shape_theo} $(i)$ shows that 
our generation technique is very general, 
because, for every \mcnf{} formula $\vi$,
there exists a choice for the parameters
s.t. a purely random generator returns $\vi$ 
with some non-zero probability ${\cal P\/}$.

Of course, the choice criterium for $C$ and $p$ suggested 
by points $(a)$ and $(b)$ 
is not unique as, for example,
any other setting obtained from it  by 
turning zeros into non-zeros would match the
requirements. 
As an extreme case, we might think to do very general choices like 
\begin{equation}
\begin{array}{l}
\mbox{{\tt C = [[1,1,1,...],...]  p = [[[[1,1],[1,1,1],[1,1,1,1]...]]]}.}
\label{cp_all_eq}
\end{array}
\end{equation}
which guarantee to have every possible \mcnf{} 
formula within a given bound in clause size with non-zero probability.
Anyway, Theorem~\ref{shape_theo} $(ii)$ shows that,
extending the number of non-zeros values,
the probability of generating $\vi$ decreases.

For instance, consider Example~\ref{shape_ex}. Turning  
the first list in $C$ of (\ref{cp_ex_eq}) into {\tt  [1,1,1]\/}
 would still allow for generating the formula
(\ref{wff_ex_equ}), but it 
would allow for generating also  unary clauses at top level with
probability $1-(2/3)^L$, which converges  quickly to $1$ with $L$.

\smallskip

Usually we are not interested in randomly generating 
one precise formula with some non-zero probability ---which would
be rather small anyway--- but rather to randomly generate a class 
of formulae which are as similar as possible a given  target class of
formulae. Adding redundant non-zeros would extend the range 
of shapes for formulae, extending the variance and lowering the
resemblance to the target class of formulae.





%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Discussion
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Discussion}
\label{discussion_sec}

\subsection{The Basic and the Advanced Method}
 
Our new testing method can be used at two different levels,
depending on the attitude ---and on the skills and experience--- of the user. 
 
\smallskip
In the {\em basic\/} usage 
the clause length $C$ is represented by lists with either only one non-zero
element (e.g., {\tt [[0,0,1]]\/}, meaning ``clause length $2$'') 
or  only two adjacent non-zero elements
(e.g., {\tt [[0,2,1]]\/}, meaning ``clause length $2$ or $3$, with
 probability $2/3$ and $1/3$ respectively'');
similarly, the propositional/modal rate $p$ is represented by lists 
with either only one non-zero
element (e.g., {\tt [[[],[],[0,1,0,0]]]\/}, meaning ``$1$ propositional
literal per clause'') 
or  only two non-zero adjacent elements 
(e.g., {\tt [[[],[],[0,3,2,0]]]\/}, meaning ``either $1$ or $2$
propositional literals per clause, with
probability $3/5$ and $2/5$ respectively'');
the distributions do not vary with the depth.

In the basic way the random generator is used  as a ``flawless''%
\footnote{In the sense of ``free from the flaw
highlighted in the work by
\citeauthor{hustadt3}~\citeyear{hustadt3} and
\citeauthor{giunchiglia108}~\citeyear{giunchiglia108}''.} 
extension of \new{3}{footnote added}
the \kcnf{} method of
\citeauthor{giunchiglia93}~\citeyear{giunchiglia93},  which allows for
setting the clause length to either 
fixed integer values or to non-integer average values.
The number of parameters  is kept relatively small, so that to allow
a coarse-grained coverage of a significant subspace with an affordable 
number of tests. 

\smallskip 

In  the {\em advanced\/} usage, 
it is possible to apply any finite probability distributions
to  both $C$ and $p$;
moreover, it is possible to use different 
distributions at  different depths.
This opens a huge amount of possibilities, but 
requires some skills and experience from the user:
the representation of sophisticated multi-level
distributions may be rather complicated, %\new{3}{added ``experience''}
and may thus require some practice;
moreover, the usage of complex distributions requires some care, 
as the presence non-constant distributions in both clause length and 
propositional/modal rate may significantly enlarge the variance of the 
features of the generated formulae, making the effects of the tests 
more unpredictable and instance-dependent. 

\smallskip
In order to guide the user, we  provide some general
suggestions for  \new{3}{paragraphs added}  
choosing the parameter sets in a testing session. 
They come from both theoretical issues and our practical experience in
using the generator. 
\begin{itemize}
\item %(Mandatory!)
 Avoid generating purely
propositional top-level clauses, that is,  set {\tt p =
  [[...,0],...]}. See 
Sections~\ref{p_subsec} and ~\ref{shape_subsec}.
%\item 
If possible, avoid generating unary top-level clause, that is,  set {\tt C =
  [[0,...],...]}). See also Section~\ref{asymptotic_sec}. 
\item In organizing a testing session, fix the parameter sets
  according to the following order and directives. 
  \begin{renumerate}
    \item Fix  {\tt d}. 
With {\tt d=1} the search is mostly dominated by its propositional component, 
with {\tt d>2} it tends to be dominated by its modal component.
{\tt d=2}  is typically a good  start. 
    \item Fix {\tt m}. 
 {\tt m} 
substantially partitions the problem into {\tt
         m} independent problems.  
Increasing {\tt m}, the samples tend to be more
likely-satisfiable. 
{\tt m=1}  is typically a good start. 
    \item Set {\tt C}. 
    Increasing the top level values of {\tt C}, the samples tend to be more
likely-satisfiable and the
propositional component of search increases, so that 
the transition area moves to the right and the hardness peaks grow.
    Average values in $[2.0,3.0]$ for the top level distributions of
    {\tt C} are typically a good  start. 
    \item Set {\tt p}. Decreasing the  top level values of {\tt p},
the modal component of search  increases.
For the the top level distributions of {\tt p}, having on average
half of top-level atoms propositional  (that is, the $p=0.5$ of Section
~\ref{new_testing_sec}) is    typically a good start.  
    \item For each choice of the above parameters, increase {\tt N},
      starting from (at least) the maximum length in {\tt C}, until 
the desired level of hardness is reached. 
    \item Make {\tt L} vary within the satisfiability transition
      area. 
  \end{renumerate}
\item When dealing with {\tt C} and {\tt p}, focus on top-level clause distributions first. Small
  variations of  {\tt C} and {\tt p}  at top level may cause big
  variations in hardness and satisfiability probability. Variations at
  lower levels typically cause much smaller effects. 
\item Use convex distributions: e.g., {\tt [1,5,1]} and {\tt
    [5,1,5]} have the same mean value, but the variance of the former
  is much smaller than that of the latter. 
\item Do keep {\tt L} ranging in the satisfiability transition area: 
increasing {\tt L} out of it, the fraction of trivially
unsatisfiable samples can become relevant. 
To determine the satisfiability  transition area, make a
preliminary check with few samples per point (say, 10) using 
dichotomic search. 
\item Unlike {\tt N} (and {\tt m}), the parameters {\tt d}, {\tt C}, {\tt p} make  the formulas vary
  their shape. 
Thus, we suggest to group together plots with the same {\tt d}, {\tt
  C} and {\tt  p} values and increasing {\tt N}'s.
\end{itemize}

 
On the whole, the large number of parameters makes it impossible to cover the parameter
space in a reasonable amount of testing.  However, just about any \mcnf{}
formula shape can be generated so that
the method described in Section~\ref{generality_sec}  can 
be used to produce random formulae
reasonably similar to some  formula(e) of interest.
 
\subsection{Comparison with the Old \kcnf{} Method}

On the whole, the new method inherits all the features of the old \kcnf{} method. 
\begin{description}


\item[Scalability:] 
Increasing $N$,  $d$ (and also the average clause length in $C$) the 
difficulty of the generated problems scales
up at will. Thus it is possible to compare  how the performance of
different systems scale up with problems of increasing difficulty, for
each source of difficulty (e.g., size, depth, etc.).
 
\item[Valid vs.\ not-valid balance:] 
The parameter $L$ allows for tuning the satisfiability rate of the
formula at will. Moreover, it is always possible to choose $L$ 
to generate testbeds with about a 50\%-satisfiable rate, which allows
for the maximum uncertainty.   

\item[Termination:] The new method allows for generating test sets 
of up to depth 3-4 which are run by state-of-the-art systems in 
a reasonable amount of time. 

\item[Reproducibility:] 
The results of each  testbed are easy to reproduce because
\new{3}{modified}
the generator's code and all the parameters' values are made publicly available.  

\item[Parameterization:] 
The random generation of \mcnf{} %\new{1}{}
formulae is fully parametric.  

\item[Data organization:] 
The most natural way to use the new random generator is to  generate tests 
and plot data by increasing values of one or two  parameters. 
This allows for easy, quantitative and qualitative evaluations of the
performances of the different procedures under test. 
\end{description}

\noindent
Moreover, the new method  improves the \kcnf{} method for the following features. 

\begin{description}
\item[Representativeness:] As stated in Section~\ref{generality_sec},
  \new{1}{``significance'' substituted}
\mcnf{} formulae represent all formulae in the
normal modal logics from \Km{} upward, 
as  there is an equivalence-preserving way of 
converting all modal formulae into \mcnf{}.  
% \footnote{This can be done recursively on the depth of the formula,
% from the leaves to the root, each time applying to subwffs the
% propositional CNF conversion and the transformation
% \mbox{$
% \Box\bigwedge_j \bigvee_{i}\varphi_{ij} \Longrightarrow 
% \bigwedge_j  \Box\bigvee_{i}\varphi_{ij}.
% $}}
From Theorem~\ref{shape_theo}, the new  method allows for a very
fine-grained sampling of the  
class of \mcnf{} formulae. 

\item[Difficulty:] 
The random \mcnf{} formulae with $d\ge 2$ and $N\ge 4$ provide challenging test sets 
for state-of-the art procedures. 
\mcnf{} formulae with $d\ge 4$ and $N\ge 9$ can be well considered as
challenges for next-generation systems. (Of course, it is not a problem
to generate easy problems too.) \new{1,3}{sentence added}

\item[Control:] 
The parameters $N$, $d$ and $C$ allow for controlling 
{\em monotonically} the difficulty of the test set.
(E.g., if you increase $N$, you are reasonably sure that 
your mean/median CPU time plots will increase.)
The parameter $L$ allows for controlling the satisfiability rate. 
% Remarkably, the parameters  $d$, $N$, $m$, \ldots{} have a direct
% meaning (modal depth, number of prop. variables, \ldots{}). This 
% provides {\em a priori\/} a coarse idea  --modulo randomness-- of
% what the resulting formulae will look like.  
 Monotonicity allows for controlling one feature
 by simply increasing or decreasing one value,  and thus for
 eliminating uninteresting areas of the input space. 

\item[Modal vs.\ propositional balance:]
The size of the Kripke models spanned by the decision procedures
has increased exponentially with the higher modal depths 
reached by the new test sets; moreover, the probability of repeated  
top-level atoms has dramatically reduced.%
\footnote{
The number of possible distinct modal atoms increases 
hyper-exponentially with $d$ \cite{Horrocks-IGPL}.}
Consequently, unlike the tests by
\citeauthor{hustadt3}~\citeyear{hustadt3} and
\citeauthor{giunchiglia108}~\citeyear{giunchiglia108}
the search is no longer dominated by the pure propositional component of
reasoning, and the empirical results show that a large number of modal
successors are explored.  

\end{description}

\noindent
Finally, the new method  completely removes or drastically reduces the effects of
the following problems.

\begin{description}
\item[Redundancy:] 
Propositional and modal redundancy had already been eliminated in
the last versions of the \kcnf{} method \cite{giunchiglia108}. 
Moreover, the new method allows for  eliminating all strictly propositional clauses.
 
\item[Triviality:] 
The main cause of trivial unsatisfiability has been
removed, so that trivially unsatisfiable formulae have been relegated out of the
transition areas in our experiments. 

\item[Artificiality:] 
Our method allows the user to
shape the test formulae so that to maximize
the resemblance to the expected typical inputs of his/her system(s). 
\new{3}{lines  added}
Of course, this is done within the limits imposed by randomness:
 the more irregular the typical input formulas, the higher the
 variance of the randomly generated formulas, the lower their
 average resemblance to the typical input formulas. 


\item[Over-size:]
The new method allows for generating extremely hard problems with
reasonable size. It comes from the analysis of the resulting data 
that hard problems require very big amounts  of both search branches and 
modal successors generated, so that the search is not dominated by 
parsing and data managing. 
 
\end{description}


The generator presented 
by \citeauthor{Horrocks99f}~\citeyear{Horrocks99f},
\new{1}{paragraph added} 
extends the \kcnf{} generator of 
\citeauthor{giunchiglia108}~\citeyear{giunchiglia108}  too. 
However, our new generator allows for shaping the 
probability distributions of both C and p, and for using different
distributions at every depth level. 
In principle, the generator of  
\citeauthor{Horrocks99f}~\citeyear{Horrocks99f} allows also for 
setting the probabilities $n_p$ and $n_m$ by which propositional and
modal atoms are
negated. However, this feature is not used very much---in the experiments
by \citeauthor{Horrocks99f}~\citeyear{Horrocks99f} $n_p$ is 
always $0.5$ and $n_m$ is different from $0.5$ only in one
experiment--- and adds nothing to the generality of the 
generator, so that in our new generator we decided not to re-introduce it.   


\subsection{Comparison with the QBF-based  Method}

Before  comparing our new \mcnf{} generation method 
with the  QBF-based  generation method, we must notice   
that, so far, they have been used in different ways,
corresponding to the two different test techniques briefly summarized in 
Section~\ref{past_testing_sec}.



\begin{itemize}
\item
In the TANCS competition(s) \cite{massacci_TANCS99}, 
the tests have been performed on single data points, and 
the results are presented in the form of big tables,
each entry consisting of  the number of successful solutions 
and in the rescaled geometrical mean CPU time for such solutions.  
Two or more systems are compared according to their number of successful
solutions, considering the geometrical mean CPU time value
only when the result is even.
This is due to the fact that a comparison between geometrical means 
is possible only if they are computed on the same number of successful
values, or, for a more accurate comparison, on the same successful
values.% 
\footnote{
In case of tests exceeding the timeout, 
geometrical means are altered by the truncation introduced 
by the unsuccessful solutions.
Thus the geometrical mean makes sense 
only if calculated only on successful results. 
}
This method was chosen to guarantee the fairness of the comparison
between the competitors, which is the key requirement in a
competition.

\item
In this paper instead, we have focused on highlighting
both the qualitative and quantitative behavior of the  system(s). 
Thus we have preferred plots to tables, and 
we have preferred representing percentiles CPU times rather than %\new{1}{} 
the number of successful solutions and their geometrical mean times.
In fact, the former does not require to distinguish between 
successful and non-successful solutions.%
\footnote{If the percentage of successful solutions is greater or equal
than $Q$, then the value $Q$-th percentile is not influenced by the
truncation of values introduced by timeouts, otherwise 
it is equal to the timeout value.}
Thus, they are much more suitable for plotting, because
a comparison on geometrical means makes sense only for those
data points %\new{1}{} 
with the same number of successful solutions, 
which is very hard to follow in a plot.

\end{itemize}

\noindent
Of course, both generators can be used in both ways.
(See \citeauthor{heguiabehere1}~\citeyear{heguiabehere1} for some plots with the random QBF-based method.) 
Comparing the two approaches above in organizing and presenting 
data is not one of the goals of this paper, so 
we restrict our analysis to the generation methods,
independently from how they have been  used so far. 

\smallskip



The  QBF-based  generation method of 
\citeauthor{massacci_TANCS99}~\citeyear{massacci_TANCS99} 
\new{3}{feature description dropped}
shares with our new \mcnf{} generation method several features
---in particular
{\bf Scalability}, 
{\bf Valid vs.\ not-valid balance}, 
{\bf Termination}, 
{\bf Reproducibility}, 
{\bf Parameterization},
{\bf Data Organization},
{\bf Difficulty},
{\bf Modal vs.\ propositional balance}, 
{\bf Redundancy} and
{\bf Triviality}---
for which considerations which are 
identical or analogous to those for our new method hold, 
once we consider parameters $V$, $D$ and $C$ instead of parameters $N$, $d$
and $L$.~%  
The following features instead deserve more discussion. 

\begin{description}


\item[Control:] 
 The parameters $V$ and $D$  allow for controlling 
 monotonically the difficulty of the test set. 
 The parameter $C$ allows for controlling the satisfiability rate. 
%
 However, unlike the \mcnf{} case, the main parameters of the QBF
 generator (e.g., $D$ and  $V$) do {\em not\/} have a direct
 meaning wrt. the main characteristics of the resulting modal 
 formulae like, e.g., the modal depth and the number of propositional
 variables. 

\item[Representativeness:] 
In general QBF formulae  are good representatives for the whole
\new{1}{``significance'' substituted}
class of quantified boolean 
formulae, as there is a way to
convert a generic quantified boolean formula 
%\new{2}{footnote} 
into QBF.%  
\footnote{Notice that by ``QBF'' here we denote
the class of prenex CNF QBF formulae, given by an alternation of quantification
variables ending with an existential one followed by a CNF
propositional formula. The conversion works by lifting quantifiers outside the formula and
then converting into k-CNF [k-DNF] the matrix if the innest quantifier is an
$\exists$ [a $\forall$, negating the result and pushing down the
negation recursively].  The conversion is truth-preserving [truth-inverting].
}
(The randomly generated QBF formulae used by
\citeauthor{massacci_TANCS99}~\citeyear{massacci_TANCS99}
restrict to those having a fixed amount of variables per alternation.)
%
Nevertheless, the class of modal-encoded QBF formulae
restrict to those having  candidate Kripke structures 
with the very regular  structure imposed by
the QBF and/or binary search trees. 
% Thus we cannot see how they can 
%  be considered as a representative sample of the input space
% of modal formulae. 
% Nevertheless, modal-encoded QBF formulae
% have a very peculiar modal structure, 
% as their candidate Kripke structures 
% are restricted to those having the very regular  structure imposed by
% the QBF and/or binary search trees. Thus we cannot see how they can 
%  be considered as a representative sample of the input space
% of modal formulae. 


\item[Artificiality:] 
% Another problem with modal-encoded random QBF formulae is that they are
% rather artificial, as their candidate Kripke structures 
% are restricted to those having the very regular  structure imposed by
% the QBF and/or binary search trees. 
Unlike the \mcnf{} case, the main parameters of the QBF
generator (e.g., $D$ and  $V$) do not have a direct
meaning wrt. the main characteristics of the resulting modal 
formulae. 
Thus,  it is hard to choose the parameters for 
the random QBF generator so that to resemble expected typical inputs
of the system(s). 

\item[Over-size:]
One final problem with random modal-encoded QBF formulae is size. 
%pfps YES, essentially \todo{Peter, is this still true?}
Initial versions of the translation method produced test sets in the
1GB range, which stressed too much 
the data-storage and retrieval portion of the provers. 
(For example, running \Dlp{} on these formulae resulted in a 1000s timeout
without any significant search.)
Although the encoding has been significantly improved in this
sense,  
the current versions still produce very large modal formulae, mostly to
constrain the Kripke structures.

\end{description}

\noindent
Similar considerations have been very recently presented by
\citeauthor{heguiabehere1}~\citeyear{heguiabehere1}.

% ``POLITICAL'' COMMENT
On the whole, we believe that the QBF generation method 
is still appealing, and that the two methods can co-exist 
in any empirical test session. 
 
\subsection{Complexity Issues}

From a purely theoretical viewpoint, 
it is remarked that modal-encoded QBF formulae 
can capture the problems in $\Sigma_D^P$, 
while \mcnf{} formulae are ``stuck at NP''  
\cite{massacci_TANCS99}%
\footnote{More precisely, 
  \citeauthor{massacci_TANCS99}~\citeyear{massacci_TANCS99} 
  referred to the \kcnf{} formulae of \citeauthor{giunchiglia108}~\citeyear{giunchiglia108}.
  The statement holds  also for all the \mcnf{} formulae.
  }.
This statement requires some clarification.

First, test sets are necessarily {\em finite\/}, 
therefore it makes no sense to attribute to them a complexity class.
Thus, when speaking of complexity classes for test problems, we do not
refer to test sets, but rather to the
{\em infinite\/} sets of formulae we could generate if we could have
 {\em unbounded\/} values for (at least one of)  the generation
parameters.  
In particular, the statement above means that the infinite set
of QBF formulae with unbounded number of variables per
alternation $V$ and bounded alternation depth $D$ 
is complete for $\Sigma_D^P$ \cite{garey1},
while the infinite set of \mcnf{} formulae with bounded depth and 
unbounded number of propositional variables is in NP
\cite{halpern5}.

Secondly, the alternation depth $D$ and the variable number per
alternation $V$  
are not the ``QBF-analogous'' of \Km{}'s modal depth  and
variable number respectively, as both the latter
values for the resulting modal formulae grow as $O(D\cdot V)$.%
\footnote{As we have already noticed \cite{Horrocks-IGPL}, 
a better ``QBF-analogous'' of the modal depth is 
the total number of universally quantified variables $U$ 
($U = V\cdot \lfloor D/2\rfloor$ in our case). In fact,
 like modal \Km{} with bounded depth, 
the class of QBF formulae with bounded $U$ is only complete in NP, as it is possible to
``guess'' a tree-like witness with  $O(U\cdot 2^U)$ nodes.
}
In fact,  QBF formulae with bounded alternation
 depth $D$ and  
 unbounded  number of variables per
alternation $V$ give rise to
modal formulae  of both unbounded depth and
unbounded number of variables. 


Finally,  the ``$\Sigma_D^P$ vs. NP'' issue of 
\citeauthor{massacci_TANCS99}~\citeyear{massacci_TANCS99} is not a matter of generators,
but rather a matter of how such generators are used, and of how
results are organized and presented.  
In fact, so far  random \mcnf{} testbeds have always been organized 
by fixing all the parameters except $L$ (modal depth $d$ included!) 
and making $L$ vary. 
This choice,  whose goal is  to produce  data plots covering
the satisfiability 
transition area, is what 
causes the testbed formulae to be ``stuck at NP''.
To avoid this fact, one  may want to make $d$ vary and to fix all
the other parameters,
as \Km{} satisfiability  with unbounded  depth
   and bounded number of propositional variables is PSPACE-complete
   \cite{halpern5}. 

\subsection{Asymptotic Behavior}\new{2,3}{section added}
\label{asymptotic_sec}

\noindent
\citeauthor{achlioptas1}~\citeyear{achlioptas1} 
presented a study on the {\em asymptotic behavior} of random CSP
problems.
They showed that, for most well-known random
generation models (which did not reveal flaws in empirical tests)
the probability that problems are trivially unsatisfiable tends to 1
with $N\longmapsto \infty$, $N$ being the number of variables. 
\citeauthor{gent4}~\citeyear{gent4} 
lately explained this discrepancy between theoretical and empirical
results by showing that 
the above phenomenon happens with significant probability only for
values of $N$ which are out of  the reach of current  CSP solvers. 

The problem 
is due to the possible presence of (implicit) {\em unary constraints} causing some variable's value 
to be inadmissible. % (``{\em flawed}'').  
If this occurs with 
some non-zero probability, then with non-zero probability
some variable may have all its values
inadmissible. This causes
a ``local'' inconsistency of the whole problem, which is very easily
revealed by the solver. 
When $N\longmapsto\infty$, the probability of not having such
situation tends to zero. 
Analogous problems have been revealed with random SAT problems generated with
 the constant probability generation model, as 
unary clauses are generated with non-zero probability
 \cite{mitchell1},
and with random QBF problems, as implicit unit clauses, ---i.e., clauses
 containing only one existential variable---
are generated with non-zero probability \cite{gent3}. 
For the random k-SAT model,  $k\ge 2$, such problem does not occur
 \cite{friedgut1,achlioptas1}. 

\smallskip

Our generation model is far more complicated to analyze than the models above. 
First, \mcnf{} formulas have a much more complicated
structure than random SAT, CSP and QBF formulas, involving a much wider number of
parameters. 
Second, unlike with the models discussed above, the 
(constraints described by)  \mcnf{} clauses  are not picked in a {\em
  uniform} way, as  
the probability of generating a given \mcnf{} atom $\Box_r \phi$ 
varies strongly with its depth and shape, and it is typically much
smaller than that of generating a propositional atom $A_i$.% 
\footnote{Again, we recall that the number of possible distinct \mcnf{} atoms increases 
hyper-exponentially with the modal depth $d$ \cite{Horrocks-IGPL}.}
Thus, developing a formal probabilistic analysis for the asymptotic
behavior of our model is out of the reach (and of the scope) of this
paper. However, we provide here some heuristic considerations. 
%We distinguish two cases.

The simplest case is when we do not allow the generation of unary clauses
at top level, that is, when {\tt C = [[0,...],...]}, so that 
 we do not have explicit unary constraints.
We may still have {\em implicit} unary constraints like, e.g., 
$(A_i\vee\Box_r\phi)\wedge (A_i\vee\neg\Box_r\phi)$ or 
$(\Box_i\psi\vee\Box_r\phi)\wedge
(\Box_i\psi\vee\neg\Box_r\phi)$. Anyway, a simple heuristic
consideration suggests  that, 
given the big numbers of distinct \mcnf{} modal
atoms which may potentially be  generated,  
such situations are  more unlikely than that of having implicit unit constraints like
$(A_i\vee A_j)\wedge (A_i\vee\neg A_j)$ in the standard 2-SAT model,
which is free from the asymptotic local inconsistency problem.~%


A more critical case is when we allow for the generation of unary clauses
at top level, that is, when {\tt C = [[x,...],...]}, ${\tt x}>0$. 
In this case
we can generate unary clauses, and thus  local
inconsistencies, with  non-zero probability. 
Thus, a simple way to avoid this problem is to restrict the values of
$C$ so that not to  
allow unary top-level clauses, that is, to always set {\tt C =
  [[0,...],...]}.   
Notice, however, that this hardly becomes a problem in practice if we respect
the condition described in 
Sections~\ref{p_subsec} and ~\ref{shape_subsec} of avoiding purely
propositional top-level clauses (that is, always set {\tt p =
  [[...,0],...]}). In fact, given the big numbers of distinct \mcnf{} modal
atoms which may potentially be  generated, the probability of having two
contradictory modal unit clauses $\Box_r\phi$, $\neg\Box_r\phi$
within the same formula becomes quickly negligible even with small depths. 

Notice that here we have intentionally not considered ``modal'' implicit unary
constraints  like, e.g.,  $(A_i\vee\phi)\wedge
(A_i\vee\psi)$,  $\phi$ and $\psi$ being
mutually  inconsistent modal literals (e.g., $\phi=\Box_r \vi_1$,
$\psi=\neg\Box_r (\vi_1\vee \vi_2)$). In fact,  detecting
such inconsistencies 
requires investigating recursively the modal successors, and therefore it
is not ``trivial''.  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Conclusions and future work
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Conclusions and Future Work}
\label{conclusion_sec}


As shown by the test sets above our new method, in its basic form,
 allows us to generate a
wider variety of problems covering more of the input space.
We can better-tune the difficulty of problems for various parameter values,
including the first reasonable test sets for maximum modal depths of $2$
and $3$.  
We can produce interesting scaling dimensions, varying more than just the
number of propositional variables $\nvar$.
For example, we can now vary the propositional probability $p$ or the size
of clauses $C$ to vary the difficulty of interesting problems.
As neither $p$ nor $C$ are restricted to integral values, we have
extremely fine control over the difficulty of test sets.
Thus we can create more interesting test sets where the
satisfiable/unsatisfiable transition is explorable with current decision
procedures. 

We have drastically reduced the influence of trivial unsatisfiability,
which flawed the previous \mcnf methodologies when $p>0$.
We retain the desirable features of the previous \mcnf methodo\-logies.
Our test sets are easy to reproduce and are not too large.

\smallskip
In our full methodology we have introduced 
the possibility of 
%a very large number of parameters. This allows for 
shaping  the
distribution of both the size and the propositional/modal rate of the
clauses. This can be done at each level of modal depth. 
This allows for  generating a much wider variety of problems, covering
in principle the whole input space. For instance, we have produced a
full test set with  $d=5$ and $N=5$ (Figure~\ref{results-variable}). 

We have not moved closer to application data, as there are no
significant direct applications of modal decision procedures and thus no guidance
for the sorts of inputs that would be close to application inputs.
In any case, we believe we have moved closer than ever to the possibility 
of approximating given classes of input formulae. 

There is still much work to be done using our generation methodology.
We can produce more test sets and try these test sets out on various modal
decision procedures.
We may also want to uncover parameter settings where the full generality of our
generation method is needed to produce reasonable test sets.

\section*{Acknowledgments}

We would like to thank  Thomas Eiter and the three
anonymous reviewers for their valuable comments and helpful
suggestions which greatly improved  the quality of the paper.
The second author is supported by a {\sc MIUR COFIN02} project, code
    {\sf 2002097822\_003}, and 
by the  {\sc Calculemus!} {\sc IHP-RTN}
 EC project, contract code {\sf HPRN-CT-2000-00102}, and has thus
 benefited of 
 the financial contribution of  the Commission  through the IHP 
 programme. 



\section*{Appendix A: Fully-detailed Proof of Theorem \ref{shape_theo}}
\setcounter{section}{6}
%%%%%%%%%%%%%%%%%%%% THEOREM %%%%%%%%%%%%%%
\begin{theorem}
Let rnd\_\mcnf{} be a purely random generator as in Figure~\ref{randgen_fig}.
%
Let $\vi$ be a sorted \mcnf{} formula of depth $d$ and with $L$
top-level clauses
built on all the propositional atoms in $\{A_1,...A_N\}$ 
and on all the modal boxes in $\{\Box_1,...\Box_m\}$,
 which has no repeated clause at top level and
no repeated atoms inside any
clause at any level.
%
Let $C$ and $p$ be built from $\vi$  so that to verify points $(a)$ and
$(b)$ of Section~\ref{generality_sec}. 
%
Let $C'$ and $p'$ be obtained from $C$ and $p$ respectively 
by substituting some zero-values with some non-zero values.
%
Then we have:
\begin{renumerate}
\item 
rnd\_\mcnf{}(d,m,L,N,p,C) returns $\vi$ with some non-zero
probability ${\cal P\/}$; 
\item 
rnd\_\mcnf{}(d,m,L,N,p',C') returns $\vi$ with some non-zero
probability ${\cal P'\/}\le{\cal P\/}$.
\end{renumerate}
%\label{shape_theo}
\end{theorem}
 

%%%%%%%%%%%%%%%%%%%% PROOF %%%%%%%%%%%%%%
\noindent
\begin{proof}
\noindent
The proof works by induction on the structure of $\vi$. 
First, we prove that:
\begin{enumerate}
\item 
every propositional atom  occurring in $\vi$ at some depth $i$ 
is returned with the same non-zero probability ${\cal P\/}_1$ by 
both {\em rnd\_atom(0,m,N,p,C)\/} and {\em rnd\_atom(0,m,N,p',C')\/};
\item 
every modal atom $\Box_v Cl$ occurring in $\vi$ at some depth $i$ 
is returned with some non-zero probability ${\cal P\/}_2$ by 
{\em rnd\_atom(d-i,m,N,p,C)\/}, and 
is returned with some non-zero probability ${\cal P'\/}_2\le {\cal P\/}_2$ by 
{\em rnd\_atom(d-i,m,N,p',C')\/};
\item 
every clause $Cl$ occurring in $\vi$ at some depth $i$ 
is returned with some non-zero probability ${\cal P\/}_3$ by 
{\em rnd\_clause(d-i,m,N,p,C)\/}, and
is returned with some non-zero probability ${\cal P'\/}_3\le {\cal P\/}_3$ by 
{\em rnd\_clause(d-i,m,N,p',C')\/}.
\end{enumerate}

\noindent
From point 3. we have that every top level clause $Cl_k$ 
is  returned by {\em rnd\_clause(d,m,N,p,C)\/} 
and {\em rnd\_clause(d,m,N,p',C')\/} with some probabilities
 ${\cal P\/}_{k}$ and ${\cal P'\/}_{k}$ respectively, being
${\cal P'\/}_{k} \le {\cal P\/}_{k}$.
As $\vi$ has no repeated clause, 
recalling  a property of probabilities we have:
\begin{eqnarray}
{\cal P}\ & = &
\begin{array}{l} 
{\cal P\/}_{1} \cdot \\
%
({\cal P\/}_{2}+
{\cal P\/}_{1} {\cal P\/}_{2} + 
 {\cal P\/}_{1}^2 {\cal P\/}_{2} + \ldots
) \cdot \\
({\cal P\/}_{3}+
({\cal P\/}_{1}+{\cal P\/}_{2}) {\cal P\/}_{3} + 
 ({\cal P\/}_{1}+{\cal P\/}_{2})^2 {\cal P\/}_{3} + \ldots
) \cdot \\
\ldots \\
 ({\cal P\/}_{L}+
 ({\cal P\/}_{1}+\ldots+{\cal P\/}_{L-1}) {\cal P\/}_{L} + 
  ({\cal P\/}_{1}+\ldots+{\cal P\/}_{L-1})^2 {\cal P\/}_{L} + \ldots) \\
\end{array} \\
\label{prob1_equ}
 & = & \prod_{k=1}^{L}  \left (
\sum_{i=0}^{\infty} 
(\sum_{s=1}^{k-1}{\cal P\/}_{s})^i \cdot {\cal P\/}_{k} \right )\\
%
& = & \prod_{k=1}^{L} 
\frac{{\cal P\/}_{k}}{1-\sum_{s=1}^{k-1}{\cal P\/}_{s}}.
\label{prob_equ}
\end{eqnarray}

\noindent
Notice that (\ref{prob1_equ}) is strictly monotonic in all its components.
Thus, ${\cal P'\/}\le {\cal P\/}$. 

Now we need to prove points 1, 2 and 3. 
% \begin{eqnarray}
% {\cal P}\ = 
% {\cal P\/}_{1} \cdot 
% ({\cal P\/}_{2}+
%  (1-{\cal P\/}_{1}) {\cal P\/}_{2} + 
%  (1-{\cal P\/}_{1})^2 {\cal P\/}_{2} + \ldots
% ) \cdot \ldots \\
%  = \prod_{k=1}^{L}  \left (
% \sum_{i=0}^{\infty} 
% (1-\sum_{s=1}^{k-1}{\cal P\/}_{s})^i \cdot {\cal P\/}_{k} \right )\\
% %
% = \prod_{k=1}^{L} 
% \frac{{\cal P\/}_{k}}{1-\sum_{s=1}^{k-1}{\cal P\/}_{s}} .
% \end{eqnarray}
%%%%%%%% 3 STEPS: PROOF %%%%%%%%%%%%
\begin{enumerate}

%%%%%%%%%%%% STEP 1
\item 
Let $A_k$ be a propositional atom in $\{A_1,...,A_N\}$ occurring in
$\vi$ at depth $i$, for some $i\le d$.  
Then both {\em rnd\_atom(0,m,N,p,C)\/} and {\em rnd\_atom(0,m,N,p',C')\/}
invoke {\em rnd\_propositional\_atom(N)\/},
which returns $A_k$ with probability ${\cal P\/}_1 = 1/N$.

%%%%%%%%%%%% STEP 2
\item
Let  $\Box_v Cl$ be a boxed clause occurring in
$\vi$ at depth $i$, for some $i< d$ and  $v\le m$.~%
Then the clause $Cl$ occurs  in
$\vi$ at depth $i+1$.
(Notice that $i< d$ instead of  $i\le d$: $\Box_v Cl$ 
cannot occur in $\vi$ at depth $d$, because $d$ is the maximum depth of $\vi$.)

\begin{renumerate}
\item %%%%%%%%%%%% STEP 2 (i)
By inductive hypothesis, 
it follows from point 3. that $Cl$ is returned with some non-zero
probability ${\cal P\/}_3$ by 
{\em rnd\_clause(d-i-1,m,N,p,C)\/}.
As $i<d$, {\em rnd\_atom(d-i,m,N,p,C)\/} invokes 
{\em rand\_box(m) $\cdot$ rand\_clause(d-i-1,m,N,p,C)\/}, which returns  $\Box_v Cl$
 with the non-zero probability  ${\cal P\/}_2 = 1/m \cdot {\cal P\/}_3$.

\item %%%%%%%%%%%% STEP 2 (ii)
By inductive hypothesis, 
it follows from point 3. that $Cl$ is returned with some non-zero
probability ${\cal P'\/}_3\le {\cal P\/}_3$ by 
{\em rnd\_clause(d-i-1,m,N,p',C')\/}.
{\em rnd\_atom(d-i,m,N,p',C')\/} invokes 
{\em rand\_box(m) $\cdot$ rand\_clause(d-i-1,m,N,p',C')\/}, which returns  $\Box_v Cl$
 with the non-zero probability  ${\cal P'\/}_2 = 1/m \cdot {\cal P'\/}_3$.
Thus, ${\cal P'\/}_2 \le {\cal P\/}_2$.
\end{renumerate}

\item %%%%%% STEP 3
Let $Cl$ be a clause with length $j$ and $r\le j$ propositional literals, 
which occurs in $\vi$ at depth $i$, for some $i\le d$.
As $\vi$ is sorted, $Cl$ is represented as 
$Sort(\psi_1\vee ... \vee \psi_r\vee \phi_1 \vee ... \vee \phi_{j-r})$, where
 $\psi_1, ..., \psi_r$ denote propositional literals 
and $\phi_1, ..., \phi_{j-r}$ denote modal literals. 
\begin{renumerate}

\item %%%%%%  STEP 3 (i)
By inductive hypothesis, it follows from point 1. that each propositional literal $\psi_k$ 
is returned with some non-zero probability $0.5\cdot {\cal P\/}_{1,k}$ by 
{\em rnd\_sign() $\cdot$ rnd\_atom(0,m,N,p,C)\/}, and 
it follows from point 2. that each modal literals $\phi_l$ 
is returned with the non-zero probability $0.5\cdot {\cal P\/}_{2,l}$ by 
{\em rnd\_sign() $\cdot$ rnd\_atom(d-i,m,N,p,C)\/}. 

By construction of $C$, the $j$-th element of the $i$-th sublist in $C$ is
non-zero; thus, $j$ is returned with some non-zero probability ${\cal P\/}_j$ by {\em rnd\_length(d-i,C)}.

By construction of $p$, the $r+1$-the element of the $j$-th sub-sublist of the $i$-th sublist in $p$ is
non-zero; thus, $r$ is returned with some non-zero probability ${\cal
P\/}_{r|j}$ by {\em rnd\_propnum(d,p,j)\/}.% 
\footnote{
Notice that ${\cal P\/}_{r|j}$ is a conditioned probability,
that is, the probability of having $r$ propositional literal provided
the clause has $j$ literals. This matches the fact that $j$ is
an input in {\em rnd\_propnum(d,p,j)\/}.
}

% \todo{Find an explicit representation of ${\cal P\/}_3$ in terms of 
% ${\cal P\/}_{1,k}, {\cal P\/}_{2,l}, {\cal P\/}_j,
% {\cal P\/}_{r|j}$ (or show it is monotonic).
% Ask some math guy. If not, recall file new\_testing.tex.3} 
%
Similarly to (\ref{prob_equ}), $\vi$ has
no repeated atoms inside any clause,
so that $Cl$ is returned by
{\em rnd\_clause(d-i,m,N,p,C)\/} with the non-zero probability 
\begin{equation}
{\cal P\/}_3\ = \ 
{\cal P\/}_j \cdot
{\cal P\/}_{r|j} \cdot
(0.5)^j \cdot
\prod_{k=1}^{r} \frac{{\cal P\/}_{1,k}}{1-\sum_{s=1}^{k-1}{\cal P\/}_{1,s}} \cdot
\prod_{l=1}^{j-r} \frac{{\cal P\/}_{2,l}}{1-\sum_{t=1}^{l-1}{\cal P\/}_{2,t}}.
\label{p3_equ}
\end{equation}
As with (\ref{prob_equ}), the expression on the right in (\ref{p3_equ}) is strictly
monotonic in all its terms 
${\cal P\/}_j$, ${\cal P\/}_{r|j}$, ${\cal P\/}_{1,k}$ 's, ${\cal
P\/}_{2,l}$ 's within the domain of definition. 

\item %%%%%%  STEP 3 (ii)
By inductive hypothesis, it follows from point 1. that each propositional literal $\psi_k$ 
is returned with some non-zero probability 
$0.5\cdot {\cal P'\/}_{1,k}\le 0.5\cdot {\cal P\/}_{1,k}$ by 
{\em rnd\_sign() $\cdot$ rnd\_atom(0,m,N,p',C')\/}, and 
it follows from point 2. that each modal literals $\phi_l$ 
is returned with some non-zero probability 
$0.5\cdot {\cal P'\/}_{2,l} \le 0.5\cdot {\cal P\/}_{2,l}$ by 
{\em rnd\_sign() $\cdot$ rnd\_atom(d-i,m,N,p',C')\/}. 

By construction of $C$ and $C'$, the $j$-th element of the $i$-th sublist in $C'$ is
non-zero; thus, $j$ is returned with some non-zero probability ${\cal
P'\/}_j$ by {\em rnd\_length(d-i,C')}.
By construction of $C'$ from $C$, ${\cal P'\/}_j\le {\cal P\/}_j$.

By construction of $p$ and $p'$, the $r+1$-the element of the $j$-th sub-sublist of the $i$-th sublist in $p$ is
non-zero; thus, $r$ is returned with some non-zero probability ${\cal
P'\/}_{r|j}$ by {\em rnd\_propnum(d,p,j)\/}.  
By construction of $p'$ from $p$, ${\cal P'\/}_{r|j}\le {\cal P\/}_{r|j}$.

As $\vi$ has
no repeated atoms inside any clause,
it follows that $Cl$ is returned by
{\em rnd\_clause(d-i,m,N,p',C')\/} with the non-zero probability 
\begin{equation}
{\cal P'\/}_3\ = \ 
{\cal P'\/}_j \cdot
{\cal P'\/}_{r|j} \cdot
(0.5)^j \cdot
\prod_{k=1}^{r} \frac{{\cal P'\/}_{1,k}}{1-\sum_{s=1}^{k-1}{\cal P'\/}_{1,s}} \cdot
\prod_{l=1}^{j-r} \frac{{\cal P'\/}_{2,l}}{1-\sum_{t=1}^{l-1}{\cal P'\/}_{2,t}}.
\label{p3'_equ}
\end{equation}
Because of the strict monotonicity of (\ref{p3_equ}) and
(\ref{p3'_equ}), we have that ${\cal P'\/}_3 \le {\cal P\/}_3$.
\end{renumerate}
\end{enumerate}
\end{proof}





\vskip 0.2in
%\bibliography{ih,rs,pfps}
%\bibliographystyle{theapa}

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Achlioptas, Kirousis, Kranakis, Krizanc, Molloy,\ \BBA\
  Stamatiou}{Achlioptas et~al.}{1997}]{achlioptas1}
Achlioptas, D., Kirousis, L.~M., Kranakis, E., Krizanc, D., Molloy, M. S.~O.,
  \BBA\ Stamatiou, Y.~C. \BBOP1997\BBCP.
\newblock \BBOQ Random constraint satisfaction: {A} more accurate picture\BBCQ\
\newblock In Smolka, G.\BED, {\Bem Principles and Practice of Constraint
  Programming}, \lowercase{\BVOL}\ 1330 of {\Bem Lecture Notes in Computer Science},
  \BPGS\ 107--120, Berlin. Springer.

\bibitem[\protect\BCAY{Beckert\ \BBA\ Gor{\'e}}{Beckert\ \BBA\
  Gor{\'e}}{1997}]{Beckert97a}
Beckert, B.\BBACOMMA\  \BBA\ Gor{\'e}, R. \BBOP1997\BBCP.
\newblock \BBOQ Free variable tableaux for propositional modal logics\BBCQ\
\newblock In {\Bem Automated Reasoning with Analytic Tableaux and Related
  Methods: International Conference Tableaux'97}, \lowercase{\BVOL}\ 1227 of
  {\Bem Lecture Notes in Artificial Intelligence}, \BPGS\ 91--106, Berlin. Springer.

\bibitem[\protect\BCAY{Cadoli, Giovanardi,\ \BBA\ Schaerf}{Cadoli
  et~al.}{1998}]{cadoli2}
Cadoli, M., Giovanardi, A., \BBA\ Schaerf, M. \BBOP1998\BBCP.
\newblock \BBOQ An algorithm to evaluate quantified {Boolean} formulae\BBCQ\
\newblock In {\Bem Proceedings of the 15th National Conference on Artificial
  Intelligence ({AAAI}-98)}, \BPGS\ 262--267, Menlo Park, CA. AAAI Press.

\bibitem[\protect\BCAY{Friedgut}{Friedgut}{1998}]{friedgut1}
Friedgut, E. \BBOP1998\BBCP.
\newblock \BBOQ Sharp thresholds of graph properties, and the {k-sat}
  problem\BBCQ\
\newblock {\Bem Journal of the American Mathematical Society}, {\Bem 12\/}(4),
  1017--1054.

\bibitem[\protect\BCAY{Garey\ \BBA\ Johnson}{Garey\ \BBA\
  Johnson}{1979}]{garey1}
Garey, M.~R.\BBACOMMA\  \BBA\ Johnson, D.~S. \BBOP1979\BBCP.
\newblock {\Bem {C}omputers and {I}ntractability: A Guide to the Theory of
  {NP}-Completeness}.
\newblock W. H. Freeman, New York.

\bibitem[\protect\BCAY{Gent, MacIntyre, Prosser, Smith,\ \BBA\ Walsh}{Gent
  et~al.}{2001}]{gent4}
Gent, I.~P., MacIntyre, E., Prosser, P., Smith, B.~M., \BBA\ Walsh, T.
  \BBOP2001\BBCP.
\newblock \BBOQ Random constraint satisfaction: Flaws and structure\BBCQ\
\newblock {\Bem Journal of Constraints}, {\Bem 6\/}(4), 345--372.

\bibitem[\protect\BCAY{Gent\ \BBA\ Walsh}{Gent\ \BBA\ Walsh}{1999}]{gent3}
Gent, I.~P.\BBACOMMA\  \BBA\ Walsh, T. \BBOP1999\BBCP.
\newblock \BBOQ Beyond {NP}: The {QSAT} phase transition\BBCQ\
\newblock In {\Bem Proceedings of the Sixteenth National Conference on
  Artificial Intelligence and the Eleventh Innovative Applications of
  Artificial Intelligence Conference (AAAI-99)}, \BPGS\ 648--653, Menlo Park,
  CA. AAAI Press.

\bibitem[\protect\BCAY{Giunchiglia, Giunchiglia, Sebastiani,\ \BBA\
  Tacchella}{Giunchiglia et~al.}{2000}]{giunchiglia108}
Giunchiglia, E., Giunchiglia, F., Sebastiani, R., \BBA\ Tacchella, A.
  \BBOP2000\BBCP.
\newblock \BBOQ {SAT} vs. {T}ranslation based decision procedures for modal
  logics: a comparative evaluation\BBCQ\
\newblock {\Bem Journal of Applied Non-Classical Logics}, {\Bem 10\/}(2),
  145--172.

\bibitem[\protect\BCAY{Giunchiglia, Giunchiglia,\ \BBA\ Tacchella}{Giunchiglia
  et~al.}{2002}]{giunchiglia-sat2000}
Giunchiglia, E., Giunchiglia, F., \BBA\ Tacchella, A. \BBOP2002\BBCP.
\newblock \BBOQ {SAT} based decision procedures for classical modal
  logics\BBCQ\
\newblock {\Bem Journal of Automated Reasoning}, {\Bem 28}, 143--171.

\bibitem[\protect\BCAY{Giunchiglia\ \BBA\ Sebastiani}{Giunchiglia\ \BBA\
  Sebastiani}{1996}]{giunchiglia93}
Giunchiglia, F.\BBACOMMA\  \BBA\ Sebastiani, R. \BBOP1996\BBCP.
\newblock \BBOQ Building decision procedures for modal logics from
  propositional decision procedures - the case study of modal {K}\BBCQ\
\newblock In {\Bem Proceedings of the Thirteenth Conference on Automated
  Deduction}, \lowercase{\BVOL}\ 1104 of {\Bem Lecture Notes in Artificial
  Intelligence}, \BPGS\ 583--597, Berlin. Springer.

\bibitem[\protect\BCAY{Giunchiglia\ \BBA\ Sebastiani}{Giunchiglia\ \BBA\
  Sebastiani}{2000}]{giunchiglia97}
Giunchiglia, F.\BBACOMMA\  \BBA\ Sebastiani, R. \BBOP2000\BBCP.
\newblock \BBOQ Building decision procedures for modal logics from
  propositional decision procedures - the case study of modal {K}(m)\BBCQ\
\newblock {\Bem Information and Computation}, {\Bem 162\/}(1/2), 158--178.

\bibitem[\protect\BCAY{Haarslev\ \BBA\ M{\"o}ller}{Haarslev\ \BBA\
  M{\"o}ller}{2001}]{haarslev1}
Haarslev, V.\BBACOMMA\  \BBA\ M{\"o}ller, R. \BBOP2001\BBCP.
\newblock \BBOQ {RACER} system description\BBCQ\
\newblock In {\Bem Proceedings of the International Joint Conference on
  Automated Reasoning, IJCAR'2001}, \lowercase{\BVOL}\ 2083 of {\Bem Lecture
  Notes in Computer Science}, \BPGS\ 701--705, Siena, Italy. Springer.

\bibitem[\protect\BCAY{Halpern}{Halpern}{1995}]{halpern5}
Halpern, J.~Y. \BBOP1995\BBCP.
\newblock \BBOQ The effect of bounding the number of primitive propositions and
  the depth of nesting on the complexity of modal logic\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 75\/}(3), 361--372.

\bibitem[\protect\BCAY{Halpern\ \BBA\ Moses}{Halpern\ \BBA\
  Moses}{1992}]{halpern4}
Halpern, J.~Y.\BBACOMMA\  \BBA\ Moses, Y. \BBOP1992\BBCP.
\newblock \BBOQ A guide to the completeness and complexity for modal logics of
  knowledge and belief\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 54\/}(3), 319--379.

\bibitem[\protect\BCAY{Heguiabehere\ \BBA\ de~Rijke}{Heguiabehere\ \BBA\
  de~Rijke}{2001}]{heguiabehere1}
Heguiabehere, J.\BBACOMMA\  \BBA\ de~Rijke, M. \BBOP2001\BBCP.
\newblock \BBOQ The random modal {QBF} test set\BBCQ\
\newblock In {\Bem IJCAR'2001 Workshop on Issues in the Design and Experimental
  Evaluation of System for Modal and Temporal Logics}, \BPGS\ 58--67.

\bibitem[\protect\BCAY{Heuerding, J{\"a}ger, Schwendimann,\ \BBA\
  Seyfreid}{Heuerding et~al.}{1995}]{Heuerding95a}
Heuerding, A., J{\"a}ger, G., Schwendimann, S., \BBA\ Seyfreid, M.
  \BBOP1995\BBCP.
\newblock \BBOQ Propositional logics on the computer\BBCQ\
\newblock In Baumgartner, P., H{\"a}hnle, R., \BBA\ Posegga, J.\BEDS, {\Bem
  Automated Reasoning with Analytic Tableaux and Related Methods: International
  Conference Tableaux'95}, \lowercase{\BVOL}\ 918 of {\Bem Lecture Notes in
  Artificial Intelligence}, \BPGS\ 310--323, Berlin. Springer.

\bibitem[\protect\BCAY{Heuerding\ \BBA\ Schwendimann}{Heuerding\ \BBA\
  Schwendimann}{1996}]{heuerding2}
Heuerding, A.\BBACOMMA\  \BBA\ Schwendimann, S. \BBOP1996\BBCP.
\newblock \BBOQ A benchmark method for the propositional modal logics {K},
  {KT}, {S4}.\BBCQ\
\newblock \BTR\ IAM-96-015, University of Bern, Switzerland.

\bibitem[\protect\BCAY{Horrocks}{Horrocks}{1998}]{Horrocks98c}
Horrocks, I. \BBOP1998\BBCP.
\newblock \BBOQ Using an expressive description logic: {FaCT} or fiction?\BBCQ\
\newblock In Cohn, A.~G., Schubert, L., \BBA\ Shapiro, S.~C.\BEDS, {\Bem
  Principles of Knowledge Representation and Reasoning: Proceedings of the
  Sixth International Conference (KR'98)}, \BPGS\ 636--647. Morgan Kaufmann
  Publishers, San Francisco, California.

\bibitem[\protect\BCAY{Horrocks\ \BBA\ Patel-Schneider}{Horrocks\ \BBA\
  Patel-Schneider}{2002}]{Horrocks99f}
Horrocks, I.\BBACOMMA\  \BBA\ Patel-Schneider, P.~F. \BBOP2002\BBCP.
\newblock \BBOQ Evaluating optimised decision procedures for propositional
  modal $\mathbf{K}_{(\mathbf{m})}$ satisfiability\BBCQ\
\newblock {\Bem Journal of Automated Reasoning}, {\Bem 28\/}(2), 173--204.

\bibitem[\protect\BCAY{Horrocks, Patel-Schneider,\ \BBA\ Sebastiani}{Horrocks
  et~al.}{2000}]{Horrocks-IGPL}
Horrocks, I., Patel-Schneider, P.~F., \BBA\ Sebastiani, R. \BBOP2000\BBCP.
\newblock \BBOQ An analysis of empirical testing for modal decision
  procedures\BBCQ\
\newblock {\Bem Logic Journal of the IGPL}, {\Bem 8\/}(3), 293--323.

\bibitem[\protect\BCAY{Hustadt\ \BBA\ Schmidt}{Hustadt\ \BBA\
  Schmidt}{1999}]{hustadt3}
Hustadt, U.\BBACOMMA\  \BBA\ Schmidt, R.~A. \BBOP1999\BBCP.
\newblock \BBOQ An empirical analysis of modal theorem provers\BBCQ\
\newblock {\Bem Journal of Applied Non-Classical Logics}, {\Bem 9\/}(4),
  479--522.

\bibitem[\protect\BCAY{Hustadt, Schmidt,\ \BBA\ Weidenbach}{Hustadt
  et~al.}{1999}]{Hustadt99-mspass}
Hustadt, U., Schmidt, R.~A., \BBA\ Weidenbach, C. \BBOP1999\BBCP.
\newblock \BBOQ {MSPASS}: Subsumption testing with {SPASS}\BBCQ\
\newblock In Lambrix, P., Borgida, A., Lenzerini, M., M{\"o}ller, R., \BBA\
  Patel-Schneider, P.\BEDS, {\Bem Proceedings of the 1999 International
  Workshop on Description Logics (DL'99).}, \BPGS\ 136--137.

\bibitem[\protect\BCAY{Massacci}{Massacci}{1999}]{massacci_TANCS99}
Massacci, F. \BBOP1999\BBCP.
\newblock \BBOQ Design and results of {Tableaux}-99 non-classical (modal)
  system competition\BBCQ\
\newblock In {\Bem Automated Reasoning with Analytic Tableaux and Related
  Methods: International Conference Tableaux'99}, \lowercase{\BVOL}\ 1617 of
  {\Bem Lecture Notes in Artificial Intelligence}, \BPGS\ 14--18, Berlin. Springer.

\bibitem[\protect\BCAY{Mitchell, Selman,\ \BBA\ Levesque}{Mitchell
  et~al.}{1992}]{mitchell1}
Mitchell, D., Selman, B., \BBA\ Levesque, H. \BBOP1992\BBCP.
\newblock \BBOQ Hard and easy distributions of {SAT} problems\BBCQ\
\newblock In {\Bem Proceedings of the Tenth National Conference on Artificial
  Intelligence}, \BPGS\ 459--465, San Jose, California. American Association
  for Artificial Intelligence.

\bibitem[\protect\BCAY{Patel-Schneider}{Patel-Schneider}{1998}]{patel-schneide%
r:dlp-description}
Patel-Schneider, P.~F. \BBOP1998\BBCP.
\newblock \BBOQ {DLP} system description\BBCQ\
\newblock In Franconi, E., Giacomo, G.~D., MacGregor, R.~M., Nutt, W., Welty,
  C.~A., \BBA\ Sebastiani, F.\BEDS, {\Bem Collected Papers from the
  International Description Logics Workshop (DL'98)}, \BPGS\ 87--89.
\newblock Available as CEUR-WS/Vol-11 from {\sf
  http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS}.

\bibitem[\protect\BCAY{Patel-Schneider\ \BBA\ Sebastiani}{Patel-Schneider\
  \BBA\ Sebastiani}{2001}]{pfps-ijcar2001}
Patel-Schneider, P.~F.\BBACOMMA\  \BBA\ Sebastiani, R. \BBOP2001\BBCP.
\newblock \BBOQ A new system and methodology for generating random modal
  formulae\BBCQ\
\newblock In {\Bem Proceedings of the International Joint Conference on
  Automated Reasoning, IJCAR'2001}, \lowercase{\BVOL}\ 2083 of {\Bem Lecture
  Notes in Computer Science}, \BPGS\ 464--468, Siena, Italy. Springer.

\bibitem[\protect\BCAY{Pitt\ \BBA\ Cunningham}{Pitt\ \BBA\
  Cunningham}{1996}]{Pitt96a}
Pitt, J.\BBACOMMA\  \BBA\ Cunningham, J. \BBOP1996\BBCP.
\newblock \BBOQ Distributed modal theorem proving with {KE}\BBCQ\
\newblock In Minglioli, P., Moscato, U., Mindici, D., \BBA\ Ornaghi, M.\BEDS,
  {\Bem Automated Reasoning with Analytic Tableaux and Related Methods:
  International Conference Tableaux'96}, \lowercase{\BVOL}\ 1071 of {\Bem Lecture
  Notes in Artificial Intelligence}, \BPGS\ 160--176, Berlin. Springer.

\bibitem[\protect\BCAY{Tacchella}{Tacchella}{1999}]{Tacchella99a}
Tacchella, A. \BBOP1999\BBCP.
\newblock \BBOQ {*SAT} system description\BBCQ\
\newblock In Lambrix, P., Borgida, A., Lenzerini, M., M{\"o}ller, R., \BBA\
  Patel-Schneider, P.\BEDS, {\Bem Proceedings of the 1999 International
  Workshop on Description Logics (DL'99).}, \BPGS\ 142--144.

\end{thebibliography}



\end{document}





