Boolean Satisfiability for Sequence Mining Said Jabbour

In this paper, we propose a SAT-based encoding for the problem of discovering frequent, closed and maximal pat-terns in a sequence of items and a sequence of itemsets. Our encoding can be seen as an improvement of the approach proposed in [8] for the sequences of items. In this case, we show experimentally on real world data that our encoding is significantly better. Then we introduce a new extension of the problem to enumerate patterns in a sequence of item-sets. Thanks to the flexibility and to the declarative aspects of our SAT-based approach, an encoding for the sequences of itemsets is obtained by a very slight modification of that for the sequences of items. Categories and Subject Descriptors F.4.1 [Mathematical logic and formal languages]: Math-ematical Logic—Logic and constraint programming; H.2.