Models Enumeration in SAT-Based Itemset Mining
Said Jabbour and Lakhdar Sais and Yakoub Salhi
Frequent itemset mining is an essential part of data analysis and data mining. Recent works propose interesting SAT-based encodings for the problem of discovering frequent itemsets. Our aim in this work is to define strategies for adapting SAT solvers to such encodings in order to improve models enumeration. In this context, we deeply study the effects of restart, branching heuristics and clauses learning. We then conduct an experimental evaluation on SAT-Based itemset mining instances to show how SAT solvers can be adapted to obtain an efficient SAT model enumerator.
AllModelsV3.tex

%%%%%%%%%%%%%%%%%%%%%%% file typeinst.tex %%%%%%%%%%%%%%%%%%%%%%%%%
%
% This is the LaTeX source for the instructions to authors using
% the LaTeX document class 'llncs.cls' for contributions to
% the Lecture Notes in Computer Sciences series.
% http://www.springer.com/lncs       Springer Heidelberg 2006/05/04
%
% It may be used as a template for your own input - copy it
% to a new faile with a new name and use it as the basis
% for your article.
%
% NB: the document class 'llncs' has its own and detailed documentation, see
% ftp://fftp.springer.de/data/pubftp/pub/tex/latex/llncs/latex2e/llncsdoc.pdf
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\documentclass[a4paper]{llncs}

\usepackage{etex}
\usepackage{times}
\usepackage{graphicx}
\usepackage{float,latexsym,url}
\usepackage[ruled,vlined]{algorithm2e}
\usepackage{pstricks-add}
\usepackage{pgf}
\usepackage[utf8]{inputenc}
\usepackage{colortbl}

\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{latexsym,xspace}
\usepackage{graphics,graphicx,float}
\usepackage{times,psfrag}
%\usepackage{auto-pst-pdf}
\usepackage{pstricks-add}
\usepackage{rotate}
\usepackage{epsfig}
\usepackage{subfigure}
\usepackage{textcomp}
\usepackage{tikz}
\usetikzlibrary{arrows,shapes,snakes,automata,backgrounds,petri,shadows}




%\usepackage{graphicx}
%\usepackage{graphics}
\usepackage{latexsym}

%\usepackage{tikz}
%\usepackage{amssymb}
%\usetikzlibrary{arrows}

\usepackage{proof}
%\newtheorem{definition}{Definition}
%\newtheorem{example}{Example}
%\newtheorem{proposition}{Proposition}
%\newtheorem{property}{Property}
\newtheorem{theorm}{Theorem}
%\newtheorem{property}{Property}
%\newtheorem{remark}{Remark}
%\newtheorem{prop}{Proposition}

