In this talk, we overview our contributions to data mining and more generally to the cross-fertilization between data mining, constraint programming and propositional satis ability. We will focus on three contributions. First, we show how propositional satis ability (SAT) can be used to model and solve problems in data mining. As an illustration, we present a SAT-based declarative approach for itemset, association rules and sequences mining. Then, we present an original use of data mining techniques to compress Boolean formulas. Finally, we discuss how symmetries widely investigated in Constraint Programming (CP) and Propositional Satis ability (SAT) can be extended to deal with data mining problems.