\usepackage{url}
\urldef{\mailsa}\path|{alfred.hofmann, ursula.barth, ingrid.haas, frank.holzwarth,|
\urldef{\mailsb}\path|anna.kramer, leonie.kunz, christine.reiss, nicole.sator,|
\urldef{\mailsc}\path|erika.siebert-cole, peter.strasser, lncs}@springer.com|    
\newcommand{\keywords}[1]{\par\addvspace\baselineskip
\noindent\keywordname\enspace\ignorespaces#1}


\newcommand{\dpll}{\textsc{dpll}\xspace}
\newcommand{\cdcl}{\textsc{cdcl}\xspace}
\newcommand{\minisat}{\textsc{minisat}\xspace}
\newcommand{\glucose}{\textsc{glucose}\xspace}
\newcommand{\rsat}{\textsc{rsat}\xspace}
\newcommand{\sat}{\textsc{sat}\xspace}
\newcommand{\unsat}{\textsc{unsat}\xspace}
\newcommand{\etal}{\textit{et al.}\xspace}
\newcommand{\vsids}{\textsc{vsids}\xspace}
\newcommand{\phase}{\mathcal{P}}
\newcommand{\intention}{\mathcal{N}}
\newcommand{\core}{\mathcal{C}}
\newcommand{\dist}{\delta}
\newcommand{\var}{\mathcal{V}\_{\Sigma}}
\newcommand{\lit}{\mathcal{L}\_{\Sigma}}
\newcommand{\cnf}{\textsc{cnf}\xspace}
\newcommand{\uip}{\textsc{uip}\xspace}
\newcommand{\formule}{\Sigma}
\newcommand{\I}{\mathcal{I}}
\newcommand{\LBD}{\textsc{LBD}\xspace}
\newcommand{\Random}{\textsc{Random}\xspace}
\newcommand{\CSIDS}{\textsc{CSIDS-D}\xspace}
\newcommand{\FIFO}{\textsc{FIFO}\xspace}
\newcommand{\BTL}{\textsc{BTL}\xspace}
\newcommand{\Undef}{\textsc{PUndef}\xspace}
\newcommand{\PSM}{\textsc{PSM}\xspace}
\newcommand{\Dist}{\textsc{CSIDS-S}\xspace}
\newcommand{\manysatbds}{\texttt{ManySAT-BDS}\xspace}

\newcommand{\more}[1]{{\bf A VOIR:} \emph{#1}}
\newcommand{\nomore}[1]{}
\newcommand{\eg}{\textsl{e.g. }}
\newcommand{\set}[1]{\{ {#1} \}}
\newcommand{\goto}{\textsl{GO TO }}
\newcommand{\Label}{Label Trim}

%\newtheorem{definition}{Definition}
\newcommand{\ie}{\textit{ie.}\xspace}
\newcommand{\manysat}{\texttt{ManySAT}\xspace}

\begin{document}

\mainmatter  % start of an individual contribution



\title{On SAT Models Enumeration in Itemset Mining}
%\title{Models Enumeration in SAT-Based Itemset Mining}
\author{Said Jabbour and Lakhdar Sais and Yakoub Salhi}

\institute{
CRIL-CNRS Univ. Artois\\
F-62307, Lens \\
France \\
\{jabbour, sais, salhi\}@univ-orleans.fr
}

\maketitle




\begin{abstract}
Frequent itemset mining is an essential part of data analysis and data mining.
Recent works propose interesting SAT-based encodings for the problem of discovering 
frequent itemsets. Our aim in this work is to define strategies for adapting 
SAT solvers to such encodings in order to improve models enumeration.
In this context, we deeply study the effects of restart, branching heuristics and clauses learning.
We then conduct an experimental evaluation on SAT-Based itemset mining instances to show how SAT solvers can be adapted to obtain an efficient SAT model enumerator. 
\end{abstract}
 
\section{Introduction}
\label{sect:introduction}

Frequent itemset mining is a keystone in several data analysis and data mining tasks. Since the first article of Agrawal \cite{agrawal93} on association rules and itemset mining, the huge number of works, challenges, datasets and projects show the actual interest in this problem (see \cite{tiwari2010survey} for a  survey of works addressing this problem). 
In~ \cite{Raedt08}, De Raedt  et al initiate a research  trend on constraint programming and data mining. The authors proposed a framework 
for itemset mining offering a declarative and flexible representation with several generic and efficient CP solving techniques.
Encouraged by the promising results of this framework, several contributions addressed other data mining problems using either constraint programming (CP) or 
 propositional satisfiability (SAT) (e.g. \cite{Raedt08,GunsNR11,Lynce12Itemset,CoqueryJSS12,JabbourSS13topk,JabbourSS13seq}).
 In this work, we focus on the SAT-based encoding of itemset mining problems \cite{JabbourSS13topk}. In this new SAT application, the goal is to enumerate all the models of the propositional formula. 

Today, propositional satisfiability has gained a considerable audience with the advent of a new generation of solvers able to solve large instances encoding real-world problems. 
%and the demonstration that these solvers represent important low-level building blocks for many important fields, e.g., SAT modulo theory (SMT), Model checking, Quantified boolean formulas (QBF) , Maximum Satisfiability (Max-SAT), Pseudo boolean (PB),  Knowledge compilation (KC), etc. 
In addition to the traditional applications of SAT to hardware and software formal verification, this impressive progress led to increasing use of SAT technology to solve new real-world applications such as  planning, bioinformatics, cryptography.  In the majority of these applications, we are mainly interested in the decision problem and 
some of its optimisation variants (e.g. Max-SAT). Compared to other issues in SAT, the SAT model enumeration problem has received much less attention. Most of the recent proposed model enumeration approaches are built on the top of SAT solvers. Usually, these implementations are based on the  use of additional clauses, called blocking clauses, to avoid producing repeated models~\cite{McMillan02,Chauhan03usingsat,morgado05silva,Jin05efficientconflict}. 
%The basic algorithms for model enumeration are based on adding the negation of the current found model which is different the use of blocked clauses defined in \cite{Kullmann97ona}. 
Improvements have  been proposed to this blocking clause based enumeration solvers (e.g. \cite{Jin05efficientconflict,morgado05silva}). 
In particular, the authors in~\cite{morgado05silva} proposed several optimizations obtained through learning and simplification of  blocked clauses. 
However, these kind of approaches are clearly impractical. Indeed, in addition to clauses learned form conflicts, one might add an exponential number of blocked clauses in the worst case.  In \cite{MartinGebser07}, the authors elaborate an interesting approach for enumerating answer sets of a logic program (ASP), centered around First-UIP learning and backjumping. 
%Other approaches for enumerating answer sets are also proposed in the literature (e.g. \cite{Lin2004115}).

In~\cite{JabbourLSS14}, we proposed an approach based on a combination of a DPLL-like procedure with CDCL-based SAT solvers
in order to mainly avoid the limitation that concerns the space complexity
induced by blocking clauses addition. In this work, we focus on the SAT encoding of the problem of frequent itemset mining that we introduced in~\cite{JabbourSS13topk}. In such encoding, there is a one-to-one mapping between the models of the propositional formula and the set of interesting patterns  of the transaction database. Additionally, even for  condensed representation such as closed or maximal itemsets, the size of the output might be exponential in the worst case. 

The work presented in this paper is mainly motivated by this interesting SAT application to data mining and by the lack of efficient model enumerator. 

%The SAT-based data mining framework is interesting since the set of interesting patterns corresponding to the set of models of the propositional formula the is often very large.

Our aim is to study through an extensive empirical evaluation, the effects on model enumeration of the main components of CDCL based SAT solvers including restarts, branching heuristics and clauses learning. 
%To this end, we conduct an extensive empirical evaluation. 
 
\section{Background}

Let us first introduce the propositional satisfiability problem (SAT) and some necessary notations.  
We consider the  conjunctive normal form (CNF) representation for the propositional formulas. A {\it CNF formula}  $\Phi$  is a
conjunction ($\wedge$) of {clauses}, where a {\it clause} is a disjunction ($\vee$) of {literals}. 
A {\it literal} is a positive ($p$) or negated ($\neg{p}$) 
propositional variable.  The two literals $p$ and $\neg{p}$ are called {\it complementary}. A CNF formula can also be seen as a set of clauses, and a clause as a set of literals. 
Let us mention that any propositional formula can be translated to CNF using linear Tseitin's encoding \cite{Tseitin68}. 
We denote by $Var(\Phi)$ the set of propositional variables occurring in $\Phi$.

A {\it Boolean interpretation} ${\cal B}$ of a propositional formula $\Phi$ is a function which  associates a value ${\cal B}(p )\in\{0, 1\}$ ($0$ corresponds to $false$ and $1$ to $true$)
to the propositional variables $p \in Var(\Phi)$. It is extended to CNF formulas as usual.
 A {\it model} of a formula $\Phi$ is a Boolean  interpretation ${\cal B}$ that  satisfies the  formula, i.e., ${\cal B}(\Phi)=1$. 
  We note ${\cal M}(\Phi)$ the set of models of $\Phi$. {\it SAT problem} consists in deciding if a given  formula 
admits a model or not. 
%This well known NP-Complete problem has seen spectacular progress these recent years. Efficient SAT solvers can now handle CNF formulae encoding industrial problems up to millions of variables and clauses. Providing SAT encoding allows us to benefit from this progress. 

Let us informally describe the most important components of modern SAT solvers. They are based on a reincarnation of the historical Davis, Putnam, Logemann and Loveland procedure, commonly called DPLL \cite{Davis62}. It performs a backtrack search; selecting at each level of the search tree, a decision variable which is set to a Boolean value. This assignment is followed by an inference step that deduces and propagates some forced unit literal assignments. This is recorded in the implication graph, a central data-structure, which encodes the decision literals   together with there implications. This branching process is repeated until finding a model or a conflict. In the first case, the formula is answered satisfiable, and the model is reported, whereas in the second case, a conflict clause (called learnt clause) is generated by resolution following a bottom-up traversal of the implication graph \cite{Marques-Silva96,Zhang01}. The learning or conflict analysis process stops when a conflict clause containing only one literal from the current decision level is generated. Such a conflict clause asserts that the unique literal with the current level (called asserting literal)  is implied  at a previous level, called assertion level,  identified as the maximum level of the other literals of the clause. The solver backtracks to the assertion level and assigns that asserting literal to \textit{true}. When an empty conflict clause is generated, the literal is implied at level 0, and the original formula can be reported unsatisfiable. In addition to this basic scheme, modern SAT solvers use other components such as activity based heuristics and restart policies. An extensive overview can be found in \cite{HandbookSAT}.

\section{Frequent Itemset Mining}

%The problem of mining frequent itemsets (FMI for short) is well-known and essential in data mining, knowledge discovery and data analysis.  Note that several data mining tasks are closely related to the itemset mining problem such as the ones of association rule mining, frequent pattern mining in sequence data, data clustering, etc. 

%In itemset mining problem, the notion of Top-$k$ frequent itemsets is introduced as an alternative to finding the appropriate value for the minimum support threshold.
%In this section, we propose a SAT-based encoding  for enumerating all closed itemsets.  
%Then  we use this encoding in the Top-$k$ SAT problem for computing all Top-$k$ frequent closed itemsets.
Formally, we define the problem of mining frequent itemsets (FMI for short) in the following way. 
Let $\Omega$ be a finite set of {\it items}. 
A {\it transaction} is defined as a couple $(tid,I)$ where $tid$ is the {\it transaction identifier} and 
$I$ is an {\it itemset}, i.e., $I\subseteq {\Omega}$. A {\it transaction database}  is a finite set of transactions 
where the attribute $tid$ refers to a unique itemset. 
We say that a transaction $(tid, I)$ {\it supports} an itemset $J$ if  $J\subseteq I$.\\
~\\
The {\it cover} of an itemset $I$ in a transaction database $\cal D$ is the set of
transactions  in   $\cal D$ supporting $I$: 
${\cal C}(I,{\cal D})=\{(tid,J)\in{\cal D}\mid  I\subseteq J \}$.
The {\it support} of an itemset $I$ in $\cal D$ is defined as the size of its cover:
${\cal S}(I,{\cal D})=\mid {\cal C}(I,{\cal D})\mid$.
%Moreover, the frequency of $I$ in $\cal D$ is defined by:  
%${\cal F}(I,{\cal D})=\frac {{\cal S}(I,{\cal D})}{\mid{\cal D}\mid}$.\\

\begin{table}
\begin{center}
\begin{tabular}{cccc}
\hline
Tid & Itemset \\
\hline
&&&\\
1 &  $A,B,C,D$ \\
%\hline
2 & $A,B,E,F$ \\	
%\hline
3 &  $A,B,C$ \\
%\hline
4 & $A,C,D,F$ \\
%\hline
5 & $G$ \\
%\hline
6 & $D$\\\cal B
%\hline
7 & $D,G$ \\
\hline
\end{tabular}
\end{center}
\caption{A transaction database $\cal D$}
\label{table1}
\end{table}
%\cal B
Let $\cal D$ be a transaction database over $\Omega$ and $n$ a minimum support threshold.
The {\it frequent itemset mining problem} consists in computing the following set:
$${\cal FIM}({\cal D},n)=\{I\subseteq {\Omega}\mid {\cal S}(I,{\cal D})\geq n\}. $$
\begin{definition}[Closed Frequent  Itemset]
Let $\cal D$ be a transaction database (over $\Omega$) and $I$ an itemset ($I\subseteq{\Omega}$)
such that ${\cal S}(I,{\cal D})\geq 1$.
The itemset $I$ is closed if, for all itemset $J\subseteq {\Omega}$ with $I\subset J$, we have that 
${\cal S}(J,{\cal D}) < {\cal S}(I,{\cal D})$.
\end{definition}
One can  see that all the elements of ${\cal FIM}({\cal D},n)$ can be obtained from the closed 
itemsets by computing their subsets. Enumerating all closed itemsets
allows us to reduce the size of the output. We denote by ${\cal CFIM}({\cal D},n)$ the subset of all closed itemsets in ${\cal FIM}({\cal D},n)$.

For instance, consider the transaction database described in Table~\ref{table1}. 
The closed frequent itemsets with the minimal support threshold equal to 2 are: 
${\cal CFIM}({\cal D}, 2)=\{A, D, G, AB, AC, AF, ABC,ACD\}$.


\section{A SAT Encoding of Frequent Itemset Mining}
\label{sec:enc}
%\subsection{Preliminary Definitions and Notations}
In this section, we describe SAT encodings for itemset mining which are mainly based on the encodings proposed in~\cite{JabbourSS13topk}. 
 In order to do this, we fix, without loss of generality, a transaction database 
 ${\cal D}=\{(1,I_1), \ldots{}, (m, I_m)\}$ and a minimal support threshold $n$.
 
 The SAT encoding of itemset mining that we consider is based on the use of propositional variables representing the items and the transaction identifiers in $\cal D$.  
 More precisely, for each item $a$ (resp. transaction identifier $i$), we associate a propositional variable, denoted $p_a$ (resp. $q_i$).
 These propositional variables are used to capture all possible itemsets and their covers. Formally, given a model $\cal B$ of the considered encoding, 
 the candidate itemset is $\{a\in \Omega\mid {\cal B}(p_a)=1\}$ and its cover is $\{i\in \mathbb{N}\mid {\cal B}(q_i)=1\}$.
 
 The first propositional formula that we describe allows us to obtain the cover of the candidate itemset: 
 \begin{equation}
 \label{form:1}
 \bigwedge_{i=1}^m (\neg q_i \leftrightarrow \bigvee_{a\in \Omega\setminus I_i} p_a)
 \end{equation}
 This formula expresses that $q_i$ is true if and only if the candidate itemset is supported by the $i^{th}$ transaction. In other words, the candidate itemset is not supported by the $i^{th}$ transaction ($q_i$ is false), when there exists an item $a$ ($p_a$ is true)  that does not belong to the transaction ($a\in \Omega\setminus I_i$).
 
 The following propositional formula allows us to consider the itemsets having a support greater than or equal to 
 the minimal support threshold: 
  \begin{equation}
   \label{form:2}
\sum_{i=1}^m q_i \geq n
 \end{equation}
This formula corresponds to 0/1 linear inequalities, usually called cardinality  constraints.  
The first linear encoding of general 0/1 linear inequalities to CNF have been proposed by J. P. Warners in~\cite{Warners96}. 
Several authors have addressed the issue of finding an efficient encoding of cardinality (e.g. \cite{Sinz05,SilvaL07,Asin11}) as a CNF formula. 
Efficiency refers to both the compactness of the representation (size of the CNF formula)  and to the ability to achieve the same level of constraint propagation (generalized arc consistency) 
on the CNF formula.\\

We use ${\cal E}_{FIM}({\cal D},n)$ to denote the encoding corresponding to the conjunction of the two formul\ae{} ($\ref{form:1}$) and ($\ref{form:2}$).
Then, we have the following property:
$\cal B$ is a model of ${\cal E}_{FIM}({\cal D},n)$ iff $I=\{a\in\Omega\mid {\cal B}(p_a)=1\}$ is a frequent itemset where ${\cal C}(I,{\cal D})= \{i\in\mathbb{N}\mid {\cal B}(q_i)=1 \}$.


We now describe the propositional formula allowing to force the candidate itemset to be closed: 
\begin{equation}
\label{form:3}
\bigwedge_{a\in {\Omega}} (\bigwedge_{i=1}^{m} q_{i}\rightarrow a\in I_i)\rightarrow   p_{a}
\end{equation} 
This formula means that if we have ${\cal S}(I, {\cal D})={\cal S}(I\cup\{a\}, {\cal D})$ then $a\in I$ holds. 
This condition is necessary and sufficient to force the candidate itemset to be closed. 
Let us note that the expressions  of the form $a\in I_i$ correspond to constants, i.e.,  $a\in I_i$ corresponds to $\top$ if the item $a$ is in $I_i$, to $\bot$ otherwise.

Note that the formula ($\ref{form:3}$) can be simply  reformulated as a conjunction of clauses as follows: 
\begin{equation}
\label{form:32}
\bigwedge_{a\in {\Omega}} ( (\bigvee_{ 1\leq i\leq m, a\not\in I_i,} q_{i})\vee  p_{a})
\end{equation} 
This reformulation is obtained using the equivalence $A\rightarrow B\equiv\neg A\vee B$.

We use ${\cal E}_{CFIM}({\cal D},n)$ to denote the encoding corresponding to the conjunction of the formul\ae{}  ($\ref{form:1}$), ($\ref{form:2}$) and ($\ref{form:32}$).
Then, we have the following property:
$\cal B$ is a model of ${\cal E}_{CFIM}({\cal D},n)$ iff $I=\{a\in\Omega\mid {\cal B}(p_a)=1\}$ is a closed frequent itemset where ${\cal C}(I,{\cal D})= \{i\in\mathbb{N}\mid {\cal B}(q_i)=1 \}$.


\begin{example}
Let us consider the transaction database of Table \ref{table1}. The Problem encoding the enumeration of frequent closed itemsets with a threshold 4 can be written as: \\

\begin{tabular}{ll}
 & $ \{ \neg q_1 \leftrightarrow (p_{E} \vee p_{F} \vee p_{G})$,\\
&$\neg q_2 \leftrightarrow (p_{C} \vee p_{D} \vee p_{G})$,\\
&$\neg q_3 \leftrightarrow (p_{D} \vee p_{E} \vee p_{F} \vee p_{G})$,\\
&$\neg q_4 \leftrightarrow (p_{B} \vee p_{E} \vee p_{G})$,\\
&$\neg q_5 \leftrightarrow (p_{A} \vee p_{B} \vee p_{C} \vee p_{D} \vee p_{E} \vee p_{F})$,\\
&$\neg q_6 \leftrightarrow (p_{A} \vee p_{B} \vee p_{C}  \vee p_{E} \vee p_{F} \vee p_{G})$,\\
&$\neg q_5 \leftrightarrow (p_{A} \vee p_{B} \vee p_{C} \vee p_{E} \vee p_{F}),$\\
&($q_5 \vee q_6 \vee q_7 \vee p_{A}$), \\
&($q_4 \vee q_5 \vee q_6 \vee q_7 \vee p_{B}$), \\
&($q_2 \vee q_5 \vee q_6 \vee q_7 \vee p_{C}$), \\
&($q_2 \vee q_3 \vee q_5  \vee p_{D}$), \\
&($q_2 \vee q_3 \vee q_4 \vee q_5 \vee q_6 \vee q_7 \vee p_{E}$), \\
&($q_1 \vee q_3 \vee q_4 \vee q_5 \vee q_6 \vee q_7 \vee p_{F}$),\\
&($q_1 \vee q_2 \vee q_3 \vee q_4 \vee q_6 \vee  p_{G}$),\\
& $q_1 + q_2 + q_3 + q_4 +q_5 + q_6 + q_7 \ge 4 \}$
\end{tabular}
\end{example}

\section{Enumerating all Models of CNF Formulae} 
\label{sec:enum}
A naive way to extend modern SAT solvers for the problem of enumerating all models of a CNF formula consists in adding a blocking clause to prevent the search to return the same model again. This approach is used in the majority of the model enumeration methods in the literature. 
The main limitation of this approach concerns the space complexity, since the number of blocking clauses may be exponential in the worst case. 
Indeed, in addition to the clauses learned at each conflict by the CDCL-based SAT solver, the number of added blocking clauses is very important on problems with a huge number of models.
This explains why it is necessary to design methods avoiding the need to keep all blocking clauses. 
It is particularly the case for encodings of data mining tasks where the number of interesting patterns is often significant, even when using condensed representations such as closed patterns. 


%Modern SAT sovlers can be extended to enumerate to deal with the problem of enumerating all models of a CNF theory.
%the first naive way to extend modern SAT solvers to solve the problem of enumerating all modes of a CNF formula consists in adding a blocking clause each time a model is found. We call this first extension $BC$-$Enum$, for blocking clause based enumeration solver.   The enumeration solver $BC$-$Enum$ and its improved variants admit several drawbacks. The first problem is that the space complexity of $BC$-$Enum$-like algorithm is exponential in the worst case.  Indeed, in addition to the clauses learned at each conflict by the CDCL-based SAT solver, the number of added blocking clauses remains very important on problems with a huge number of models. The second problem is related to the use of VSIDS variable ordering heuristic more suitable for finding a single model or proving that such a model does not exist.  It is well known that the ordering used for enumerating all models may change radically the computational complexity \cite{CreignouOS11}. In \cite{Dechter92findingall}, Dechter and Itai have shown that enumerating all models of a given theory can be performed in time proportional to the product of the number of models and the effort needed to generate each model in isolation. Consequently, one possible way to improve such enumeration process is to search for all the models near the model found at a given iteration. 
%Let us mention, that in \cite{MartinGebser07}, as long as no solution has been found, the First-UIP scheme is applied as usual (see. \cite{GebserKNS07}). Once a model is found, its decision literals are backtracked chronologically. 

%Motivated by the above observations,  in \cite{}, the authors propose an extension to CDCL based solvers in order to enumerate all models of a CNF formula. Our algorithm, called $BR$-$Enum$ (for Backtrack with Reason based Enumeration), is obtained from CDCL based SAT solver ${\cal S}$ in the following way: 
%\begin{enumerate}
%\item Search for the first model using  ${\cal S}$ without any modification
%\item After finding the first model, run ${\cal S}$ while inhibiting the restart (without restart)
%\item Let $<x_1, x_2\dots x_n>$ be the sequence of decision literals of the branch associated to the current model. The algorithm backtrack to the decision level ${n-1}$ and propagate the literal $\tilde{x_n}$ thanks to the reason $(\tilde{x_1}\vee\tilde{x_2}\vee\dots\vee\tilde{x_n})$. 
%\end{enumerate}
%
%Our proposal aims to eliminate the main limitations of the $BC$-$Enum$ algorithm identified previously. As mentioned above, the main limitation concerns the space complexity induced blocking clauses addition. 


%\subsection{Impact of Learning and Restart on Frequent Itemset Enumeration}
%\subsection{DPLL versus CDCL on enumeration problems}
Our main aim is to experimentally study the effects of each component of modern SAT solvers on the efficiency of the model enumeration, in the case of the encoding described in Section~\ref{sec:enc}. 
As the number of  frequent closed itemsets is usually huge, this results in a huge number of models for the considered encoding.
Consequently, it is not suitable to store the found models using blocking clauses during the enumeration process. 
%Starting from the previous observation stating that the number of frequent closed itemset set is generally huge. 
%As a consequence, the number of models of corresponding SAT formula is very huge. 
%As a consequence, storing models during enumeration prevent the efficiency of SAT solvers to  compete with dedicates ones. As a consequence, SAT solvers must be adapted in order to avoid storing such models during search. to reach this goal, 


We proceed by removing incrementally some components of modern SAT solvers in order to evaluate their effects on the efficiency of model enumeration. The first removed component is  the restart policy.  
Indeed, we inhibit the restart in order to allow solvers to avoid the use of blocking clauses. Thus, our procedure performs a simple backtracking at each found model.
The second removed component is that of  clause learning, which leads to a DPLL-like procedure.  
%If this removal outperform those of CDLC based enumeration, then the question is if clause learning is absolutely required. To answer this question, we propose to remove  completely the clause learning component leading to a DPLL procedure. 
%Removing restart from SAT solver and in order to avoid redundancy this is implied that the solver must perform a simple backtracking instead of a backjumping. Pushing further this reasoning, we question on the utility of clause learning component. So we decide to remove the clause learning component allowing to consider only a DPLL procedure.
%By removing the restart and learning, the obtained solver is a DPLL procedure. 
Considering a DPLL-like procedure,  we pursue our analysis by considering the  branching heuristics.  Indeed, our goal is to find the heuristics suitable to the considered SAT encoding.  
To this end, we consider three branching  heuristics. We first study the performance of the well-known VSIDS (Variable State Independent, Decaying Sum) branching heuristic. 
In this case, at each conflict an analysis is only performed to weight variables (no learnt clause is added).
The second considered branching heuristic is based on the maximum number of occurrences of the the variables. The third one consists in selecting the variables randomly. 
%Indeed, our goal is to find which heuristic deal efficiently with SAT problems encoding frequent closed itemsets. To answer this question, we consider three heuristics. The first one is VSIDS. Indeed, at each conflict a conflict analysis is performed only to weight variables. The second one is MOMS \cite{}, and the last one is a random based variable selection.


%Now using a simple DPLL procedure for model enumeration, heuristic can have an impact on enumeration? To answer this question we consider our DPLL enumerator with three different heuristic. The first one choose randomly a variable. The second one is based on MOMS \cite{}. It choose the variable having the maximum occurrences.

\section{Experiments}

We carried out an experimental evaluation to analyze the effects of adding blocking clauses, adding learned clauses and branching heuristics. To this end, 
we implemented a DPLL-like procedure, denoted {\tt DPLL-Enum}, without adding blocking and learned clauses. We also implemented a procedure on the top 
of the state-of-the-art CDCL SAT solver MiniSAT 2.2, denoted {\tt CDCL-Enum}. In this procedure, each time a model is found, we add a no-good and perform a restart. 
 We considered a variety of datasets taken from the {\tt FIMI}\footnote{FIMI: http://fimi.ua.ac.be/data/} and {\tt CP4IM}\footnote{CP4IM: http://dtai.cs.kuleuven.be/CP4IM/datasets/} repositories.  
 All the experiments were done on Intel Xeon quad-core machines with 32GB of RAM running at 2.66 Ghz. For each instance, we used a timeout of 15 minutes of CPU time.
%\textcolor{red}{demander a francois les caracterisitques du cluster utilise}

%We carried out an experimental evaluation of the performance of a  SAT solver using based on a DPLL procedure to enumerate solutions. We note this solver {\tt DPLL-Enum}. We compare its performances against a solver based on a CDCL solver enumerating solution named {\tt CDCL-Enum}. This solver  store models during search and perform a restart each time a model is found.
% We considered a variety of datasets taken from the {\tt FIMI}\footnote{FIMI: http://fimi.ua.ac.be/data/} and {\tt CP4IM}\footnote{CP4IM: http://dtai.cs.kuleuven.be/CP4IM/datasets/} repositories.  
% All the experiments were done on Intel Xeon quad-core machines with 32GB of RAM running at 2.66 Ghz. For each instance, we used a timeout of 30 minutes of CPU time.
%\textcolor{red}{demander a francois les caracterisitques du cluster utilise}

In our experiments, we compare the performances of {\tt CDCL-Enum} to three variants of {\tt DPLL-Enum}, with different branching heuristics, in enumerating all the models corresponding to the closed frequent itemsets. The considered variants of {\tt DPLL-Enum} are the following: 
\begin{itemize}
\item {\tt DPLL-Enum+VSIDS}:  {\tt DPLL-Enum} with the VSIDS branching heuristic; 
\item {\tt DPLL-Enum+JW}:  {\tt DPLL-Enum} with a branching heuristic based on the maximum number of occurrences of the variables \cite{Jeroslow90}; 
\item {\tt DPLL-Enum+RAND}: {\tt DPLL-Enum} with a random variable selection. 
\end{itemize}
%To evaluate the performances of the considered enumeration  procedures, we compare the time needed to   
%{\tt CDCL-Enum}, and 3 variants of {\tt DPLL-Enum} i.e., {\tt DPLL-Enum+JW}, {\tt DPLL-Enum+RAND}, and {\tt DPLL-Enum+VSIDS} (with different branching heuristics) to enumerate all models corresponding to all closed frequent itemsets. 

Our comparison is depicted by the the cactus plots of Figure \ref{fig:scatter}.  Each dots $(x, y)$ represents an instance  with a fixed minimal support threshold $n$. Each cactus plot represents an instance and the evolution of CPU time needed to enumerate all models with the different algorithms while varying the quorum. For each instance, we tested different values of $n$.   The x-axis (respectively y-axis) represents the CPU time (in seconds) needed for the enumeration of all closed frequent itemsets. 

%Our comparison is depicted by the the scatter plots of Figure \ref{fig:scatter}.  Each dots $(x, y)$ represents an instance  with a fixed minimal support threshold $n$. The scatterplot represent all the instances described in Table \ref{tab:fimi} (18 instances), where for each instance, we tested 70 different values of $n$.    The x-axis (respectively y-axis) represents the CPU time (seconds) needed for the enumeration of all closed frequent itemsets. 

%(see Table \ref{tab:fimi})

 \begin{figure}[htbp]
\centering
\begin{tabular}{cc}
  \includegraphics[width=5cm]{FIG/german-credit.pdf}   & \includegraphics[width=5cm]{FIG/australian-credit.pdf}    \\
  german-credit & australian-credit \\
   \includegraphics[width=5cm]{FIG/hepatitis.pdf}   & \includegraphics[width=5cm]{FIG/mushroom.pdf}    \\
  hepatitis.pdf & mushroom \\
    \includegraphics[width=5cm]{FIG/anneal.pdf}   & \includegraphics[width=5cm]{FIG/primary-tumor.pdf}    \\
  anneal & primary-tumor \\  
      \includegraphics[width=5cm]{FIG/heart-cleveland.pdf}   & \includegraphics[width=5cm]{FIG/splice-1.pdf}    \\
  heart-cleveland.pdf & splice-1 \\   
        \includegraphics[width=5cm]{FIG/chess.pdf}   & \includegraphics[width=5cm]{FIG/kr-vs-kp.pdf}    \\        
  chess & kr-vs-kp \\      
  \end{tabular}
\caption{Frequent Closed Itemsets: CDCL vs DPLL-Like enumeration} 
\label{fig:scatter}
\end{figure}




%Clearly, the partition based approach outperforms those without partition on the majority of instances.  

%The results of our empirical evaluation allows the following observations. 
Unsurprisingly, the DPLL-like procedures outperform {\tt CDCL-Enum} on the majority of instances. 
This shows that a DPLL  based approach is more suitable for SAT-based itemset mining. 
Part of explanation lies in the significant number of models. Furthermore, {\tt DPLL-Enum+RAND} 
is clearly less efficient than  {\tt DPLL-Enum+VSIDS} and {\tt DPLL-Enum+JW}, which shows that the branching heuristic 
plays a key role in model enumeration algorithms. Moreover, our experiments show that {\tt DPLL-Enum+JW} is better than 
{\tt DPLL-Enum+VSIDS}, even if {\tt DPLL-Enum+VSIDS}  compete with the procedure {\tt DPLL-Enum+JW} on datasets such as {\tt anneal} and {\tt mushroom}.
Indeed, {\tt DPLL-Enum+JW} clearly outperforms {\tt DPLL-Enum+VSIDS} on several datasets, such as {\tt chess}, {\tt kr-vs-kp} and {\tt splice-1}. Note that for theses two data, the solvers {\tt DPLL-Enum+RAND} and {\tt CDCL-Enum} are not able to enumerate completely the set of all models of all considered quorums.

%An explanation of the performance of  the procedure  {\tt DPLL-Enum+JW} lies in the fact that we use a branching heuristic similar to a heuristic used in the  best dedicated frequent itemset miner. Indeed, the number of  occurrences of items is used as a heuristic for selecting candidate itemsets.\\

%Unsurprisingly, {\tt CDCL-Enum} algorithm obtain the worst performances. Avoiding storing blocking models during search allows to better enumerate models encoding frequent closed itemsets problems. Consequently,  DPLL-Based procedures is more suitable to enumerate frequent closed itemsets encoded into CNF. Concerning the heuristics, {\tt CDCL-Enum-RAND} is less efficient that  {\tt CDCL-Enum-VSIDS} and {\tt CDCL-Enum-MOMS}. This is show clearly the branching heuristic play a important role during the enumeration process. 
%Finally between {\tt CDCL-Enum-VSIDS} and {\tt CDCL-Enum-MOMS}, {\tt CDCL-Enum-MOMS} is better. Even if {\tt CDCL-Enum-VSIDS}  compete with the procedure {\tt CDCL-Enum-MOMS} on several data i.e., {\tt anneal, mushroom}, etc.  On other datas {\tt chess, kr-vs-kp, splice-1}, {\tt CDCL-Enum-MOMS} outperforms clearly {\tt CDCL-Enum-VSIDS}. It arrives to enumerate all models for smallest Quorum values and on the instantiation solved by the two algorithms, {\tt CDCL-Enum-MOMS} obtain better time. 
%An explanation of the performance of 
%
%%On the considered instances, the solver {\tt DPLL-Enum+JWMS}  is clearly the the best model enumerator. The solver outperform considerably the other considered procedures. More precisely,  {\tt DPLL-Enum+JWMS} arrives to enumerates all models for smaller values  of quorum when CDCL-Based enumerator struggle. For some instances e.g., {\tt anneal, australian-credit}, etc. the performances are clearly impressive.
%
%Theses good performances of  {\tt DPLL-Enum+JWMS} can be explained by the fact that the best dedicated frequent itemset miner  considers the occurrences of items in transactions databases as a way to guide their searches.
 
 
 As a summary, our experimental evaluation suggests that a DPLL-like procedure is a more suitable approach when the number of models of a propositional formula is significant. 
 It also suggests that the branching heuristic is a key point in such a procedure to improve the performance. 
 
 
%As a summary, to allow SAT technologie to handle problems coming from data mining, the SAT-Based enumerators must be better analyzed to design more efficient solvers. Our empirical evaluation suggests that DPLL-Based is a promising way when the number of models is huge. We proved that the branching heuristic is a .... key to the efficiency of enumeration. incorporate cleverly  clause learning component enumeration algorithm is a challenging work that we plan to investigate.
%
%As described in the previous section,  the Algorithm \ref{DEC} takes a transaction database and a k-partition of the set of items as inputs, and returns the set of patterns of interest (frequent, closed or maximal). In our experiments, we consider a partition ${\cal P}$ where each $S_i\in {\cal P}$ contains a single item and $S_i\prec S_{i+1}$ if $S_i$ contains a less frequent item than  $S_{i+1}$. Obviously, in this case $k$ is equal to $|\Omega|$.  This ordering allows us to first generate encodings of smaller size. Our goal is to show the feasibility of our proposed approach even when a basic partitioning scheme is considered. Finding a $k$-partition of the set of items that leads to better improvements is an interesting optimisation problem. This issue is out of the scope of this paper.   We compare our partition based approach noted $SAT^{\cal P}_{CFIM}$ ($SAT$-$P$-$CFIM$ in the figures) with  $SAT_{CFIM}$, the encoding of frequent closed itemsets mining problem without partition (named $SAT$-$CFIM$ in the figures). 
%
%We implemented the Algorithm \ref{DEC} in C. For the enumeration of all models of the Boolean formula encoding the corresponding itemset mining problem, we use the extension of modern SAT solvers  described in \cite{JSS2013IRI}.  The implementation is based on an extension of MiniSAT 2.2 \footnote{MiniSAT: http://minisat.se/}. 
%
%
%Note that, the time needed to generate the partition does not exceed 1 seconds on the majority of the instances, except for {\tt splice-1} and {\tt connect}, which takes 17 and 60 seconds respectively. 

%
%First, we present in Table \ref{tab:fimi}, the characteristics of the dataset and the size of the CNF formula encoding the whole transaction database  for the closed itemsets mining problem. 
%%More precisely, to be independent from a given support threshold, we only illustrate the size of the encoding by omitting the frequency constraint (formula \ref{form:2}). 
%For each instance, we mention the number of transactions ($\#trans$), the number of items ($\#items$), the size of the formula encoding the whole problem in terms of number of variables ($\#vars$) and clauses ($\#clauses$). The last two columns give the number of clauses of the smallest ($min$) respectively the largest formula ($max$) generated using our partition based encoding. 
%On all instances, the number of clauses of the largest  formula ($max$) generated with our partition based encoding is significantly smaller than those generated without partition ($\#clauses$). 
%
%%
%
%
%
%
%
%
%
%
%This is implies that restarts must be completely eliminated from SAT solvers. 
%
%Since the restart is removed to avoid storing huge number of models, one have to remove the clause learning component. This allows us to have a simple DPLL solvers. 
%Our first experiments  consists then, to remove restarts in SAT solvers  and compare the performances of obtained solver with the one performing restarts during search. 
%To avoid redundant models, at each conflict or found model, the solver perform  a simple backtracking. Consequently the obtained solver is a DPLL solver.
%Since, the obtained solver is a DPLL, we propose to study the intake of clause learning. Our second experiments consists to remove the clause learning i.e., no clause is learned. We name the obtained solver ${\tt DPLL-WL-VSIDS}$ for DPLL without learning but the VSDIS heuristic is kept.
%Unsurprisingly, the obtained solver allows to improve the obtained results. Figure \ref{} shows that eliminating also the learnt clauses allows to  split the time in half.
%Now we are interested with the VSIDS heuristic. Using a 
%

\section{Conclusion}
In this paper, we investigated the impact of modern SAT solvers on the problem of enumerating all the models of CNF formulas encoding frequent closed itemsets mining problem. Our goal is to measure the impact of the classical components of CDCL-based SAT solvers on the efficiency of model enumeration. Our results suggest that on formula with a huge number of models, SAT solvers must be adapted to efficiently enumerate all the models. We showed that the simple DPLL solver augmented with the classical Jeroslow-Wang heuristic achieve better performance.  

%simple extension of modern SAT solvers to deal with the problem of enumerating all models of a CNF formula. Our extension aims to benefit from the efficiency of SAT solvers for finding a single model, while avoiding the main limitations behind the use of blocking clauses to avoid enumerating the same models.  We have shown that our proposed approach outperforms blocking clause based enumeration techniques with several orders of magnitude on both satisfiable instances taken from the last SAT challenge and also on the SAT instances encoding the sequence mining problem. The results presented in this paper will be helpful in several applications domains (data mining, non monotonic reasoning, knowledge compilation) where the issue is to find all the models instead of finding only one in the case of SAT.  

As a future work, we plan to pursue our investigation in order to find the best heuristics for enumerating models encoding data mining problems. Finding how to efficiently integrate clauses learning for model enumeration is another interesting issue. 


% a first  improvement to our new $BR$-$Enum$ algorithm consists in integrating, when a model is found, the best simplification techniques to derive the smallest possible sub-sequence of decisions that can be extended to the current model by unit propagation. We also plan, to compare our approach with other model enumeration algorithms \cite{Grumberg04,ZhaoW09}. 
 %interesting issue that we plan to investigate, is to find the best way for an efficient integration of clauses learning for model enumeration. 
 

\bibliographystyle{plain}
\bibliography{satBib}
\end{document}



the impact of learning on problems encoded using equations \ref{}, \ref{}, \ref{}. 
Since we have to enumerate all patterns that are frequents, and as the number of patterns can grows exponentially, we propose first to adapt SAT solvers in order to note store the set of all models. As a consequence, one have to desactive the restarts strategy.
Formally, we propose to use minisat solvers where the restarts is desactived. Each time a model is learnt, we extract the corresponding patterns allowing and we backtrack without storing the counter model. The model is written is a separated file.
The clauses learnt from each conflict is kept in this first section. 

We done a first comparison between the {\tt MiniSAT-Enum} that add a counter model to avoid to find it another time and and {\tt MiniSATWL-Enum} where restart is desactived and the models are not stored.
Figure \ref{} shows the obtained results. As we can observe, desactving the restarts strategy allows clearly to outperforms considerably the one storing the counter-models. On all considered instances as the number of models grows, the performances of 
{\tt MiniSATWL-Enum} grows more. \\


This first enhancement entourages us to pursue our investigation to be interested to learnt clauses. More precisely, we want to answer the question concerning the real role of clause learning in enumeration problems encoding the frequent closed itemsets problem. To this end, we propose to compare the solver {\tt MiniSATWL-Enum}  and {\tt MiniSATWL-Enum}   and when the the clause learning is desactived. More precisely, each time a conflict occurs, and a new clause is learnt, this clause is then used to backjump in the search tree but this clause is not attached to avoid its use during the propagation process.

Figure \ref{}, shows the obtains results. As we can see, adapting the role of clause learning in enumeration problem allows to maintain the same result with a slight amelioration.


In order to study the real impact of clause learning we perform a last experiment where {\tt MiniSATWL-Enum} is changed to be a simple DPLL solver i.e., in each conflict a simple backtracking is operated.

In this section, an experimental evaluation of our approach on large real world instances is given. We compare both {\tt BR-Enum} and {\tt BC-Enum} implemented on the top of the state of the art SAT solver  MiniSAT 2.2 \footnote{MiniSAT: http://minisat.se/}.

We conducted two kind of experiments. In the first one, we considered the satisfiable SAT instances taken from the SAT Challenge 2012 \footnote{http://baldur.iti.kit.edu/SAT-Challenge-2012/} .  After $4$ hours time limit, only few instances are solved i.e. all the models are found. On the majority of the instances, the number of models is very huge, or the formula contains a small number of models and the proof of the unsatisfiability (or the proof that there is no additional model) takes a long time. The results are depicted in Table \ref{tab:indusmodels4h}. As we can see on the solved instances, $BR$-$Enum$ significantly outperform $BC$-$Enum$.  What is surprising, is that $BR$-$Enum$ is even better for proving the unsatisfiability after finding the single model of the instance. We recall that both approaches perform the same search until finding the first model.  In Table \ref{tab:indusmodels1h}, we report on a sample of instances, the number of models computed by both approaches under the time limit of 1 hour. Again the number of models computed by $BR$-$Enum$ is significantly higher than the number of models computed by $BC$-$Enum$. 

%\begin{table}
%\begin{scriptsize}
%\centering
%\begin{tabular}{|l|c|c|c|}
%\hline
%Instance & \# M &  $BC$-$Enum$ & $BR$-$Enum$ \\
% &  &  time (sec.) & time (sec.)\\
%\hline\hline
%E03X18   & 40098146 &  -- &  {\bf 6903.92} \\
%AProVE09-19   & 83261 &  249.90 &   {\bf 41.23}  \\
%aes\_64\_1\_keyfind\_2  & 3 &  -- &   {\bf 3124.54} \\
%aes\_32\_3\_keyfind\_2  & 2 &  7426.28 &   {\bf 834.98} \\ 
%vmpc\_27  & 2   & 258.07  &  {\bf 242.70 } \\
%aes\_32\_3\_keyfind\_1 & 1 & 6902.55 &  {\bf 2530.45} \\ 
%vmpc\_26  & 1  &  {\bf 90.65} &  102.75  \\
%cnf-r4-b1-k1.2-comp.*-355  & 1 &  468.09   &  {\bf 232.35} \\
%cnf-r4-b1-k1.1-comp.*-354  & 1  & 419.00  &  {\bf 75.52} \\
%vmpc\_29.renamed-as.sat05-1916   & 1 &  1272.33 &    {\bf 674.98} \\
%cube-9-h11-sat  & 1 &  512.59 &   {\bf 356.43} \\
%gss-19-s100  & 1 &  1790.73  &    {\bf 802.94} \\
%cube-11-h14-sat  & 1  & 993.80 &    {\bf 896.06} \\
%\hline
%\end{tabular}
%  \caption{SAT Challenge 2012 - Application benchmarks}
%   \label{tab:indusmodels4h}
%  \end{scriptsize}
%\end{table}

%
%\begin{table}
%\begin{scriptsize}
%\centering
%\begin{tabular}{|l|c|c|}
%\hline
%Instance & $BC$-$Enum$ & $BR$-$Enum$ \\
%& \# M  & \# M\\
%\hline\hline
%2dimensionalstrippacking/E03X18 					& 1 710 611 	& {\bf 19 278 566}\\
%AProVE09-17 									& 411 509 		& {\bf 20 917 038}\\
%AProVE09-19 									& 579 568 		&{\bf 23 207 913}\\
%AProVE09-10									 & 258 651 	&{\bf 26 271 396}\\
%AProVE11-09 									& 287 893 		&{\bf 17 158 626}\\
%AProVE09-24 									& 270 811 		&{\bf 29 637 497}\\
%AProVE11-16 									& 198 568 		&{\bf 22 501 889}\\
%AProVE11-15 									& 187 707 		&{\bf 31 721 321}\\
%AProVE11-05 									& 157 466 		&{\bf 25 576 043}\\
%AProVE09-15 									& 124 949 		&{\bf 17 769 578}\\
%AProVE09-20									 & 367 337		&{\bf 44 453 886}\\
%E04F17   			         							& 1 940 731 		& {\bf 32 514 229}\\
%E05F18 										& 1 400 553 	& {\bf 25050772}\\
%een-tip-sat-nusmv-t5.B 							& 335 379 			& {\bf 27 875 794}\\
%maris-s03-gripper11 							& {\bf 1 377 539} 		& 2 783\\
%ndhf\_xits\_21\_SAT								 & 1 933 955 	& {\bf 17683508}\\
%ndhf\_xits\_22\_SAT								 & 1 759 887 	& {\bf 21 338 735}\\
%q\_query\_3\_l38\_lambda 						& 751 319 			& {\bf 23 719 149}\\
%q\_query\_3\_l42\_lambda 						& 704 322 			& {\bf 20701564}\\
%q\_query\_3\_l41\_lambda 						& 687 614 			&{\bf 22 471 909}\\
%q\_query\_3\_l40\_lambda 						& 750 261 			& {\bf 26 383 677}\\
%q\_query\_3\_l39\_lambda	 					& 700 211 			& {\bf 24 895 994}\\
%q\_query\_3\_l43\_lambda 						& 632 218 		& {\bf 20 927 175}\\
%SAT\_dat.k100 									& 163 551 		& {\bf 16 406 161}\\
%smtlib-qfbv-aigs-innfeed\_innfeed\_vc36608-tseitin 		& 153 643 		& {\bf 15 815 556}\\
%smtlib-qfbv-aigs-innfeed\_innfeed\_vc37051-tseitin 		& 168 765 		& {\bf 15 849 656}\\
%smtlib-qfbv-aigs-src\_wget\_vc18517-tseitin 			& 73 186 		&{\bf 154 03 814}\\
%palac-sn7-ipc5-h16 								& 73 064 		& {\bf 14 696 917}\\
%rbcl\_xits\_14\_SAT 								& 2 322 846 	&{\bf 60 331 630} \\
%rbcl\_xits\_15\_SAT 								& 2 345 052 	& {\bf 46 581 322}\\
%sha0\_35\_3									 & 73			 & {\bf 120}\\
%sha0\_35\_4 									& 58 			& {\bf 89}\\
%tip\_bmc:sat\_nusmv.tcas-t.5.B  					& 314 845 		& {\bf 26 667 126}\\
%total-10-13-s 									& 99 731 		& {\bf 15 390 618}\\
%\hline
%\end{tabular}
%  \caption{SAT Challenge 2012 - Application benchmarks}
%    \label{tab:indusmodels1h}
%\end{scriptsize}
%\end{table}
%
%
% 
%\begin{figure}[htbp]
%\centering
%    \includegraphics[width=9cm]{FIG/bio_allmodels_ems.pdf}
%  \caption{Comparaison of $BR$-$Enum$ and $BC$-$Enum$ on sequence mining (Bio instances)}
% \label{fig:biouser}
%\end{figure}
%
%\begin{figure}[htbp]
%\centering
%    \includegraphics[width=9cm]{FIG/iuser_allmodels_ems.pdf}  
%  \caption{Comparaison of $BR$-$Enum$ and $BC$-$Enum$ on sequence mining (User instances)}
% \label{fig:sp}
%\end{figure}

In the second experiment, we consider our  SAT-Based encoding of the sequence mining problem (EMS). The datasets are taken from two application domains:
\begin{itemize}
\item {\it Bioinformatics}:   proteinic data encoded as a sequence of  amino-acid of arbitrary length\footnote{http://www.biomedcentral.com/1471-2105/11/175/additional/}. 
\item {\it Computer security}:  user data drawn from the
command histories of UNIX computer users\footnote{http://kdd.ics.uci.edu/databases/UNIX\_user\_data/} \cite{Lane98}.  These data encode the tcsh history files and has been parsed and command names, flags, and shell metacharacters have been preserved.  Additionally, $**SOF**$ and $**EOF**$ tokens have been inserted at the start and end of
shell sessions, respectively. The data can be seen as a sequence of Unix commands.  
\end{itemize}	
This experiment aims to analyze the behavior of our proposed algorithm on SAT instances encoding real world enumeration problems. Figure \ref{fig:biouser} shows the evolution of the computation time when varying the value of the quorum $\lambda$. 
As we can see, on both {\tt Bioinformatics} (Figure \ref{fig:biouser}) or {\tt Computer security} (Figure \ref{fig:sp}) instances, $BR$-$Enum$ approach leads to  important improvements in terms of CPU time.

In Table \ref{tab:highlighEnumSeq} we give more detailed results on some instances. As expected, higher is the number of models, better are the performances of $BR$-$Enum$.  Contrary the SAT instances taken from the SAT 2012 challenge, on SAT instances encoding sequence mining problems with only one single model,  $BR$-$Enum$ and $BC$-$Enum$ present similar behavior. This clearly demonstrate that our approach $BR$-$Enum$ is even better for formula with a huge number of models. It also illustrates that restarts strategies used in SAT solving and inhibited in our proposed approach is clearly not suitable for model enumeration. 
%The number of instances where BC-Enum outperforms BR-Enum is very limited. For Bioinformatics instances, there exists only two instances {\tt bio qr.60 sz.1200.ems} and 
%{\tt bio qr.85 sz.1200.ems}.

%\begin{table}
%\begin{scriptsize}
%\centering
%\begin{tabular}{|l|c|c|c|}
%\hline
%instance & \# M &  BC-Enum  & BR-Enum  \\
% & &  (time in seconds) & (time in seconds) \\
%\hline\hline
% iuser\_qr.10\_sz.600.ems & 3478 & 4815.30 &  {\bf 2879.77} \\
% iuser\_qr.15\_sz.600.ems & 576 & 1490.95 &  {\bf 772.55} \\
% iuser\_qr.20\_sz.600.ems & 265 & 673.85 &  {\bf 432.14 }\\
% iuser\_qr.25\_sz.600.ems & 139 & 380.87 &  {\bf 209.10} \\
% iuser\_qr.30\_sz.600.ems & 65 & 167.77 &  {\bf 96.74} \\
% iuser\_qr.35\_sz.600.ems & 20 & 62.98 &  {\bf 47.19} \\
% iuser\_qr.40\_sz.600.ems & 9 & 59.09 &  {\bf 55.91} \\
% iuser\_qr.45\_sz.600.ems & 4 & 46.40 &  {\bf 39.45} \\
% iuser\_qr.50\_sz.600.ems & 2 & 32.99 &  {\bf 30.54} \\
% iuser\_qr.55\_sz.600.ems & 2 & {\bf 35.22} &  50.23 \\
% \hline\hline
%bio\_qr.15\_sz.1200.ems & 1183 & -- & {\bf8189.52 } \\
%bio\_qr.20\_sz.1200.ems & 362 & 7740.61 & {\bf 3082.18}  \\
%bio\_qr.25\_sz.1200.ems & 196 & 6302.09 & {\bf 2039.85}  \\
%bio\_qr.30\_sz.1200.ems & 83 & 3006.54 & {\bf 1082.10}  \\
%bio\_qr.35\_sz.1200.ems & 39 &  1864.40 & {\bf 1433.08}  \\
%bio\_qr.40\_sz.1200.ems & 21 & 1583.22 & {\bf 1157.70}  \\
%bio\_qr.45\_sz.1200.ems & 16 & {\bf 1115.55} & 1465.26  \\
%bio\_qr.50\_sz.1200.ems & 13 & 1327.75 & {\bf 1010.37}  \\
%bio\_qr.55\_sz.1200.ems & 10 & 1000.47 & {\bf 641.64 } \\
%bio\_qr.60\_sz.1200.ems & 7 & {\bf 564.45} & 638.58  \\
%bio\_qr.65\_sz.1200.ems & 7 & 655.83 & {\bf 622.79}  \\
%bio\_qr.70\_sz.1200.ems & 7 & 618.75 & {\bf 483.18}  \\
%bio\_qr.75\_sz.1200.ems & 5 & 465.74 & {\bf 430.51}  \\
%bio\_qr.80\_sz.1200.ems & 4 & 313.38 & {\bf 182.36}  \\
%bio\_qr.85\_sz.1200.ems & 3 & {\bf 223.45} & 235.78  \\
%bio\_qr.90\_sz.1200.ems & 3 & 195.06 & {\bf 156.51}  \\
%bio\_qr.95\_sz.1200.ems & 1 & {\bf 124.95} & 127.82  \\
%%& &&\\
% \hline\hline
%bio\_qr.100\_1101\_sz.1200 & 1 & 120.18 & {\bf 119.64}  \\
%bio\_qr.105\_1096\_sz.1200 & 1 & {\bf 114.50 }& 119.04  \\
%bio\_qr.110\_1091\_sz.1200 & 1 & 105.00 & {\bf 101.09}  \\
%bio\_qr.115\_1086\_sz.1200 & 1 & {\bf 149.21} & 154.02  \\
%bio\_qr.120\_1081\_sz.1200 & 1 & {\bf 146.09} & 159.14  \\
%bio\_qr.125\_1076\_sz.1200 & 1 & {\bf 149.64} & 150.70  \\
%bio\_qr.130\_1071\_sz.1200 & 1 & 99.68 & {\bf 98.74}  \\
%bio\_qr.135\_1066\_sz.1200 & 1 & 139.25 & {\bf 134.84}   \\
%bio\_qr.140\_1061\_sz.1200 & 1 & {\bf 98.31} & 100.99  \\
%bio\_qr.145\_1056\_sz.1200 & 1 & 147.37 & {\bf 100.63}  \\
%bio\_qr.150\_1051\_sz.1200 & 1 & 96.97 & {\bf 91.17}  \\
%bio\_qr.155\_1046\_sz.1200 & 1 & {\bf 159.40} & 163.51  \\
%bio\_qr.160\_1041\_sz.1200 & 1 & 128.77 & {\bf 107.71}  \\
%bio\_qr.165\_1036\_sz.1200 & 1 & {\bf 136.67} & 140.30  \\
%bio\_qr.170\_1031\_sz.1200 & 1 & {\bf 68.14} & 82.91  \\
%bio\_qr.175\_1026\_sz.1200 & 1 & {\bf 49.07} & 57.72 \\
%\hline
%\end{tabular}
%  \caption{Highlight result on {\tt proteinic data} and {\tt user data} instances}
%   \label{tab:highlighEnumSeq}
%\end{scriptsize}
%\end{table}


As a summary, our proposed $BR$-$Enum$ approach is clearly an interesting adaptation of CDCL-Based SAT solvers for model enumeration. The experiments clearly demonstrate that $BR$-$Enum$ outperforms one of the most known CDCL-Based Enumeration Solver $BC$-$Enum$ both in term of CPU time and number of found models. Under a given time limit, $BR$-$Enum$  allows us to output significantly more models than $BC$-$Enum$. 
 \section{Acknowledgments}
This work is supported by the French ANR projects TUPLES "Tractability for Understanding and Pushing forward the Limits of Efficient Solvers" and  DAG "Declarative approaches for enumerating interesting patterns". 


%reductions of the set of decisions such that the model associated to a given model.   

%for deducing the smallest sequence of decision associated to can be improved using the 

% EOF

defs.tex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Definition de nouvelles commandes % 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\stc}[1]{\mbox{$\langle\,#1\/\, \rangle$}}
\newcommand{\cro}[1]{\mbox{$\[\,#1\/ \]$}}
\newcommand{\ens}[1]{\mbox{$\{\,#1\/\,\}$}}
\newcommand{\quo}[1]{``#1''}
\newcommand{\egaldef}{\mbox{$\stackrel{\rm def}{=}$}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Definition de symboles logiques utiles %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% symboles de BI

\newcommand{\BImtop}{I} % unite conjonctive multiplicative 
\newcommand{\BIatop}{\top} % unite conjonctive additive
\newcommand{\BIabot}{\bot} % unite disjonctive additive
\newcommand{\BImand}{\ast} % conjonction multiplicative
\newcommand{\BImimp}{-\hspace{-1ex}\ast} % implication multiplicative
\newcommand{\BIaand}{\wedge} % conjonction additive
\newcommand{\BIaimp}{\rightarrow} % implication additive
\newcommand{\BIaor}{\vee} % disjonction additive
\newcommand{\BImnul}{\emptyset_m} % bunch multiplicatif vide
\newcommand{\BIanul}{\emptyset_a} % bunch additif vide
\newcommand{\BIax}{ax} % nom de la regle axiome
\newcommand{\BIcut}{cut} % nom de la regle de coupure
\newcommand{\BIweak}{w} % nom de la regle d'affaiblissement
\newcommand{\BIcont}{c} % nom de la regle de contraction
\newcommand{\BIequi}{\equiv} % nom de la regle d'equivalence structurelle

\newcommand{\BIvarp}{L} % lettre pour l'ensemble de variables propositionnelles

%\BIprop[varprop]: ensemble des propositions de BI issues de varprop
\newcommand{\BIprop}[1][\BIvarp]{{\cal P}({#1})}

% symboles de MILL

\newcommand{\LLtimes}{\otimes}
\newcommand{\LLwith}{\&}
\newcommand{\LLpar}{\rotatebox[origin=c]{180}{\rm \LLwith}}
\newcommand{\LLimp}{-\hspace{-1ex}\circ}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Definition d'abbreviations utiles %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\IL}{{\bf IL}}
\newcommand{\LL}{{\bf LL}}
\newcommand{\MLL}{{\bf MLL}}
\newcommand{\ILL}{{\bf ILL}}
\newcommand{\MILL}{{\bf MILL}}
\newcommand{\BIc}{{\bf \BI$^{\bot}$}}
\newcommand{\BI}{{\bf BI}}
\newcommand{\TBI}{{\bf TBI}}
\newcommand{\NBI}{{\bf NBI}}
\newcommand{\NBIA}{\NBI$^{\heartsuit}$}
\newcommand{\LBI}{{\bf LBI}}
\newcommand{\LBIc}{{\bf LBI$^{\bot}$}}
\newcommand{\LBIA}{\LBI$^{\heartsuit}$}
\newcommand{\KRM}{{\bf Krm}}
\newcommand{\KRMs}{{\bf Krms}}
\newcommand{\KRI}{{\bf Kri}}
\newcommand{\KRIs}{{\bf Kris}}
\newcommand{\bunch}{\quo{bunch}}
\newcommand{\bunches}{\quo{bunches}}
\newcommand{\Bunch}{\quo{Bunch}}
\newcommand{\Bunches}{\quo{Bunches}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Macros pour dessiner les sequents %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% consequences syntaxiques |-

\newcommand{\seq}[3][]{\mbox{${#2}\vdash_{#1}{#3}$}}
\newcommand{\seqBI}[2]{\seq[BI]{#1}{#2}}
\newcommand{\seqIL}[2]{\seq[IL]{#1}{#2}}
\newcommand{\seqMILL}[2]{\seq[MILL]{#1}{#2}}

\newcommand{\notseq}[3][]{\mbox{${#2}\not\vdash_{#1}{#3}$}}
\newcommand{\notseqBI}[2]{\notseq[BI]{#1}{#2}}
\newcommand{\notseqIL}[2]{\notseq[IL]{#1}{#2}}
\newcommand{\notseqMILL}[2]{\notseq[MILL]{#1}{#2}}

% consequences semantiques |=

\newcommand{\csm}[3][]{\mbox{${#2}\models_{#1}{#3}$}}
\newcommand{\csmBI}[2]{\csm[BI]{#1}{#2}}
\newcommand{\csmIL}[2]{\csm[IL]{#1}{#2}}
\newcommand{\csmMILL}[2]{\csm[MILL]{#1}{#2}}

\newcommand{\notcsm}[3][]{\mbox{${#2}\not\models_{#1}{#3}$}}
\newcommand{\notcsmBI}[2]{\notcsm[BI]{#1}{#2}}
\newcommand{\notcsmIL}[2]{\notcsm[IL]{#1}{#2}}
\newcommand{\notcsmMILL}[2]{\notcsm[MILL]{#1}{#2}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Notations pour les structures semantiques %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\wld}[1][m]{#1} % lettre pour un monde
\newcommand{\Wld}[1][M]{#1} % lettre pour un ensemble de mondes

\newcommand{\krm}[1][M]{{\cal #1}} % lettre pour un KRM
\newcommand{\kri}[1][I]{{\cal #1}} % lettre pour une KRI=KRM+forcing
\newcommand{\ronb}[1][\bullet]{#1} % lettre pour l'operation de composition
\newcommand{\neus}[1][e]{#1} % lettre pour l'element neutre

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Notations pour les labels %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\neu}[1][1]{#1} % lettre pour l'element neutre
\newcommand{\ron}[1][\circ]{#1} % lettre pour l'operation de composition

\newcommand{\cst}[1][c]{#1} % lettre pour une constante
\newcommand{\Cst}[1][C]{#1} % ensemble de constantes
\newcommand{\Csti}[2][\Cst]{#1_{#2}}

\newcommand{\var}[1][v]{#1} % lettre pour une variable
\newcommand{\Var}[1][V]{#1} % lettre pour un ensemble de variables
\newcommand{\Vari}[2][\Var]{#1_{#2}}

\newcommand{\C}{\mathrm{\Cst}}
\newcommand{\CV}{\mathrm{\Cst\Var}}
\newcommand{\CVi}[1]{\mathrm{\Csti{#1}\Vari{#1}}}

\newcommand{\clos}[1]{\overline{#1}}

\newcommand{\lap}[1][P]{\mathrm{#1}} % lettre pour un alphabet propositionnel
\newcommand{\PROP}[1][{{\cal P}}]{#1} % langage propositionnel
\newcommand{\PROPi}[2][\PROP]{#1_{#2}}
\newcommand{\Prop}[1][P]{#1} % ensemble de propositions
\newcommand{\Propi}[2][\Prop]{#1_{#2}}

\newcommand{\lal}[1][L]{\mathrm{#1}} % lettre pour un alphabet de labels
\newcommand{\LAB}[1][{{\cal L}}]{#1} % langage de labels
\newcommand{\LABi}[2][\LAB]{#1_{#2}}
\newcommand{\LABC}[1][{\clos{\cal L}}]{#1} % langage de labels
\newcommand{\LABCi}[2][\LABC]{#1_{#2}}

\newcommand{\lab}[1][l]{#1} % lettre pour un label
\newcommand{\Lab}[1][L]{#1} % ensemble de labels
\newcommand{\Labi}[2][\Lab]{#1_{#2}}

\newcommand{\kon}[1][k]{#1} % lettre pour une contrainte
\newcommand{\Kon}[1][K]{#1} % ensemble de contraintes
\newcommand{\Koni}[2][\Kon]{#1_{#2}} % ensemble de contraintes
\newcommand{\KON}[1][{{\cal K}}]{#1} % langage de contraintes
\newcommand{\KONi}[2][\KON]{#1_{#2}} % langage de contraintes
\newcommand{\KONC}[1][{\clos{\cal K}}]{#1} % langage de contraintes
\newcommand{\KONCi}[2][\KONC]{#1_{#2}} % langage de contraintes

\newcommand{\KLi}[1]{\LAB\KONi{\mathrm{#1}}}

\newcommand{\K}{\Kon}
\newcommand{\Ki}[1]{\Kon_{#1}}

\newcommand{\Laa}[1][{{\cal L}}]{\widetilde{#1}} % algebre de labels
\newcommand{\Laai}[2][\Laa]{#1_{#2}} % algebre de labels

\newcommand{\kleqs}{\sqsubseteq} % symbole d'ordre plus petit que
\newcommand{\kleq}{\leq} % symbole d'ordre plus petit que
\newcommand{\kgeq}{\geq} % symbole d'ordre plus grand que

\newcommand{\ass}[1][as]{#1} % lettre pour une assertion
\newcommand{\Ass}[1][As]{#1} % lettre pour un ensemble d'assertions
\newcommand{\Assi}[2][\Ass]{#1_{#2}} % lettre pour un ensemble d'assertions
\newcommand{\AssC}[1][{\clos{\Ass}}]{#1}

\newcommand{\obl}[1][rq]{#1} % lettre pour  une obligation
\newcommand{\Obl}[1][Rq]{#1} % lettre pour un ensemble d'obligations
\newcommand{\Obli}[2][\Obl]{#1_{#2}} % lettre pour un ensemble d'obligations

% \kontr[nom]{label1}{label2} fabrique une contrainte 'l1<=l2' 
\newcommand{\kontr}[3][\kleq]{\mbox{$#2#1#3$}}
\newcommand{\kontrb}[3][\kleq]{\fbox{$#2#1#3$}}

\newcommand{\kontrs}[3][\kleqs]{\mbox{$#2#1#3$}}
\newcommand{\kontrsb}[3][\kleqs]{\fbox{$#2#1#3$}}

% \asser[indice]{l1}{l2} fabrique une assertion ICindice: l1 <= l2
\newcommand{\asser}[3][]{\kontr{\ass_{#1}:#2}{#3}}

% \asserb[indice]{l1}{l2} fabrique une assertion ICindice: l1 <= l2 et
%                         met cette assertion dans une boite
\newcommand{\asserb}[3][]{\kontrb{\ass_{#1}:#2}{#3}}

% \oblig[indice]{l1}{l2} fabrique une obligation RCindice: l1 <= l2
\newcommand{\oblig}[3][]{\kontr{\obl_{#1}:#2}{#3}}

% \obligb[indice]{l1}{l2} fabrique une obligation RCindice: l1 <= l2 et
%                         met cette obligation dans une boite
\newcommand{\obligb}[3][]{\kontrb{\obl_{#1}:#2}{#3}}

\newcommand{\LHS}[1]{LHS(#1)}

\newcommand{\RHS}[1]{RHS(#1)}


\newcommand{\subl}{\prec}
\newcommand{\subleq}{\preceq}
\newcommand{\Sublab}{{\cal P}}
\newcommand{\reml}{\backslash}
\newcommand{\garrow}{\rightarrowtriangle}
\newcommand{\qqquad}{\quad\quad\quad}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Notations pour les propositions %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% lettres pour nommer les variables propositionnelles
\newcommand{\vp}[1][A]{#1}
\newcommand{\vpA}[1][A]{#1}
\newcommand{\vpB}[1][B]{#1}
\newcommand{\vpC}[1][C]{#1}
\newcommand{\vpD}[1][D]{#1}
\newcommand{\vpE}[1][E]{#1}

% lettres pour nommer les meta-variables propositionnelles
\newcommand{\VP}[1][A]{#1}
\newcommand{\VPX}[1][X]{#1}
\newcommand{\VPA}[1][A]{#1}
\newcommand{\VPB}[1][B]{#1}
\newcommand{\VPC}[1][C]{#1}
\newcommand{\VPD}[1][D]{#1}
\newcommand{\VPE}[1][E]{#1}


% \fl{formule}{label} fabrique une formule labellisee
\newcommand{\fl}[2]{\mbox{${#1}:{#2}$}}

% \fls{polarite}{formule}{label} fabrique une formule polarisee labellisee 
\newcommand{\fls}[3]{\mbox{$#1\;\fl{#2}{#3}$}} 

% lettre pour un ensemble de formules polarisees labellisees
\newcommand{\Fls}[1][{{\cal F}}]{#1} 
\newcommand{\Flsi}[2][\Fls]{#1_{#2}}

% \cnx{formule}{label_T}{label_F}: ecriture d'une connexion
\newcommand{\cnx}[3]{\stc{\fls{T}{#1}{#2},\fls{F}{#1}{#3}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Notations diverses                   %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ett}[1][Es]{#1} % lettre pour les etats
\newcommand{\Ett}[1][{{\cal S}}]{#1} % lettre pour les ensembles d'etats 
\newcommand{\Etti}[2][\Ett]{#1_{#2}} % lettre pour les ensembles d'etats 

\newcommand{\cfg}[1][t]{#1} % lettre pour une configuration
\newcommand{\Cfg}[1][{{\cal T}}]{#1} % ensemble de configurations (tableau)
\newcommand{\Cfgi}[2][\Cfg]{#1_{#2}} % ensemble de configurations (tableau)

% \conf{Etats}{Cst}{Var}{Ass}{0bl} fabrique une configuration
\newcommand{\confs}[4]{\stc{#1,#2,#3,#4}} 

% \conf{Etats}{Cst}{Var}{Ass}{0bl} fabrique une configuration
\newcommand{\conf}[5]{\stc{#1,#2,#3,#4,#5}} 

\newcommand{\sig}[1][\sigma]{#1} % lettre pour une valuation
\newcommand{\Sig}[1][\Sigma]{#1} % ensemble de valuations
\newcommand{\Sigi}[2][\Sig]{#1_{#2}} % ensemble de valuations

\newcommand{\ome}[1][\omega]{#1} % lettre pour une assignation de constantes
\newcommand{\Ome}[1][\Omega]{#1} % ensemble d'assignations de constantes
\newcommand{\Omei}[2][\Ome]{#1_{#2}} % ensemble d'assignations de constantes

\newcommand{\tet}[1][\theta]{#1} % lettre pour une assignation de variables
\newcommand{\Tet}[1][\Theta]{#1} % ensemble d'assignations de variables
\newcommand{\Teti}[2][\Tet]{#1_{#2}} % ensemble d'assignations de variables

\newcommand{\interCV}[3]{\|#3\|_{#1}^{#2}} % interpretation
\newcommand{\inter}[1]{\interCV{}{}{#1}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Macros pour les tableaux semantiques %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% \coche[indice] insere une marke de coche indicee devant une formule
\newcommand{\coche}[1][]{\surd_{#1}\;\;}

% \tabvgap[vgap] sets the length of the vertical space between two
% consecutive nodes of the tableau-tree ; the default is 4mm  
\newcommand{\tabvgap}[1][3mm]{\setlength{\GapDepth}{#1}}

% \tabhgap[hgap] sets the length of the horizontal space between two
% adjacent nodes of the tableau-tree ; the default is 12mm  
\newcommand{\tabhgap}[1][1mm]{\setlength{\GapWidth}{#1}}

% \begin{tableau} ... \end{tableau} definit un environnement 
% de dessin d'un tableau semantique sous forme d'arbre binaire.
%\newenvironment{tableau}{\begin{array}{c}}{\end{array}}
\newenvironment{tableau}{}{}

% \tbloc[c|l|r]{lignes} regroupe plusieurs lignes en un bloc ;
% le parametre optionel permet de centrer ou de justifier les lignes
\newcommand{\tbloc}[1]{$\begin{array}{c} #1 \end{array}$}

\newcommand{\tclos}[1]{\tbloc{#1 \\ \times}}

% \tinfI{racine}{fils1}{fils2}
\newcommand{\tinfI}[4][0pt]
{\begin{bundle}{#2}
 \chunk{\tbloc{#3 \\ #4}}
 \end{bundle}
}

% \tinfIc{contrainte}{racine}{fils1}{fils2}
\newcommand{\tinfIc}[5][0pt]
{\begin{bundle}{#3}
 \chunk
 {
   \begin{bundle}{#2}
   \chunk{\tbloc{#4 \\ #5}}
   \end{bundle}
 }
 \end{bundle}
}

% \tinfII[espace_branches]{racine}{fils1}{fils2}
\newcommand{\tinfII}[4][2cm]
{\begin{bundle}{#2}
 \chunk
 { \begin{bundle}{}
   \chunk{\makebox[#1]{#3}}
   \chunk{\makebox[#1]{#4}}
   \end{bundle}
 }
 \end{bundle}
}

% \tinfIIc[espace_branches]{contrainte}{racine}{fils1}{fils2}
\newcommand{\tinfIIc}[5][2cm]
{\begin{bundle}{#3}
 \chunk
 { \begin{bundle}{#2}
   \chunk
   {
     \begin{bundle}{}
     \chunk{\makebox[#1]{#4}}
     \chunk{\makebox[#1]{#5}}
     \end{bundle}
   }
   \end{bundle}
 }
 \end{bundle}
}

% ajouts du 18/03/2001:

\newcommand{\Br}{\ett} % lettre pour une branche
\newcommand{\Tr}{{\cal T}} % lettre pour un arbe
\newcommand{\DG}{DG} % lettre pour un graphe de dependance
\newcommand{\garrowp}{\stackrel{\star}{\garrow}}
\newcommand{\Nod}{Nod}
\newcommand{\Arr}{Arr}

symbols.tex
% common

\let\myinfty=\infty
\def\infty{\text{BUG}}
\newcommand{\naturals}{\mathalpha{\dN}}
\newcommand{\nats}{\ensuremath\naturals}
\newcommand{\natb}{\ensuremath{\overline\naturals}}
\newcommand{\natbs}{\ensuremath{\overline\naturals^\star}}
\newcommand{\bb}{\triangle}
\newcommand{\funarrow}{\mathbin{\rightarrow}}

% logics
\newcommand{\fst}[1]{\texttt{fst}(#1)}
\newcommand{\at}{\texttt{ at }}
\newcommand{\snd}[1]{\texttt{snd}(#1)}
\newcommand{\dia}[1]{\texttt{Dia}(#1)}
\newcommand{\bt}[1]{\texttt{Box}(#1)}
\newcommand{\ubt}[1]{\texttt{Unbox}(#1)}
%\newcommand{\case}{\texttt{Case }}
\newcommand{\of}{\texttt{ of }}
\newcommand{\inr}[1]{\texttt{inr}(#1)}
\newcommand{\inl}[1]{\texttt{inl}(#1)}
\newcommand{\lgc}[1]{\mathalpha{\mathsf{#1}}}
\newcommand{\il}{\ensuremath{\lgc{IL}}}
\newcommand{\sat}{\ensuremath{\lgc{SAT}}}
\newcommand{\ssat}{\ensuremath{\lgc{SUPPSAT}}}
\newcommand{\fsat}{\ensuremath{\lgc{FREQSAT}}}
\newcommand{\gis}{\ensuremath{\lgc{G_{IS5}}}}
\newcommand{\gism}{\ensuremath{\lgc{G^-_{IS5}}}}
\newcommand{\ndis}{\ensuremath{\lgc{ND_{IS5}}}}
\newcommand{\mipq}{\ensuremath{\lgc{MIPQ}}}
\newcommand{\mipc}{\ensuremath{\lgc{MIPC}}}
\newcommand{\ipl}{\ensuremath{\lgc{IPL}}}
\newcommand{\ik}{\ensuremath{\lgc{IK}}}
\newcommand{\is}{\ensuremath{\lgc{IS5}}}
\newcommand{\sff}{\ensuremath{\lgc{S5}}}
\newcommand{\imf}{\ensuremath{\lgc{IM5}}}
\newcommand{\isf}{\ensuremath{\lgc{IS4}}}
\newcommand{\his}{\ensuremath{\lgc{HyIS5}}}
\newcommand{\gsf}{\ensuremath{\lgc{GS5}}}
\newcommand{\pil}{\ensuremath{\lgc{PIL}}}
\newcommand{\ihl}{\ensuremath{\lgc{IHL}}}
\newcommand{\chl}{\ensuremath{\lgc{CHL}}}
\newcommand{\cl}{\ensuremath{\lgc{CL}}}
\newcommand{\lc}{\ensuremath{\lgc{LC}}}
\newcommand{\hlc}{\ensuremath{\lgc{HLC}}}
\newcommand{\wmlc}{\ensuremath{\lgc{WMLC}}}
\newcommand{\ag}{\ensuremath{\lgc{Assign}}}
\newcommand{\lab}{\ensuremath{\lgc{Lab}}}
\newcommand{\lcx}[1]{\ensuremath{\lgc{LC}_{#1}}}
\newcommand{\lcn}{\lcx n}
\newcommand{\gmn}{\ensuremath{\lgc{GM}_{n}}}
\newcommand{\gm}{\ensuremath{\lgc{GM}}}
\newcommand{\wgm}{\ensuremath{\lgc{WGM}}}
\newcommand{\ghn}{\ensuremath{\lgc{GH}_{n}}}
\newcommand{\gh}{\ensuremath{\lgc{GH}}}
\newcommand{\wgh}{\ensuremath{\lgc{WGH}}}
\newcommand{\lci}{\lcx \smax}

\newcommand{\two}{\ensuremath{\{0,1\}}}

\newcommand{\rweak}{\mathrm{Weak}_L}
\newcommand{\rcut}{\mathrm{Cut}}
\newcommand{\rimp}{\limp_L^1}
\newcommand{\rcm}{\lconj_M}
\newcommand{\rdm}{\ldisj_M}
\newcommand{\rim}{\limp_M}

% sets

\newcommand{\set}[1]{\ensuremath{\mathalpha{\cal #1}}}

% semantic

\newcommand{\smax}{\mathalpha{\myinfty}}
\newcommand{\semset}[1]{\mathalpha{\overline{{\lbrack}0,{#1}{)}}}}
\newcommand{\sset}{\semset{n}}
\newcommand{\fset}{\varset\funarrow\semset{n}}

\renewcommand{\nleq}{\mathrel{\nleqslant}}
\renewcommand{\leq}{\mathrel{\leqslant}}
\renewcommand{\geq}{\mathrel{\geqslant}}
\newcommand{\eq}{\mathrel{\simeq}}
\newcommand{\tr}{\mathrel{\triangleright}}

\newcommand{\sem}[1]{\mathopen{\lbrack\hskip-1.3pt\lbrack}#1\mathclose{\rbrack\hskip-1.3pt\rbrack}}
\newcommand{\semu}[1]{\mathopen{\lceil\hskip-3pt\lceil}#1\mathclose{\rceil\hskip-3pt\rceil}}
\newcommand{\semd}[1]{\mathopen{\lfloor\hskip-3pt\lfloor}#1\mathclose{\rfloor\hskip-3pt\rfloor}}

\newcommand{\imp}{\mathbin{\rightarrowtriangle}}
\newcommand{\cgarr}[1]{\mathbin{\rightarrow_{#1}}}
% logic

\newcommand{\lconj}{\ensuremath{\mathbin{\wedge}}}
\newcommand{\ldisj}{\ensuremath{\mathbin{\vee}}}
\newcommand{\limp}{\ensuremath{\mathbin{\supset}}}
\newcommand{\lbot}{\ensuremath{\mathalpha{\bot}}}

\newcommand{\seq}{\mathbin{\vdash}}
\newcommand{\dv}{\mathbin{\rhd}}
% syntax

\newcommand{\varset}{\ensuremath{\mathalpha{\mathsf{Var}}}}
\newcommand{\formset}{\ensuremath{\mathalpha{\mathsf{Form}}}}
\newcommand{\plset}{\ensuremath{\mathalpha{\mathsf{PL}}}}
\newcommand{\propset}{\ensuremath{\mathalpha{\mathsf{Prop}}}}
\newcommand{\labset}{\ensuremath{\mathalpha{\mathsf{Lab}}}}
\newcommand{\relset}{\ensuremath{\mathalpha{\mathsf{Rel}}}}

\newcommand{\btop}{\ensuremath{\mathalpha{\diamondsuit}}}
\newcommand{\bbot}{\ensuremath{\mathalpha{\boxempty}}}

\newcommand{\bctx}[1]{\ensuremath{\mathalpha{{#1}_{\diamondsuit}}}}

\newcommand{\gcon}{\mathbin{\oast}}
\newcommand{\id}[1]{\ensuremath{\mathalpha{\cal X}_{#1}}}
\newcommand{\dt}[1]{\ensuremath{\delta^#1}}

% boolean logic

\newcommand{\boolneg}[1]{\mathalpha{\overline{#1}}}

% graphs

\newcommand{\rarr}{\ensuremath{\mathbin{\Rightarrow}}}
\newcommand{\garr}{\ensuremath{\mathbin{\rightarrow}}}
\newcommand{\graph}[1]{\mathalpha{\cal #1}}
\newcommand{\cls}[1]{\mathalpha{[#1]}}
\newcommand{\arr}{\mathbin{\rightarrow}}

% matrices

\newcommand{\trace}{\mathalpha{\text{tr}}}
\newcommand{\crarr}[1]{\mathbin{\rarr_{#1}}}

AllModelsV3.bbl
\begin{thebibliography}{10}

\bibitem{agrawal93}
Rakesh Agrawal, Tomasz Imieli\'{n}ski, and Arun Swami.
\newblock Mining association rules between sets of items in large databases.
\newblock In {\em Proceedings of the 1993 ACM SIGMOD International Conference
  on Management of Data}, SIGMOD '93, pages 207--216, New York, NY, USA, 1993.
  ACM.

\bibitem{Asin11}
Roberto Asin, Robert Nieuwenhuis, Albert Oliveras, and Enric
  Rodriguez-Carbonell.
\newblock Cardinality networks: a theoretical and empirical study.
\newblock {\em Constraints}, 16(2):195--221, 2011.

\bibitem{HandbookSAT}
Armin Biere, Marijn J.~H. Heule, Hans van Maaren, and Toby Walsh, editors.
\newblock {\em Handbook of Satisfiability}, volume 185 of {\em Frontiers in AI
  and Applications}.
\newblock IOS Press, 2009.

\bibitem{Chauhan03usingsat}
Pankaj Chauhan, Edmund~M. Clarke, and Daniel Kroening.
\newblock Using sat based image computation for reachability analysis.
\newblock Technical report, Technical Report CMU-CS-03-151, 2003.

\bibitem{CoqueryJSS12}
Emmanuel Coquery, Sa\"{\i}d Jabbour, Lakhdar Sa\"{\i}s, and Yakoub Salhi.
\newblock A sat-based approach for discovering frequent, closed and maximal
  patterns in a sequence.
\newblock In {\em Proceedings of the 20th European Conference on Artificial
  Intelligence (ECAI'12)}, pages 258--263, 2012.

\bibitem{Davis62}
M.~Davis, G.~Logemann, and D.~W. Loveland.
\newblock A machine program for theorem-proving.
\newblock {\em Comm. of the ACM}, 5(7):394--397, 1962.

\bibitem{MartinGebser07}
Martin Gebser, Benjamin Kaufmann, André Neumann, and Torsten Schaub.
\newblock Conflict-driven answer set enumeration.
\newblock In Chitta Baral, Gerhard Brewka, and John Schlipf, editors, {\em
  Logic Programming and Nonmonotonic Reasoning}, volume 4483 of {\em Lecture
  Notes in Computer Science}, pages 136--148. Springer Berlin Heidelberg, 2007.

\bibitem{GunsNR11}
T.~Guns, S.~Nijssen, and L.~De Raedt.
\newblock Itemset mining: A constraint programming perspective.
\newblock {\em Artif. Intell.}, 175(12-13):1951--1983, 2011.

\bibitem{abs-1207-6253}
Rui Henriques, In{\^e}s Lynce, and Vasco~M. Manquinho.
\newblock On when and how to use sat to mine frequent itemsets.
\newblock {\em CoRR}, abs/1207.6253, 2012.

\bibitem{JabbourLSS14}
Sa{\"{\i}}d Jabbour, Jerry Lonlac, Lakhdar Sais, and Yakoub Salhi.
\newblock Extending modern {SAT} solvers for models enumeration.
\newblock In {\em Proceedings of the 15th {IEEE} International Conference on
  Information Reuse and Integration, {IRI} 2014, Redwood City, CA, USA, August
  13-15, 2014}, pages 803--810, 2014.

\bibitem{JabbourSS13seq}
Sa\"{\i}d Jabbour, Lakhdar Sais, and Yakoub Salhi.
\newblock Boolean satisfiability for sequence mining.
\newblock In {\em 22nd ACM International Conference on Information and
  Knowledge Management (CIKM'13)}, pages 649--658. ACM, 2013.

\bibitem{JabbourSS13topk}
Sa\"{\i}d Jabbour, Lakhdar Sais, and Yakoub Salhi.
\newblock The top-k frequent closed itemset mining using top-k sat problem.
\newblock In {\em European Conference on Machine Learning and Knowledge
  Discovery in Databases (ECML/PKDD'03)}, pages 403--418, 2013.

\bibitem{Jeroslow90}
R.~G. Jeroslow and J.~Wang.
\newblock Solving propositional satisfiability problems.
\newblock {\em Annals of Mathematics and Artificial Intelligence}, 1:167--187,
  1990.

\bibitem{Jin05efficientconflict}
Hoonsang Jin, Hyojung Han, and Fabio Somenzi.
\newblock Efficient conflict analysis for finding all satisfying assignments of
  a boolean circuit.
\newblock In {\em In TACAS'05, LNCS 3440}, pages 287--300. Springer, 2005.

\bibitem{Marques-Silva96}
J.~P. Marques-Silva and K.~A. Sakallah.
\newblock {GRASP - A New Search Algorithm for Satisfiability}.
\newblock In {\em Proceedings of IEEE/ACM CAD}, pages 220--227, 1996.

\bibitem{McMillan02}
Kenneth~L. McMillan.
\newblock Applying sat methods in unbounded symbolic model checking.
\newblock In {\em Proceedings of the 14th International Conference on Computer
  Aided Verification (CAV'02)}, pages 250--264, 2002.

\bibitem{morgado05silva}
Ant\'onio~R. Morgado and Jo\~ao~P. Marques-Silva.
\newblock {Good Learning and Implicit Model Enumeration}.
\newblock In {\em International Conference on Tools with Artificial
  Intelligence (ICTAI'2005)}, pages 131--136. IEEE, 2005.

\bibitem{Raedt08}
L.~De Raedt, T.~Guns, and S.~Nijssen.
\newblock Constraint programming for itemset mining.
\newblock In {\em ACM SIGKDD}, pages 204--212, 2008.

\bibitem{SilvaL07}
J.~P.~Marques Silva and I.~Lynce.
\newblock Towards robust cnf encodings of cardinality constraints.
\newblock In {\em CP}, pages 483--497, 2007.

\bibitem{Sinz05}
C.~Sinz.
\newblock Towards an optimal cnf encoding of boolean cardinality constraints.
\newblock In {\em CP'05}, pages 827--831, 2005.

\bibitem{tiwari2010survey}
A.~Tiwari, R.K. Gupta, and D.P. Agrawal.
\newblock A survey on frequent pattern mining: Current status and challenging
  issues.
\newblock {\em Inform. Technol. J}, 9:1278--1293, 2010.

\bibitem{Tseitin68}
G.S. Tseitin.
\newblock On the complexity of derivations in the propositional calculus.
\newblock In H.A.O. Slesenko, editor, {\em Structures in Constructives
  Mathematics and Mathematical Logic, Part II}, pages 115--125, 1968.

\bibitem{Warners96}
J.~P. Warners.
\newblock A linear-time transformation of linear inequalities into conjunctive
  normal form.
\newblock {\em Information Processing Letters}, 1996.

\bibitem{Zhang01}
L.~Zhang, C.~F. Madigan, M.~W. Moskewicz, and S.~Malik.
\newblock Efficient conflict driven learning in \protect{Boolean}
  satisfiability solver.
\newblock In {\em IEEE/ACM CAD'2001}, pages 279--285, 2001.

\end{thebibliography}
