1. Amal EL HIDOURI, février 2018 - juillet 2018, Approches contraintes pour la fouille des itemsets high utility, 2018.

2. Abderrahim RACHID, février 2018 - juillet 2018, *Fouille de données textuelles*, 2018.

3. Abdesattar MHADHBI, février 2017 - juillet 2017, Approches logiques pour la compression des grands graphes, 2017.

4. Soukaine HATTAD, février 2016 - juillet 2016, Résolution des problèmes d'optimisation en SAT, 2016.

5. Abdelhamid BOUDANE, février 2015 - juillet 2015, *Fouille de données symbolique*, 2015.

6. Rym MEGHNOUS, février 2014 - juillet 2014, automatisation des systèmes de preuves éтен-dus, 2014.

7. Fares BOUDRAA, février 2014 - juillet 2014, Symétries en fouille de séquences, 2014.

8. Essid MOHAMED, février 2014 - juillet 2014, Exploitation des classes traitables pour la simplification des formules booléennes, 2011.

**Internship & Post-doc**

1. Florian LEGENDRE, septembre 2014 - avril 2015, *Fouille de données par contraintes*, Post-doc (6 mois), projet TUPLES

2. Mehdi KHIARRI, septembre 2012 - Août 2013, *Fouille de données par contraintes*, Post-doc (11 mois), projet DAG

3. Yakoub SALHI, octobre 2011 - septembre 2012, Modèles logiques pour la fouille de données, Post-doc (12 mois), projet DAG

**8.2.2 Membre de comités de programme**

— Membre du comité de programme de "The 23rd International Conference on Artificial Intelligence", IJCAI’2018, août 28 au 1 septembre, 2018, Melbourne, Sweden, 2018

— Membre du comité de programme de "The 23rd International Conference on Principles and Practice of Constraint Programming", CP’2017, août 28 au 1 septembre, 2018, Lille, France, 2018

— Membre du comité de programme de "The 23rd International Conference on Principles and Practice of Constraint Programming", CP’2017, août 28 au 1 septembre, 2017, Melbourne, Australie, 2017

— Membre du comité de programme de "The 19th International Conference on Principles and Practice of Constraint Programming", CP’2013, September 16-20, 2013, Uppsala, Suède, 2013

**8.2.3 Relecture d'articles**

**Revues** : Artificial Intelligence Journal 2017-2018, FUNDAMENTA INFORMATICAE 2017, International Journal of Artificial Intelligence Tools 2013, 2014, 2016, Journal of Experimental algorithmics 2015.

**Conférences** : CP’2013, CP’2018, IJCAI’2018, SAT’2013, CIIA’2013, ICTAI’2013, SAT’2012, JFPC’2011, ICTAI’2010, POS’2010, SAT’2010.
## 8.2.4 Expertise de projets

- Expert auprès du ministère des affaires étrangères, Projet Chili, 2012

## 8.2.5 Collaborations internationales et bourses de thèse

- Joao Marques SILVA, University College of Dublin, Ireland (2014), "Computing Prime implicant of CNF formulae" (Publié à JELIA'2014).

- Takeaki UNO, National Institute of Informatics, Tokyo, Japan. Collaboration autour de la compression de formules bolléennes par les approches de fouille de données (Publication commune à CIKM'2013).

- Clémentin Tayou NDJEMINI, Université de Schang, Cameroun. Collaboration autour de SAT et plus particulièrement sur l'intégration de la substitution de fonctions booléennes dans les solveurs SAT (Publication commune à la revue RIA en 2014). Cette collaboration a donné lieu au financement de la thèse de Jerry Lonlac par le ministère des affaires étrangères Français (soutenue en 2014)

- Youssef HAMADI, Microsoft Research Cambridge (UK) : nos collaborations ont porté sur la résolution parallèle de SAT et sur l'amélioration des solveurs SAT modernes [ECAI'2008, SAT'2008, IJCAI'2009, ICTAI'2009, CP'2010, etc.]. Le solveur ManySAT est né de cette collaboration.

- Lucas BORDEAUX, Microsoft Research Cambridge (UK) : nous avons proposé un cadre général pour l'analyse des conflits à l'origine du solveur eSAT, un des meilleurs solveurs SAT actuellement [SAT'2008].

## 8.2.6 Collaborations nationales

- Badran RADDAOUI, Télécom SudParis, SAMOVAR - CNRS UMR 5157 (CP'18, IDA'18, PAKDD'17, BigData'16, etc.)

- Salima BENBERNOU, université Paris Descartes, LIPADE. "Relaxation based SaaS for Repairing Failed Queries over the Cloud Computing" (Publié à ICEBE 2015)

- Yue MA, Université Paris Sud, Orsay, LRI : Plusieurs publications autour des mesures d'inconsistances (ECAI'2014, AAMAS'2015)

- Belaid BENHAMOU, Université d'Aix-Marseille, LSIS : Lors de la délégation CNRS de Belaid Benhamou au CRIL (2013-2014), nous avons travaillé sur les symétries en fouille de données (publication KDIR'2014)

- Emmanuel COQUERY, Université de Lyon I : Fouille de séquences par la programmation par contraintes - ANR DAG (ECAI'12, Wks ICDM'11)

## 8.2.7 Responsabilités collectives

- Membre du COS pour le recrutement d'un maître de conférences (MCF), Université d'Artois, 2016.

- Membre de la commission API pour le recrutement des Attachés Temporaires d'Enseignement et de Recherche (ATER), 2014-2016.

- Membre du conseil du laboratoire CRIL, 2013-2017.
— Co-responsable des emplois de temps, 2014-2018.
<figure><img src="image_14.png" /></figure>
Bibliographie

[Acuña et al. 2012] Vicente Acuña, Paulo Vieira Milreu, Ludovic Cottret, Al-
berto Marchetti-Spaccamela, Leen Stougie et Marie-France Sagot.
Algorithms and complexity of enumerating minimal precursor sets in genome-wide metabolic networks.
Bioinformatics, vol. 28, no. 19, pages 2474–2483, 2012. (Cité en page 13.)

[Adamcsek et al. 2006] Balázs Adamcsek, Gergely Palla, Illés J. Farkas, Imre Derényi et Tamás Vicsek. CFinder : locating cliques and overlapping modules in biological networks. Bio-informatics, vol. 22, no. 8, pages 1021–1023, 2006. (Cité en page 41.)

[Agrawal & Srikant 1994] Rakesh Agrawal et Ramakrishnan Srikant. Fast Algorithms for Mining Association Rules in Large Databases. Dans Proceedings of VLDB’94, pages 487–499, 1994. (Cité en page 21.)

[Alba 1973] Richard D. Alba. A graph-theoretic definition of a sociometric clique. Journal of Mathematical Sociologys, vol. 3, pages 113–126, 1973. (Cité en pages 41 et 42.)

[Aloul et al. 2003a] F. A. Aloul, A. Ramani, I. L. Markov et K. A. Sakallah. Solving difficult instances of Boolean satisfiability in the presence of symmetry. IEEE Trans. on CAD of Integrated Circuits and Systems, vol. 22, no. 9, pages 1117–1137, 2003. (Cité en page 7.)

[Aloul et al. 2003b] Fadi A. Aloul, Arathi Ramani, Igor L. Markov et Karem A. Sakallah. Efficient Symmetry-Breaking for Boolean Satisfiability. Dans Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, 2003. (Cité en page 7.)

[Andrews 1968] Peter B. Andrews. Resolution With Merging. Journal of the ACM, vol. 15, no. 3, pages 367–381, Juillet 1968. (Cité en page 8.)

[Arimura & Uno 2007] Hiroki Arimura et Takeaki Uno. An efficient polynomial space and polynomial delay algorithm for enumeration of maximal motifs in a sequence. Journal of Combinatorial Optimization, vol. 13, 2007. (Cité en page 32.)

[Asín et al. 2009] Roberto Asín, Robert Nieuwenhuis, Albert Oliveras et Enric Rodríguez-Carbonell. *Cardinality Networks and Their Applications*. Dans 12th International Conference on Theory and Applications of Satisfiability Testing (SAT 2009), pages 167–180, 2009. (Cité en page 15.)

[Audemard & Simon 2009] Gilles Audemard et Laurent Simon. Predicting Learnt Clauses Quality in Modern SAT Solvers. Dans IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 399–404, 2009. (Cité en pages 9 et 11.)

[Audemard et al. 2007] Gilles Audemard, Saïd Jabbour et Lakhdar Sais. Symmetry Breaking in Quantified Boolean Formulae. Dans IJCAI 2007, Proceedings of the 20th International Joint Conference on Artificial Intelligence, Hyderabad, India, January 6-12, 2007, pages 2262–2267, 2007. (Cité en page 7.)

[Audemard et al. 2011] Gilles Audemard, Jean-Marie Lagniez, Bertrand Mazure et Lakhdar Sais. On Freezing and Reactivating Learnt Clauses. Dans Theory and Applications of
Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, pages 188-200, 2011. (Cité en page 10.)

[Audemard et al. 2012] Gilles Audemard, Benoît Hoessen, Saïd Jabbour, Jean-Marie Lagniez et Cédric Piette. *Revisiting Clause Exchange in Parallel SAT Solving*. Dans Theory and Applications of Satisfiability Testing - SAT 2012 - 15th International Conference, Trento, Italy, June 17-20, 2012. Proceedings, pages 200-213, 2012. (Cité en pages 9 et 10.)

[Audemard et al. 2014] Gilles Audemard, Benoît Hoessen, Saïd Jabbour et Cédric Piette. *An Effective Distributed D&C Approach for the Satisfiability Problem*. Dans 22nd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2014, Torino, Italy, February 12-14, 2014, pages 183-187, 2014. (Cité en page 12.)

[Baader et al. 2010] Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi et Peter F. Patel-Schneider. The description logic handbook : Theory, implementation and applications. Cambridge University Press, New York, NY, USA, 2nd édition, 2010. (Cité en page 52.)

[Bailleux et al. 2009] O. Bailleux, Y. Boufkhad et O. Roussel. *New Encodings of Pseudo-Boolean Constraints into CNF*. Dans SAT'2009, pages 181-194, 2009. (Cité en page 15.)

[Balbiani et al. 2010] Philippe Balbiani, Fahima Cheikh Alili, P.-C. Héam et Olga Kouchnarenko. *Composition of Services with Constraints*. Electronic Notes in Theoretical Computer Science, vol. 263, no. 0, pages 31-46, 2010. Proceedings of the 6th International Workshop on Formal Aspects of Component Software (FACS 2009). (Cité en page 53.)

[Bastide et al. 2000] Yves Bastide, Nicolas Pasquier, Rafik Taouil, Gerd Stumme et Lotfi Lakhal. *Mining Minimal Non-redundant Association Rules Using Frequent Closed Itemsets*. Dans Computational Logic - CL 2000, volume 1861, pages 972-986, 2000. (Cité en page 31.)

[Benhamou & Sais 1994] Belaid Benhamou et Lakhdar Sais. *Tractability through Symmetries in Propositional Calculus*. Journal of Automated Reasoning, vol. 12, no. 1, pages 89-102, Février 1994. (Cité en page 7.)

[Besnard 2014] Philippe Besnard. *Revisiting Postulates for Inconsistency Measures*. Dans JELIA, pages 383-396, 2014. (Cité en page 46.)

[Billard & Diday 2012] Lynne Billard et Edwin Diday. Symbolic data analysis : Conceptual statistics and data mining. John Wiley & Sons, May 2012. (Cité en page 35.)

[Bistarelli & Bonchi 2007] Stefano Bistarelli et Francesco Bonchi. *Soft constraint based pattern mining*. Data & Knowledge Engineering, vol. 62, no. 1, pages 118-137, 2007. (Cité en page 14.)

[Böhm & Speckenmeyer 1996] Max Böhm et Ewald Speckenmeyer. *A Fast Parallel SAT-Solver - Efficient Workload Balancing*. Ann. Math. Artif. Intell., vol. 17, no. 3-4, pages 381-400, 1996. (Cité en page 9.)

[Borgelt 2012] Christian Borgelt. *Frequent item set mining*. Wiley Interdisc. Rew. : Data Mining and Knowledge Discovery, vol. 2, no. 6, pages 437-456, 2012. (Cité en page 26.)

[Boudane et al. 2016] Abdelhamid Boudane, Saïd Jabbour, Lakhdar Sais et Yakoub Salhi. *A SAT-Based Approach for Mining Association Rules*. Dans Proceedings of IJCAI'16, pages 2472-2478, 2016. (Cité en pages 6, 26, 30 et 31.)
[Boudane et al. 2017a] Abdelhamid Boudane, Saïd Jabbour, Lakhdar Sais et Yakoub Salhi. *Clustering Complex Data Represented as Propositional Formulas*. Dans Advances in Knowledge Discovery and Data Mining - 21st Pacific-Asia Conference, PAKDD 2017, Jeju, South Korea, May 23-26, 2017, Proceedings, Part II, pages 441-452, 2017. (Cité en pages 35 et 36.)

[Boudane et al. 2017b] Abdelhamid Boudane, Saïd Jabbour, Lakhdar Sais et Yakoub Salhi. *Enumerating Non-redundant Association Rules Using Satisfiability*. Dans Advances in Knowledge Discovery and Data Mining - 21st Pacific-Asia Conference, PAKDD 2017, Jeju, South Korea, May 23-26, 2017, Proceedings, Part I, pages 824-836, 2017. (Cité en page 31.)

[Boutilier et al. 2004] Craig Boutilier, Ronen I. Brafman, Carmel Domshlak, David L. Poole et Holger H. Hoos. *CP-nets : A Tool for Representing and Reasoning with Conditional Ceteris Paribus Preference Statements*. Journal of Artificial Intelligence Research (JAIR), vol. 21, pages 135-191, 2004. (Cité en page 14.)

[Bouzeghoub et al. 2017] Amel Bouzeghoub, Saïd Jabbour, Yue Ma et Badran Raddaoui. *Handling conflicts in uncertain ontologies using deductive argumentation*. Dans Proceedings of the International Conference on Web Intelligence, Leipzig, Germany, August 23-26, 2017, pages 65-72, 2017. (Cité en page 52.)

[Brafman & Domshlak 2009] R. I. Brafman et Carmel Domshlak. *Preference Handling - An Introductory Tutorial*. AI Magazine, vol. 30, no. 1, pages 58-86, 2009. (Cité en pages 14 et 29.)

[Burdick et al. 2001] Doug Burdick, Manuel Calimlim et Johannes Gehrke. *MAFIA : A maximal frequent itemset algorithm for transactional databases*. Dans In ICDE, pages 443-452, 2001. (Cité en page 25.)

[Cadoli & Donini 1997] Marco Cadoli et Francesco M. Donini. *A Survey on Knowledge Compilation*. AI Commun., vol. 10, no. 3-4, pages 137-150, 1997. (Cité en page 13.)

[Cai et al. 1998] C. H. Cai, Ada W. C. Fu, C. H. Cheng et W. W. Kwong. *Mining Association Rules with Weighted Items*. Dans In Proc. of IDEAS Symp, pages 68-77, 1998. (Cité en page 29.)

[Castell et al. 1996] Thierry Castell, Claudette Cayrol, Michel Cayrol et Daniel Le Berre. *Using the Davis and Putnam Procedure for an Efficient Computation of Preferred Models*. Dans ECAI'96, pages 350-354, 1996. (Cité en page 14.)

[Chauhan et al. 2003] Pankaj Chauhan, Edmund M. Clarke et Daniel Kroening. *Using SAT based image computation for reachability analysis*. Rapport technique, Technical Report CMU-CS-03-151, 2003. (Cité en page 12.)

[Chiu & Jain 1989] D-M Chiu et R. Jain. *Analysis of the Increase and Decrease Algorithms for Congestion Avoidance in Computer Networks*. Comp. Networks, vol. 17, pages 1-14, 1989. (Cité en page 10.)

[Chrabakh & Wolski 2003] Wahid Chrabakh et Richard Wolski. *GridSAT : A Chaff-based Distributed SAT Solver for the Grid*. Dans Proceedings of the ACM/IEEE SC2003 Conference on High Performance Networking and Computing, 15-21 November 2003, Phoenix, AZ, USA, CD-Rom, page 37, 2003. (Cité en pages 9 et 12.)
[Chu *et al.* 2008] Geoffrey Chu, Peter J. Stuckey et Aaron Harwood. *PMiniSAT: A Parallelization of MiniSAT 2.0*. Rapport technique, 2008. (Cité en pages 9 et 12.)

[Chui & Kao 2008] Chun Kit Chui et Ben Kao. *A Decremental Approach for Mining Frequent Itemsets from Uncertain Data*. Dans Proceedings of the Pacific-Asia Conference on Advances in Knowledge Discovery and Data Mining, pages 64–75, 2008. (Cité en page 29.)

[Chui *et al.* 2007] Chun-Kit Chui, Ben Kao et Edward Hung. *Mining Frequent Itemsets from Uncertain Data*. Dans Proceedings of the Pacific-Asia Conference on Advances in Knowledge Discovery and Data Mining, PAKDD’07, pages 47–58, 2007. (Cité en page 29.)

[Clarke *et al.* 2001] Edmund M. Clarke, Armin Biere, Richard Raimi et Yunshan Zhu. *Bounded Model Checking Using Satisfiability Solving*. Formal Methods in System Design, vol. 19, no. 1, pages 7–34, 2001. (Cité en page 6.)

[Cohen *et al.* 2006] David A. Cohen, Peter Jeavons, Christopher Jefferson, Karen E. Petrie et Barbara M. Smith. *Symmetry Definitions for Constraint Satisfaction Problems*. Constraints, vol. 11, no. 2-3, pages 115–137, 2006. (Cité en page 7.)

[Cohen 2008] J. Cohen. *Trusses: Cohesive subgraphs for social network analysis*. Dans Technical report, National Security Agency, 2008. (Cité en page 42.)

[Cook 1971] S. A. Cook. *The complexity of theorem-proving procedures*. Dans Proceedings of the Third Annual ACM Symposium on Theory of Computing, pages 151–158, New York (USA), 1971. Association for Computing Machinery. (Cité en page 6.)

[Coquery *et al.* 2012] Emmanuel Coquery, Saïd Jabbour, Lakhdar Saïs et Yakoub Salhi. *A SAT-Based Approach for Discovering Frequent, Closed and Maximal Patterns in a Sequence*. Dans ECAI 2012 - 20th European Conference on Artificial Intelligence. Including Prestigious Applications of Artificial Intelligence (PAIS-2012) System Demonstrations Track, Montpellier, France, August 27-31, 2012, pages 258–263, 2012. (Cité en page 33.)

[Coudert & Madre 1993] O. Coudert et J.C. Madre. *Fault tree analysis: 10²⁰ prime implicants and beyond*. Dans Reliability and Maintainability Symposium, 1993. Proceedings., Annual, pages 240–245, Jan 1993. (Cité en page 13.)

[Crawford & Baker 1994] James M. Crawford et Andrew B. Baker. *Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems*. Dans Proceedings of the Twelfth National Conference on Artificial Intelligence (Vol. 2), AAAI’94, pages 1092–1097, 1994. (Cité en page 6.)

[Crawford *et al.* 1996] James M. Crawford, Matthew L. Ginsberg, Eugene M. Luks et Amitabha Roy. *Symmetry-Breaking Predicates for Search Problems*. Dans Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR’96), Cambridge, Massachusetts, USA, November 5-8, 1996., pages 148–159, 1996. (Cité en page 7.)

[Crawford 1992] James Crawford. *A theoretical Analysis of Reasoning by Symmetry in First Order Logic*. Dans Proceedings of Workshop on Tractable Reasonning, AAAI92, pages 17–22, Juillet 1992. (Cité en page 7.)
[Creignou et al. 2011] Nadia Creignou, Frédéric Olive et Johannes Schmidt. Enumerating All Solutions of a Boolean CSP by Non-decreasing Weight. Dans the 14th International Conference on Theory and Applications of Satisfiability Testing (SAT’11), pages 120–133, 2011. (Cité en page 13.)

[Dao et al. 2013] Thi-Bich-Hanh Dao, Khanh-Chuong Duong et Christel Vrain. A Declarative Framework for Constrained Clustering. Dans Proceedings of ECML PKDD’13, pages 419–434, 2013. (Cité en page 21.)

[Darwiche & Marquis 2002] Adnan Darwiche et Pierre Marquis. A Knowledge Compilation Map. J. Artif. Intell. Res. (JAIR), vol. 17, pages 229–264, 2002. (Cité en page 13.)

[Davidson et al. 2010] Ian Davidson, S. S. Ravi et Leonid Shamis. A SAT-based Framework for Efficient Constrained Clustering. Dans Proceedings of SDM’10, pages 94–105, 2010. (Cité en page 21.)

[Davis et al. 1962] M. Davis, G. Logemann et D. W. Loveland. A machine program for theorem-proving. Communications of the ACM, vol. 5, no. 7, pages 394–397, 1962. (Cité en page 6.)

[de Amo et al. 2012] Sandra de Amo, Mouhamadou Saliou Diallo, Cheikh Talibouya Diop, Arnaud Giacometti, Haoyuan D. Li et Arnaud Soulet. Mining Contextual Preference Rules for Building User Profiles. Dans Proceedings of the 14th International Conference on Data Warehousing and Knowledge Discovery, DaWaK’12, pages 229–242, 2012. (Cité en page 14.)

[de Kleer et al. 1990] Johan de Kleer, Alan K. Mackworth et Raymond Reiter. Characterizing Diagnoses. Dans Proceedings of the 8th National Conference on Artificial Intelligence (AAAI’90), pages 324–330, 1990. (Cité en page 13.)

[Dechter & Itai 1992] Rina Dechter et Alon Itai. Finding All Solutions if You can Find One. Dans In AAAI-92 Workshop on Tractable Reasoning, pages 35–39, 1992. (Cité en page 13.)

[del Val 1994] A. del Val. Tractable Databases: How to Make Propositional Unit Resolution Complete Through Compilation. Dans Proceedings of the 4th International Conference on Principles of Knowledge Representation and Reasoning (KR’94), pages 551–561, 1994. (Cité en page 13.)

[Desrosiers et al. 2007] Christian Desrosiers, Philippe Galinier, Pierre Hansen et Alain Hertz. Improving Frequent Subgraph Mining in the Presence of Symmetry. Dans Proceedings of MLG’2007, 2007. (Cité en page 27.)

[Diday & Esposito 2003] Edwin Diday et Floriana Esposito. An introduction to symbolic data analysis and the SODAS software. Intell. Data Anal., vol. 7, no. 6, pages 583–601, 2003. (Cité en page 35.)

[Dlala et al. 2010] Imen Ouled Dlala, Said Jabbour, Badran Raddaoui et Lakhdar Sais. A SAT Based Framework for Itemset Mining in Parallel. Dans In Proceedings of CP’18, pages 552–567. Springer, 2010. (Cité en page 27.)

[Dlala et al. 2015] Imen Ouled Dlala, Saïd Jabbour, Lakhdar Sais, Yakoub Salhi et Boutheina Ben Yaghlane. Parallel SAT based closed frequent itemsets enumeration. Dans 12th IEEE/ACS International Conference of Computer Systems and Applications, AICCSA 2015, Marrakech, Morocco, November 17-20, 2015, pages 1–8, 2015. (Cité en page 27.)
[Dlala et al. 2016a] Imen Ouled Dlala, Saïd Jabbour, Badran Raddaoui, Lakhdar Sais et Boutheina Ben Yaghlane. *A SAT-Based Approach for Enumerating Interesting Patterns from Uncertain Data*. Dans 28th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2016, San Jose, CA, USA, November 6-8, 2016, pages 255–262, 2016. (Cité en page 30.)

[Dlala et al. 2016b] Imen Ouled Dlala, Saïd Jabbour, Lakhdar Saïs et Boutheina Ben Yaghlane. *A Comparative Study of SAT-Based Itemsets Mining*. Dans Research and Development in Intelligent Systems XXXIII - Incorporating Applications and Innovations in Intelligent Systems XXIV. Proceedings of AI-2016, The Thirty-Sixth SGAI International Conference on Innovative Techniques and Applications of Artificial Intelligence, Cambridge, UK, December 13-15, 2016, pages 37–52, 2016. (Cité en page 25.)

[Dlala et al. 2018] Imen Ouled Dlala, Saïd Jabbour, Badran Raddaoui et Lakhdar Sais. *A Parallel SAT-Based Framework for Closed Frequent Itemsets Mining*. Dans Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings, pages 570–587, 2018. (Cité en page 26.)

[Domshlak et al. 2011] Carmel Domshlak, Eyke Hüllermeier, Souhila Kaci et Henri Prade. *Preferences in AI : An overview*. Artificial Intelligence, vol. 175, no. 7-8, pages 1037–1052, 2011. (Cité en pages 14 et 29.)

[Dung 1995] Phan Minh Dung. *On the Acceptability of Arguments and its Fundamental Role in Nonmonotonic Reasoning, Logic Programming and n-Persson Games*. Artif. Intell., vol. 77, no. 2, pages 321–358, 1995. (Cité en page 51.)

[Dutuit & Rauzy 1997] Y. Dutuit et A. Rauzy. *Exact and Truncated Computations of Prime Implicants of Coherent and non-Coherent Fault Trees within Aralia*. Reliability Engineering and System Safety, vol. 58, no. 2, pages 127–144, 1997. (Cité en page 13.)

[Eén & Biere 2005] Niklas Eén et Armin Biere. *Effective Preprocessing in SAT Through Variable and Clause Elimination*. Dans SAT, volume 3569 de Lecture Notes in Computer Science, pages 61–75. Springer, 2005. (Cité en page 18.)

[Eén & Sörensson 2006] N. Eén et N. Sörensson. *Translating Pseudo-Boolean Constraints into SAT*. JSAT, vol. 2, no. 1-4, pages 1–26, 2006. (Cité en page 15.)

[Eiter 1996] Thomas Eiter. *Open Problems in Satisfiability*. Dans http://www.ece.uc.edu/franco/Sat-workshop/sat-workshop-open-problems.html, 1996. (Cité en page 50.)

[Ester et al. 1996] Martin Ester, Hans-Peter Kriegel, Jörg Sander et Xiaowei Xu. *A Density-Based Algorithm for Discovering Clusters in Large Spatial Databases with Noise*. Dans Proceedings of the Second International Conference on Knowledge Discovery and Data Mining (KDD-96), Portland, Oregon, USA, pages 226–231, 1996. (Cité en page 36.)

[Fournier-Viger & Tseng 2013] Philippe Fournier-Viger et Vincent S. Tseng. *TNS : mining top-k non-redundant sequential rules*. Dans Proceedings of SAC ’13, pages 164–166, 2013. (Cité en page 31.)

[Fournier-Viger et al. 2014] Philippe Fournier-Viger, Antonio Gomaric, Ted Gueniche, Azadeh Soltani, Cheng-Wei Wu et Vincent S Tseng. *SPMF : a java open-source pattern mining*
*library*. The Journal of Machine Learning Research, vol. 15, no. 1, pages 3389–3393, 2014. (Cité en page 31.)

[Fu et al. 2000] Ada Wai-Chee Fu, Renfrew W. w. Kwong et Jian Tang. *Mining N-most Interesting Itemsets*. Dans Proceedings of the 12th International Symposium on MÈthodologies for Intelligent Systems (ISMIS 2000), Lecture Notes in Computer Science, pages 59–67. Springer, 2000. (Cité en page 28.)

[Gasmi et al. 2005] Ghada Gasmi, Sadok Ben Yahia, Engelbert Mephu Nguifo et Yahya Slimani. *IGB : A New Informative Generic Base of Association Rules*. Dans Proceedings of PAKDD’05, pages 81–90, 2005. (Cité en page 31.)

[Gebser et al. 2016] Martin Gebser, Thomas Guyet, René Quiniou, Javier Romero et Torsten Schaub. *Knowledge-Based Sequence Mining with ASP*. Dans IJCAI, pages 1497–1504. IJCAI/AAAI Press, 2016. (Cité en page 21.)

[Gent & Smith 2000] Ian P. Gent et Barbara Smith. *Symmetry breaking in constraint programming*. Dans Proceedings of the Thirteenth European Conference on Artificial Intelligence(ECAI’00), pages 599–603, 2000. (Cité en page 7.)

[Ginsberg 1989] MatthewL. Ginsberg. *A circumscriptive theorem prover*. Dans M. Reinfrank, J. Kleer, M.L. Ginsberg et E. Sandewall, editeurs, Non-Monotonic Reasoning, volume 346 de *Lecture Notes in Computer Science*, pages 100–114. Springer Berlin Heidelberg, 1989. (Cité en page 13.)

[Gouda & Zaki 2005] Karam Gouda et Mohammed Javeed Zaki. *GenMax : An Efficient Algorithm for Mining Maximal Frequent Itemsets*. Data Min. Knowl. Discov., vol. 11, no. 3, pages 223–242, 2005. (Cité en page 25.)

[Grant & Hunter 2008] John Grant et Anthony Hunter. *Analysing inconsistent first-order knowledgebases*. Artif. Intell., vol. 172, no. 8-9, pages 1064–1093, 2008. (Cité en page 46.)

[Grant & Hunter 2011] John Grant et Anthony Hunter. *Measuring the Good and the Bad in Inconsistent Information*. Dans IJCAI, pages 2632–2637, 2011. (Cité en page 45.)

[Grégoire et al. 2004] Éric Grégoire, Richard Ostrowski, Bertrand Mazure et Lakhdar Sais. *Automatic Extraction of Functional Dependencies*. Dans SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10-13 May 2004, Vancouver, BC, Canada, Online Proceedings, 2004. (Cité en page 8.)

[Gregory 2009] Steve Gregory. *Finding Overlapping Communities Using Disjoint Community Detection Algorithms*. Dans International Workshop on Complex Networks, pages 47–61, 2009. (Cité en page 39.)

[Guo et al. 2010] Long Guo, Youssef Hamadi, Saïd Jabbour et Lakhdar Sais. *Diversification and Intensification in Parallel SAT Solving*. Dans Principles and Practice of Constraint Programming - CP 2010 - 16th International Conference, CP 2010, St. Andrews, Scotland, UK, September 6-10, 2010. Proceedings, pages 252–265, 2010. (Cité en page 11.)

[Guo et al. 2014] Long Guo, Saïd Jabbour, Jerry Lonlac et Lakhdar Sais. *Diversification by Clauses Deletion Strategies in Portfolio Parallel SAT Solving*. Dans 26th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2014, Limassol, Cyprus, November 10-12, 2014, pages 701–708, 2014. (Cité en page 11.)
[Hamadi et al. 2009] Youssef Hamadi, Saïd Jabbour et Lakhdar Sais. Control-Based Clause Sharing in Parallel SAT Solving. Dans IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009, pages 499–504, 2009. (Cité en pages 8, 9 et 10.)

[Hamadi et al. 2011] Youssef Hamadi, Saïd Jabbour, Cédric Piette et Lakhdar Sais. Deterministic Parallel DPLL. JSAT, vol. 7, no. 4, pages 127–132, 2011. (Cité en pages 10 et 11.)

[Hamadi et al. 2012] Youssef Hamadi, Said Jabbour et Lakhdar Sais. Learning from conflicts in propositional satisfiability. 4OR, vol. 10, no. 1, pages 15–32, 2012. (Cité en page 8.)

[Hamadi et al. 2016] Youssef Hamadi, Saïd Jabbour et Lakhdar Saïs. What we can learn from conflicts in propositional satisfiability. Annals OR, vol. 240, no. 1, pages 13–37, 2016. (Cité en page 8.)

[Han et al. 2002] Jiawei Han, Jianyong Wang, Ying Lu et Petre Tzvetkov. Mining Top-K Frequent Closed Patterns without Minimum Support. Dans Proceedings of the 2002 IEEE International Conference on Data Mining (ICDM 2002), pages 211–218. IEEE Computer Society, 2002. (Cité en page 28.)

[Hattad et al. 2017] Soukaina Hattad, Saïd Jabbour, Lakhdar Sais et Yakoub Salhi. Enhancing Pigeon-Hole based Encoding of Boolean Cardinality Constraints. Dans Proceedings of the 9th International Conference on Agents and Artificial Intelligence, ICAART 2017, Volume 2, Porto, Portugal, February 24-26, 2017., pages 299–307, 2017. (Cité en page 16.)

[Henriques et al. 2012] Rui Henriques, Inês Lynce et Vasco M. Manquinho. On When and How to use SAT to Mine Frequent Itemsets. CoRR, vol. abs/1207.6253, 2012. (Cité en page 24.)

[Heule et al. 2018] Marijn J. H. Heule, Oliver Kullmann et Armin Biere. Cube-and-Conquer for Satisfiability. Dans Handbook of Parallel Constraint Reasoning., pages 31–59. 2018. (Cité en page 9.)

[Hotz et al. 2014] Lothar Hotz, Alexander Felfernig, Markus Stumptner, Anna Ryabokon, Claire Bagley et Katharina Wolter. Chapter 6 - Configuration Knowledge Representation and Reasoning. Dans Knowledge-Based Configuration, pages 41 – 72. Morgan Kaufmann, 2014. (Cité en page 35.)

[Huan et al. 2003] Jun Huan, Wei Wang et Jan Prins. Efficient Mining of Frequent Subgraphs in the Presence of Isomorphism. Dans Proceedings of the 3rd IEEE ICDM’2003, pages 549–552, 2003. (Cité en page 27.)

[Hunter & Konieczny 2005] Anthony Hunter et Sébastien Konieczny. Approaches to Measuring Inconsistent Information. Dans Inconsistency Tolerance, pages 191–236, 2005. (Non cité.)

[Hunter & Konieczny 2010] Anthony Hunter et Sébastien Konieczny. On the measure of conflicts : Shapley Inconsistency Values. Artif. Intell., vol. 174, no. 14, pages 1007–1026, 2010. (Cité en pages 45 et 46.)

[Jabbour & Raddaoui 2013] Saïd Jabbour et Badran Raddaoui. Measuring Inconsistency through Minimal Proofs. Dans ECSQARU, pages 290–301, 2013. (Cité en page 47.)
[Jabbour & Sais 2016] Saïd Jabbour et Lakhdar Sais. Exploiting MUS Structure to Measure Inconsistency of Knowledge Bases. Dans ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), pages 991–998, 2016. (Cité en pages 49 et 50.)

[Jabbour et al. 2012] Saïd Jabbour, Lakhdar Sais, Yakoub Salhi et Karim Tabia. Symmetries in Itemset Mining. Dans ECAI 2012 - 20th European Conference on Artificial Intelligence. Including Prestigious Applications of Artificial Intelligence (PAIS-2012) System Demonstrations Track, Montpellier, France, August 27-31, 2012, pages 432–437, 2012. (Cité en pages 27 et 28.)

[Jabbour et al. 2013a] Saïd Jabbour, Mehdi Khiari, Lakhdar Sais, Yakoub Salhi et Karim Tabia. Symmetry-Based Pruning in Itemset Mining. Dans 25th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2013, Herndon, VA, USA, November 4-6, 2013, pages 483–490, 2013. (Cité en page 28.)

[Jabbour et al. 2013b] Saïd Jabbour, Jerry Lonlac et Lakhdar Saïs. Adding New Bi-Asserting Clauses for Faster Search in Modern SAT Solvers. Dans Proceedings of the Tenth Symposium on Abstraction, Reformulation, and Approximation, SARA 2013, 11-12 July 2013, Leavenworth, Washington, USA., 2013. (Cité en page 8.)

[Jabbour et al. 2013c] Saïd Jabbour, Lakhdar Sais et Yakoub Salhi. Boolean satisfiability for sequence mining. Dans 22nd ACM International Conference on Information and Knowledge Management, CIKM’13, San Francisco, CA, USA, October 27 - November 1, 2013, pages 649–658, 2013. (Cité en page 33.)

[Jabbour et al. 2013d] Saïd Jabbour, Lakhdar Sais et Yakoub Salhi. A Pigeon-Hole Based Encoding of Cardinality Constraints. TPLP, vol. 13, 2013. (Cité en pages 14, 15, 16 et 24.)

[Jabbour et al. 2013e] Saïd Jabbour, Lakhdar Sais et Yakoub Salhi. The Top-k Frequent Closed Itemset Mining Using Top-k SAT Problem. Dans Proceedings of ECML/PKDD’13, pages 403–418, 2013. (Cité en pages 26 et 28.)

[Jabbour et al. 2013f] Saïd Jabbour, Lakhdar Sais, Yakoub Salhi et Takeaki Uno. Mining-based compression approach of propositional formulae. Dans 22nd ACM International Conference on Information and Knowledge Management, CIKM’13, San Francisco, CA, USA, October 27 - November 1, 2013, pages 289–298, 2013. (Cité en page 18.)

[Jabbour et al. 2014a] Saïd Jabbour, Jerry Lonlac, Lakhdar Sais et Yakoub Salhi. Extending modern SAT solvers for models enumeration. Dans Proceedings of the 15th IEEE International Conference on Information Reuse and Integration, IRI 2014, Redwood City, CA, USA, August 13-15, 2014, 2014. (Cité en page 13.)

[Jabbour et al. 2014b] Saïd Jabbour, Jerry Lonlac, Lakhdar Sais et Yakoub Salhi. Revisiting the Learned Clauses Database Reduction Strategies. CoRR, vol. abs/1402.1956, 2014. (Cité en page 9.)

[Jabbour et al. 2014c] Saïd Jabbour, Yue Ma et Badran Raddaoui. Inconsistency Measurement Thanks to MUS-Decomposition. Dans International conference on Autonomous Agents and Multi-Agent Systems (AAMAS’14), pages 877–884, 2014. (Cité en pages 46 et 47.)
[Jabbour et al. 2014d] Saïd Jabbour, Yue Ma, Badran Raddaoui et Lakhdar Sais. On the Characterization of Inconsistency : A Prime Implicates Based Framework. Dans 26th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2014, Limassol, Cyprus, November 10-12, 2014, pages 146–153, 2014. (Cité en pages 49 et 50.)

[Jabbour et al. 2014e] Saïd Jabbour, Yue Ma, Badran Raddaoui et Lakhdar Saïs. Prime Implicates Based Inconsistency Characterization. Dans ECAI, pages 1037–1038, 2014. (Cité en page 49.)

[Jabbour et al. 2014f] Saïd Jabbour, Joao Marques-Silva, Lakhdar Sais et Yakoub Salhi. Enumerating Prime Implicants of Propositional Formulae in Conjunctive Normal Form. Dans Logics in Artificial Intelligence - 14th European Conference, JELIA 2014, Funchal, Madeira, Portugal, September 24-26, 2014. Proceedings, pages 152–165, 2014. (Cité en page 13.)

[Jabbour et al. 2014g] Saïd Jabbour, Lakhdar Saïs et Yakoub Salhi. A Pigeon-Hole Based Encoding of Cardinality Constraints. Dans International Symposium on Artificial Intelligence and Mathematics, ISAIM 2014, Fort Lauderdale, FL, USA, January 6-8, 2014, 2014. (Cité en pages 15 et 16.)

[Jabbour et al. 2015a] Saïd Jabbour, Stéphanie Roussel, Lakhdar Sais et Yakoub Salhi. Mining to Compress Table Constraints. Dans 27th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2015, Vietri sul Mare, Italy, November 9-11, 2015, pages 405–412, 2015. (Cité en page 19.)

[Jabbour et al. 2015b] Saïd Jabbour, Lakhdar Sais et Yakoub Salhi. Decomposition Based SAT Encodings for Itemset Mining Problems. Dans Proceedings of PAKDD’15, pages 662–674, 2015. (Cité en page 26.)

[Jabbour et al. 2016a] Saïd Jabbour, Souhila Kaci, Lakhdar Sais et Yakoub Salhi. Itemset Mining with Penalties. Dans 28th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2016, San Jose, CA, USA, November 6-8, 2016, pages 962–966, 2016. (Cité en page 29.)

[Jabbour et al. 2016b] Saïd Jabbour, Yue Ma, Badran Raddaoui, Lakhdar Sais et Yakoub Salhi. A MIS Partition Based Framework for Measuring Inconsistency. Dans Principles of Knowledge Representation and Reasoning : Proceedings of the Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29, 2016., pages 84–93, 2016. (Cité en page 47.)

[Jabbour et al. 2016c] Saïd Jabbour, Nizar Mhadhbi, Abdesattar Mhadhbi, Badran Raddaoui et Lakhdar Sais. Summarizing big graphs by means of pseudo-boolean constraints. Dans 2016 IEEE International Conference on Big Data, BigData 2016, Washington DC, USA, December 5-8, 2016, pages 889–894, 2016. (Cité en pages 43 et 44.)

[Jabbour et al. 2016d] Saïd Jabbour, Badran Raddaoui, Lakhdar Sais et Yakoub Salhi. On the Computation of Top-k Extensions in Abstract Argumentation Frameworks. Dans ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), pages 913–920, 2016. (Cité en page 51.)
[Jabbour et al. 2017a] Said Jabbour, Abdelhamid Boudane, Badran Raddaoui et Lakhdar Sais. *Efficient SAT-Based Encodings of Conditional Cardinality Constraints*. Dans LPAR-22, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017. (Cité en page 17.)

[Jabbour et al. 2017b] Saïd Jabbour, Yue Ma, Badran Raddaoui et Lakhdar Sais. *Quantifying conflicts in propositional logic through prime implicates*. Int. J. Approx. Reasoning, vol. 89, pages 27–40, 2017. (Cité en page 49.)

[Jabbour et al. 2017c] Saïd Jabbour, Nizar Mhadhbi, Badran Raddaoui et Lakhdar Sais. *A SAT-Based Framework for Overlapping Community Detection in Networks*. Dans Advances in Knowledge Discovery and Data Mining - 21st Pacific-Asia Conference, PAKDD 2017, Jeju, South Korea, May 23-26, 2017, Proceedings, Part II, pages 786–798, 2017. (Cité en pages 41, 42, 48 et 50.)

[Jabbour et al. 2017d] Saïd Jabbour, Lakhdar Sais et Yakoub Salhi. *Mining Top-k motifs with a SAT-based framework*. Artif. Intell., vol. 244, pages 30–47, 2017. (Cité en pages 14, 28 et 29.)

[Jabbour et al. 2018] Said Jabbour, Nizar LMhadhbi, Badran et Raddaoui Lakhdar Sais. *Pushing the Envelope in Overlapping Communities Detection*. Dans Advances in Intelligent Data Analysis XVI - 16th International Symposium, IDA 2018, Proceedings, volume – de Lecture Notes in Computer Science. Springer, 2018. (Cité en page 42.)

[Jabbour 2009] Saïd Jabbour. *Learning for Dynamic Assignments Reordering*. Dans ICTAI 2009, 21st IEEE International Conference on Tools with Artificial Intelligence, Newark, New Jersey, USA, 2-4 November 2009, pages 336–343, 2009. (Cité en page 8.)

[Jabbour 2016] Saïd Jabbour. *On Inconsistency Measuring and Resolving*. Dans ECAI 2016 - 22nd European Conference on Artificial Intelligence, 29 August-2 September 2016, The Hague, The Netherlands - Including Prestigious Applications of Artificial Intelligence (PAIS 2016), pages 1676–1677, 2016. (Cité en page 51.)

[Jeroslow & Wang 1990] Robert G. Jeroslow et Jinchang Wang. *Solving propositional Satisfiability Problems*. Annals of Mathematics and Artificial Intelligence, vol. 1, pages 167–187, 1990. (Cité en page 25.)

[Jin et al. 2005] Hoonsang Jin, Hyojung Han et Fabio Somenzi. *Efficient conflict analysis for finding all satisfying assignments of a boolean circuit*. Dans In TACAS’05, LNCS 3440, pages 287–300. Springer, 2005. (Cité en page 12.)

[Jr. 1998] Roberto J. Bayardo Jr. *Efficiently Mining Long Patterns from Databases*. Dans SIGMOD 1998, Proceedings ACM SIGMOD International Conference on Management of Data, June 2-4, 1998, Seattle, Washington, USA., pages 85–93, 1998. (Cité en page 25.)

[Jurkowiak et al. 2001] Bernard Jurkowiak, Chu Min Li et Gil Utard. *Parallelizing Satz Using Dynamic Workload Balancing*. Electronic Notes in Discrete Mathematics, vol. 9, pages 174–189, 2001. (Cité en page 9.)

[Kaci 2011] Souhila Kaci. Working with preferences : Less is more. Cognitive Technologies. Springer, 2011. (Cité en page 29.)
[Karypis et al. 1999] George Karypis, Eui-Hong Han et Vipin Kumar. *Chameleon: Hierarchical Clustering Using Dynamic Modeling*. IEEE Computer, vol. 32, no. 8, pages 68–75, 1999. (Cité en page 36.)

[Katsirelos & Walsh 2007] George Katsirelos et Toby Walsh. *A Compression Algorithm for Large Arity Extensional Constraints*. Dans Proceedings of the 13th International Conference on Principles and Practice of Constraint Programming - CP 2007, volume 4741 of *Lecture Notes in Computer Science*, pages 379–393. Springer, 2007. (Cité en page 19.)

[Kemmar et al. 2014] Amina Kemmar, Willy Ugarte, Samir Loudni, Thierry Charnois, Yahia Lebbah, Patrice Boizumault et Bruno Crémilleux. *Mining Relevant Sequence Patterns with CP-Based Framework*. Dans 26th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2014, Limassol, Cyprus, November 10-12, 2014, pages 552–559, 2014. (Cité en page 21.)

[Konieczny et al. 2003] Sébastien Konieczny, Jérôme Lang et Pierre Marquis. *Quantifying information and contradiction in propositional logic through test actions*. Dans IJCAI, pages 106–111. Morgan Kaufmann, 2003. (Cité en page 46.)

[Koshimura et al. 2012] Miyuki Koshimura, Tong Zhang, Hiroshi Fujita et Ryuzo Hasegawa. *QMaxSAT: A Partial Max-SAT Solver*. JSAT, vol. 8, no. 1/2, pages 95–100, 2012. (Cité en page 16.)

[Kryszkiewicz 1998a] Marzena Kryszkiewicz. *Representative Association Rules*. Dans Proceedings of PAKDD’98, pages 198–209, 1998. (Cité en page 31.)

[Kryszkiewicz 1998b] Marzena Kryszkiewicz. *Representative Association Rules and Minimum Condition Maximum Consequence Association Rules*. Dans Proceedings of PKDD ’98, pages 361–369, 1998. (Cité en page 31.)

[Lazaar et al. 2012] Nadjib Lazaar, Youssef Hamadi, Saïd Jabbour et Michel sebag. *Cooperation control in Parallel SAT Solving : a Multi-armed Bandit Approach*. 2012. (Cité en page 10.)

[Lazaar et al. 2016] Nadjib Lazaar, Yahia Lebbah, Samir Loudni, Mehdi Maamar, Valentin Lemière, Christian Bessiere et Patrice Boizumault. *A Global Constraint for Closed Frequent Pattern Mining*. Dans Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings, pages 333–349, 2016. (Cité en page 27.)

[Leskovec et al. 2010] Jure Leskovec, Kevin J. Lang et Michael W. Mahoney. *Empirical comparison of algorithms for network community detection*. Dans WWW, pages 631–640, 2010. (Cité en page 42.)

[Leung et al. 2008] Carson Kai-Sang Leung, Mark Anthony F Mateo et Dale A Brajczuk. *A tree-based approach for frequent pattern mining from uncertain data*. Dans Advances in Knowledge Discovery and Data Mining, pages 653–661. Springer, 2008. (Cité en page 29.)

[Liberti 2012] Leo Liberti. *Reformulations in mathematical programming : automatic symmetry detection and exploitation*. Math. Program., vol. 131, no. 1-2, pages 273–304, 2012. (Cité en page 7.)
[Lin & Kedem 1998] Dao-I Lin et Zvi M. Kedem. Pincer-search : A new algorithm for discovering the maximum frequent set, pages 103–119. Springer Berlin Heidelberg, 1998. (Cité en page 25.)

[Luce 1950] R. Duncan Luce. Connectivity and generalized cliques in sociometric group structure. Psychometrika, vol. 15, no. 2, pages 169–190, Jun 1950. (Cité en page 42.)

[Ma et al. 2011] Yue Ma, Guilin Qi et Pascal Hitzler. Computing inconsistency measure based on paraconsistent semantics. J. Log. Comput., vol. 21, no. 6, pages 1257–1281, 2011. (Cité en page 46.)

[Macqueen 1967] J. Macqueen. Some methods for classification and analysis of multivariate observations. Dans In 5-th Berkeley Symposium on Mathematical Statistics and Probability, pages 281–297, 1967. (Cité en page 36.)

[Manquinho et al. 1997] Vasco M. Manquinho, Paulo E Flores, Jo P. Marques Silva et Arlindo L. Oliveira. Prime implicant computation using satisfiability algorithms. Dans in Proc. of the IEEE International Conference on Tools with Artificial Intelligence, pages 232–239, 1997. (Cité en page 13.)

[Manquinho et al. 1998] Vasco M. Manquinho, Arlindo L. Oliveira et João P. Marques Silva. Models and Algorithms for Computing Minimum-Size Prime Implicants. Dans In Proc. International Workshop on Boolean Problems (IWBP’98, 1998. (Cité en page 13.)

[Margot 2003] François Margot. Exploiting orbits in symmetric ILP. Math. Program., vol. 98, no. 1-3, pages 3–21, 2003. (Cité en page 7.)

[Marques-Silva & Sakallah 1996] Joao P. Marques-Silva et Karem A. Sakallah. GRASP - A New Search Algorithm for Satisfiability. Dans Proceedings of IEEE/ACM CAD, pages 220–227, 1996. (Cité en page 6.)

[Massacci & Marraro 2000] Fabio Massacci et Laura Marraro. Logical Cryptanalysis as a SAT Problem. J. Autom. Reasoning, vol. 24, no. 1/2, pages 165–203, 2000. (Cité en page 9.)

[Matas & Kittler 1995] Jiri Matas et Josef Kittler. Spatial and Feature Space Clustering : Applications in Image Analysis. Dans Computer Analysis of Images and Patterns, 6th International Conference, CAIP’95, Prague, Czech Republic, September 6-8, 1995, Proceedings, pages 162–173, 1995. (Cité en page 35.)

[McCluskey 1956] Jr. McCluskey E.J. Minimization of Boolean Functions. Bell System Technical Journal, vol. 35, no. 6, pages 1417–1444, 1956. (Cité en page 13.)

[McKay 1990] B. McKay. nauty user's guide (version 1.5). Rapport technique, 1990. (Cité en page 27.)

[McMillan 2002] Kenneth L. McMillan. Applying SAT Methods in Unbounded Symbolic Model Checking. Dans Proceedings of the 14th International Conference on Computer Aided Verification (CAV’02), pages 250–264, 2002. (Cité en page 12.)

[Meseguer et al. 2006] Pedro Meseguer, Francesca Rossi et Thomas Schiex. Soft Constraints. Dans Handbook of Constraint Programming, volume 2 de Foundations of Artificial Intelligence, pages 281–328. Elsevier, 2006. (Cité en page 14.)
[Michalski 1980] R. S. Michalski. *Knowledge Acquisition Through Conceptual Clustering: A Theoretical Framework and an Algorithm for Partitioning Data into Conjunctive Concepts*. Journal of Policy Analysis and Information Systems, vol. 4, no. 3, pages 219–244, 1980. (Cité en page 35.)

[Morgado & Marques-Silva 2005] António R. Morgado et João P. Marques-Silva. *Good Learning and Implicit Model Enumeration*. Dans International Conference on Tools with Artificial Intelligence (ICTAI’2005), pages 131–136. IEEE, 2005. (Cité en page 12.)

[Moskewicz et al. 2001] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang et S. Malik. *Chaff: Engineering an Efficient SAT Solver*. Dans Proceedings of the 38th Design Automation Conference, pages 530–535, 2001. (Cité en page 6.)

[Mu et al. 2011] Kedian Mu, Weiru Liu, Zhi Jin et David A. Bell. *A Syntax-based approach to measuring the degree of inconsistency for belief bases*. Int. J. Approx. Reasoning, vol. 52, no. 7, pages 978–999, 2011. (Cité en page 45.)

[Nacer et al. 2015] Amina Ahmed Nacer, Kahina Bessai, Samir Youcef et Claude Godart. *A Multi-criteria Based Approach for Web Service Selection Using Quality of Service (QoS)*. Dans Services Computing (SCC), 2015 IEEE International Conference on, pages 570–577. IEEE, 2015. (Cité en page 53.)

[Négrevergne et al. 2013] Benjamin Négrevergne, Anton Dries, Tias Guns et Siegfried Nijssen. *Dominance Programming for Itemset Mining*. Dans 2013 IEEE 13th International Conference on Data Mining, Dallas, TX, USA, December 7-10, 2013, pages 557–566, 2013. (Cité en page 14.)

[Newman & Girvan 2004] M. E. J. Newman et M. Girvan. *Finding and evaluating community structure in networks*. Phys. Rev. E, vol. 69, no. 2, page 026113, Février 2004. (Cité en pages 39 et 40.)

[Newman 2010] M. E. J. Newman. *Networks : An introduction*. Oxford Univ. Press, Oxford, U.K., 2010. (Cité en page 41.)

[Okutan & Cicekli 2010] Cagla Okutan et Nihan Kesim Cicekli. *A Monolithic Approach to Automated Composition of Semantic Web Services with the Event Calculus*. Know.-Based Syst., vol. 23, no. 5, pages 440–454, Juillet 2010. (Cité en page 53.)

[Oller 2004] Carlos A. Oller. *Measuring coherence using LP-models*. J. Applied Logic, vol. 2, no. 4, pages 451–455, 2004. (Cité en page 46.)

[Parida et al. 2000] Laxmi Parida, Isidore Rigoutsos, Aris Floratos, Dan Platt et Yuan Gao. *Pattern Discovery on Character Sets and Real-valued Data : Linear Bound on Irredundant Motifs and an Efficient Polynomial Time Algorithm*. Dans ACM-SIAM Symposium on Discrete Algorithms, pages 297–308, 2000. (Cité en page 32.)

[Pipatsrisawat & Darwiche 2008] Knot Pipatsrisawat et Adnan Darwiche. *A New Clause Learning Scheme for Efficient Unsatisfiability Proofs*. Dans Proceedings of the Twenty-Third AAAI Conference on Artificial Intelligence, AAAI 2008, Chicago, Illinois, USA, July 13-17, 2008, pages 1481–1484, 2008. (Cité en page 8.)
[Pisanti et al. 2003] Nadia Pisanti, Maxime Crochemore, Roberto Grossi et Marie france Sa-
got. Bases of motifs for generating repeated patterns with wild cards. IEEE/ACM
TCBB’2003, vol. 2, page 2005, 2003. (Cité en page 32.)

[Pizzuti 1996] Clara Pizzuti. *Computing Prime Implicants by Integer Programming*. Dans Proceedings of the 8th International Conference on Tools with Artificial Intelligence, ICTAI '96, pages 332–336, Washington, DC, USA, 1996. IEEE Computer Society. (Cité en page 13.)

[Quine 1952] W. V. Quine. *The Problem of Simplifying Truth Functions*. The American Mathematical Monthly, vol. 59, no. 8, pages 521–531, 1952. (Cité en page 13.)

[Quine 1959] W. Quine. *On cores and prime implicants of truth functions*. American Mathematical Monthly, pages 755–760, 1959. (Cité en page 13.)

[Raedt et al. 2008] Luc De Raedt, Tias Guns et Siegfried Nijssen. *Constraint Programming for Itemset Mining*. Dans Proceedings of SIGKDD’08, pages 204–212, 2008. (Cité en page 21.)

[Raedt et al. 2011] Luc De Raedt, Siegfried Nijssen, Barry O’Sullivan et Pascal Van Hentenryck. *Constraint Programming meets Machine Learning and Data Mining*. Dagstuhl Reports, vol. 1, no. 5, pages 61–83, 2011. (Cité en page 21.)

[Ramani et al. 2006] A. Ramani, I. L. Markov, K. A. Sakallah et F. A. Aloul. *Breaking Instance-Independent Symmetries In Exact Graph Coloring*. Journal of Artificial Intelligence Research (JAIR), vol. 26, pages 289–322, 2006. (Cité en page 27.)

[Rintanen 2006] J. Rintanen. *Compact representation of sets of binary constraints*. Dans Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006), pages 143–147. IOS Press, 2006. (Cité en page 18.)

[Rodriguez-Mier et al. 2011] Pablo Rodriguez-Mier, Manuel Mucientes et Manuel Lama. *Automatic Web Service Composition with a Heuristic-Based Search Algorithm*. Dans Proceedings of the 2011 IEEE International Conference on Web Services, ICWS ’11, pages 81–88, Washington, DC, USA, 2011. IEEE Computer Society. (Cité en page 53.)

[Rosa et al. 2010] Emanuele Di Rosa, Enrico Giunchiglia et Marco Maratea. *Solving satisfiability problems with preferences*. Constraints, vol. 15, no. 4, pages 485–515, 2010. (Cité en page 14.)

[Saito et al. 2008] Kazumi Saito, Takeshi Yamada et Kazuhiro Kazama. *Extracting Communities from Complex Networks by the k-Dense Method*. IEICE Transactions, vol. 91-A, no. 11, pages 3304–3311, 2008. (Cité en page 42.)

[Schaus et al. 2017] Pierre Schaus, John O. R. Aoga et Tias Guns. *CoverSize : A Global Constraint for Frequency-Based Itemset Mining*. Dans Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, pages 529–546, 2017. (Cité en page 27.)

[Seidman 1978] Stephen B. Seidman. *A graph-theoretic generalization of the clique concep*. Journal of Mathematical sociology, vol. 5, no. 3, page 139–154, 1978. (Cité en page 42.)
[Shao et al. 2014] Yingxia Shao, Lei Chen et Bin Cui. *Efficient cohesive subgraphs detection in parallel*. Dans SIGMOD, pages 613–624, 2014. (Cité en page 42.)

[Shen et al. 2009] Huawei Shen, Xueqi Cheng, Kai Cai et Mao-Bin Hu. *Detect overlapping and hierarchical community structure in networks*. Physica A, vol. 388, no. 8, pages 1706–1712, 2009. (Cité en page 39.)

[Shiaa et al. 2008] M.M. Shiaa, J.O. Fladmark et B. Thiell. *An Incremental Graph-based Approach to Automatic Service Composition*. Dans Services Computing, 2008. SCC ’08. IEEE International Conference on, volume 1, pages 397–404, July 2008. (Cité en page 53.)

[Shoham 1988] Yoav Shoham. Reasoning about change : time and causation from the standpoint of artificial intelligence. MIT Press, Cambridge, MA, USA, 1988. (Cité en page 14.)

[Silva & Lynce 2007] J. P. Marques Silva et I. Lynce. *Towards Robust CNF Encodings of Cardinality Constraints*. Dans 13th International Conference on Principles and Practice of Constraint Programming (CP 2007), pages 483–497, 2007. (Cité en page 15.)

[Sinz 2005] C. Sinz. Towards an Optimal CNF Encoding of Boolean Cardinality Constraints. Dans 11th International Conference on Principles and Practice of Constraint Programming - CP 2005, pages 827–831, 2005. (Cité en pages 15 et 17.)

[Slavkovik & Agotnes 2014] M. Slavkovik et T. Agotnes. *A Judgment Set Similarity Measure Based on Prime Implicants*. Dans Proceedings of the 13th International Conference on Autonomous Agents and Multiagent Systems, AAMAS ’14, page to appear, 2014. (Cité en page 13.)

[Sneath & Sokal 1973] P.H.A. Sneath et R.R. Sokal. Numerical taxonomy. the principles and practice of numerical classification. Freeman, 1973. (Cité en page 36.)

[Soos et al. 2009] Mate Soos, Karsten Nohl et Claude Castelluccia. Extending SAT Solvers to Cryptographic Problems. Dans Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings, pages 244–257, 2009. (Cité en page 9.)

[Soulet et al. 2011] Arnaud Soulet, Chedy Raïssi, Marc Plantevit et Bruno Crémilleux. *Mining Dominant Patterns in the Sky*. Dans ICDM’11, pages 655–664, 2011. (Cité en page 29.)

[Tan et al. 2000] Pang-Ning Tan, Vipin Kumar et Jaideep Srivastava. *Indirect Association : Mining Higher Order Dependencies in Data*. Dans Proceedings of PKDD’00, pages 632–637, 2000. (Cité en page 31.)

[Tao et al. 2003] Feng Tao, Fionn Murtagh et Mohsen Farid. *Weighted Association Rule Mining using Weighted Support and Significance Framework*. Dans Proceedings of SIGKDD’03, pages 661–666, 2003. (Cité en page 29.)

[Thimm 2016] Matthias Thimm. *On the expressivity of inconsistency measures*. Artif. Intell., vol. 234, pages 120–151, 2016. (Cité en page 47.)

[Tison 1967] P. Tison. *Generalized consensus theory and applications to the minimization of boolean circuits*. IEEE Transactions on Computers, pages 446–456, 1967. (Cité en page 13.)
[Tseitin 1968] G.S. Tseitin. *On the complexity of derivations in the propositional calculus*. Dans H.A.O. Slesenko, editeur, Structures in Constructives Mathematics and Mathematical Logic, Part II, pages 115–125, 1968. (Cité en pages 6 et 18.)

[Tversky 1977] A. Tversky. *Features of similarity*. Psychological Review, vol. 84, no. 4, page 327–352, 1977. (Cité en page 36.)

[Ugarte Rojas *et al*. 2014] Willy Ugarte Rojas, Patrice Boizumault, Samir Loudni, Bruno Cré-milleux et Alban Lepailleur. *Mining (Soft-) Skypatterns Using Dynamic CSP*. Dans Integration of AI and OR Techniques in Constraint Programming (CPAIOR’14), pages 71–87, 2014. (Cité en page 14.)

[Vanetik 2010] Natalia Vanetik. *Mining Graphs with Constraints on Symmetry and Diameter*. Dans International Workshops on Web-Age Information Management - WAIM 2010, pages 1–12, 2010. (Cité en page 27.)

[Wakrime & Jabbour 2015] Abderrahim Ait Wakrime et Saïd Jabbour. *Minimum Unsatisfiability based QoS Web Service Composition over the Cloud Computing*. Dans 15th International Conference on Intelligent Systems Design and Applications, ISDA 2015, Marrakech, Morocco, December 14-16, 2015, pages 540–545, 2015. (Cité en pages 55 et 56.)

[Wakrime & Jabbour 2017] Abderrahim Ait Wakrime et Saïd Jabbour. *Formal Approach for QoS-Aware Cloud Service Composition*. Dans 26th IEEE International Conference on Enabling Technologies : Infrastructure for Collaborative Enterprises, WETICE 2017, Poznan, Poland, June 21-23, 2017, pages 30–35, 2017. (Cité en page 55.)

[Wakrime *et al*. 2015] Abderrahim Ait Wakrime, Salima Benbernou et Saïd Jabbour. *Relaxation Based SaaS for Repairing Failed Queries over the Cloud Computing*. Dans 12th IEEE International Conference on e-Business Engineering, ICEBE 2015, Beijing, China, October 23-25, 2015, pages 245–250, 2015. (Cité en page 56.)

[Walsh 2006] T. Walsh. *General Symmetry Breaking Constraints*. Dans 12th International Conference on Principles and Practice of Constraint Programming (CP 2006), pages 650–664, 2006. (Cité en page 7.)

[Walsh 2007] Toby Walsh. *Representing and Reasoning with Preferences*. AI Magazine, vol. 28, no. 4, pages 59–70, 2007. (Cité en pages 14 et 29.)

[Wang & Cheng 2012] Jia Wang et James Cheng. *Truss Decomposition in Massive Networks*. PVLDB, vol. 5, no. 9, pages 812–823, 2012. (Cité en page 42.)

[Wang *et al*. 1999] Ke Wang, Chu Xu et Bing Liu. *Clustering Transactions Using Large Items*. Dans Proceedings of the 1999 ACM CIKM International Conference on Information and Knowledge Management, Kansas City, Missouri, USA, November 2-6, 1999, pages 483–490, 1999. (Cité en page 35.)

[Warners 1996] J. P. Warners. *A Linear-Time Transformation of Linear Inequalities into Conjunctive Normal Form*. Information Processing Letters, 1996. (Cité en page 15.)

[Wasserman & Faust 1994] S. Wasserman et K. Faust. *Social network analysis : Methods and applications*. Cambridge Univ Press, 1994. (Cité en page 42.)

[Wittkop *et al*. 2010] Tobias Wittkop, Dorothea Emig, Sita Lange, Sven Rahmann, Mario Albrech et John H. Morris. *On the maximum quasi-clique problem*. Nature Methods, vol. 7, no. 6, 2010. (Cité en page 35.)
[Wu & Khoury 2012] Ching-Seh Wu et Ibrahim Khoury. Tree-based search algorithm for web service composition in SaaS. Dans Information Technology : New Generations (ITNG), 2012 Ninth International Conference on, pages 132–138. IEEE, 2012. (Cité en page 53.)

[Xiao & Ma 2012] Guohui Xiao et Yue Ma. Inconsistency Measurement based on Variables in Minimal Unsatisfiable Subsets. Dans ECAI, pages 864–869, 2012. (Cité en page 45.)

[Xie et al. 2011] Jierui Xie, Boleslaw K. Szymanski et Xiaoming Liu. SLPA : Uncovering Overlapping Communities in Social Networks via a Speaker-Listener Interaction Dynamic Process. Dans IEEE International Conference on Data Mining, pages 344–349, 2011. (Cité en page 39.)

[Yang & Leskovec 2013] Jaewon Yang et Jure Leskovec. Overlapping community detection at scale : a nonnegative matrix factorization approach. Dans WSDM, pages 587–596, 2013. (Cité en pages 39 et 40.)

[Yun & Leggett 2005] Unil Yun et John J. Leggett. WFIM : Weighted Frequent Itemset Mining with a Weight Range and a Minimum Weight. Dans InProceedings of the Fifth SIAM International Conference on Data Mining, Pages, pages 636–640, 2005. (Cité en page 29.)

[Zaki & Hsiao 2002] Mohammed Javeed Zaki et Ching-Jiu Hsiao. CHARM : An Efficient Algorithm for Closed Itemset Mining. Dans Proceedings of SDM’02, pages 457–473, 2002. (Cité en page 25.)

[Zaki 2004] Mohammed Javeed Zaki. Mining Non-Redundant Association Rules. Data Mining Knowledge Discovery, vol. 9, pages 223–248, 2004. (Cité en pages 31 et 32.)

[Zhang et al. 2001] Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz et Sharad Malik. Efficient Conflict Driven Learning in Boolean Satisfiability Solver. Dans Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2001, San Jose, CA, USA, November 4-8, 2001, pages 279–285, 2001. (Cité en pages 6 et 25.)

[Zou et al. 2002] Qinghua Zou, Wesley W. Chu et Baojing Lu. SmartMiner : A Depth First Algorithm Guided by Tail Information for Mining Maximal Frequent Itemsets. Dans Proceedings of the 2002 IEEE International Conference on Data Mining (ICDM 2002), 9-12 December 2002, Maebashi City, Japan, pages 570–577, 2002. (Cité en page 25.)
## CHAPITRE 9

# Publications jointes

1. A Parallel SAT-based Framework for Closed Frequent Itemsets Mining (CP'2018)

2. A SAT-based Framework for Overlapping Community Detection in Network (PAKDD'2017)

3. Clustering Complex Data Represented as propositional formulas (PAKDD'2017)

4. Summarizing Large Graphs by Means of Pseudo-Boolean Constraints (BigData'2016)

5. Inconsistency Measurement Thanks to MUS Decomposition (AAMAS'2014)

6. Mining-Based Compression Approach of Propositional Formulae (CIKM'2013)

7. Boolean Satisfiability for Sequence Mining (CIKM'2013)

8. The Top-k Frequent Closed Itemset Mining Using Top-k SAT Problem (ECML/PKDD'2013)

9. Symmetries in Itemset Mining (ECAI'2012)

10. Control-based Clause Sharing in Parallel SAT Solving (IJCAI'2009)
Control-based Clause Sharing in Parallel SAT Solving

Youssef Hamadi

Microsoft Research

7 J J Thomson Avenue, CB3 0FB Cambridge,
United Kingdom, youssefh@microsoft.com

Said Jabbour and Lakhdar Sais

CRIL-CNRS, Université d'Artois

Rue Jean Souvraz SP18, F-62307 Lens,
France, {jabbour,sais} @cril.fr

Abstract

Conflict driven clause learning, one of the most
important component of modern SAT solvers, is
also recognized as very important in parallel SAT
solving. Indeed, it allows clause sharing between
multiple processing units working on related (sub-
)problems. However, without limitation, shar-
ing clauses might lead to an exponential blow up
in communication or to the sharing of irrelevant
clauses. This paper, proposes two innovative poli-
cies to dynamically adjust the size of shared clauses
between any pair of processing units. The first ap-
proach controls the overall number of exchanged
clauses whereas the second additionally exploits
the relevance quality of shared clauses. Experi-
mental results show important improvements of the
state-of the-art parallel SAT solver.

# 1 Introduction

The recent successes of SAT solvers in traditional hardware and software applications have extended their applicability to important new domains. Today, they represent essential low level reasoning components used in general theorem proving, computational biology, AI, etc. This popularity gain is related to their breakthrough on real world instances involving million of clauses and hundred of thousands of variables. These solvers, called modern SAT solvers [Moskewicz et al., 2001; Eén and Sörensson, 2003], are based on a nice combination of (i) clause learning [Marques-Silva and Sakallah, 1996; Moskewicz et al., 2001], (ii) activity-based heuristics [Moskewicz et al., 2001], and (iii) restart policies [Gomes et al., 1998] enhanced with efficient data structures (e.g. watched-literals [Moskewicz et al., 2001]). This architecture is now standard, and today only minor improvements have been observed (cf. SAT competitions). Therefore, it seems difficult to bet on others orders of magnitude gains without a radical algorithmic breakthrough.

Fortunately, the recent generalization of multicore hard-
ware gives parallel processing capabilities to standard PCs.
This represents a real opportunity for SAT researchers which
can now consider parallel SAT solving as an obvious way to-
ward substantial efficiency gains.

Recent works on parallel SAT are all based on the modern
SAT architecture [Moskewicz et al., 2001], and therefore sys-
tematically exploit clause learning as an easy way to extend
the cooperation between processing units. When a unit learns
a new clause, it can share it with all other units in order to
prune their search spaces. Unfortunately, since the number
of potential conflicts is exponential, the systematic sharing
of learnt clauses is not practically feasible. The solution is
to exchange up to some predefined size limit. This has the
advantage of reducing the overhead of the cooperation while
focusing the exchange on short clauses, recognized as more
powerful in term of search pruning.

In this work, our goal is to improve the clause sharing
scheme of modern parallel SAT solvers. Indeed, the ap-
proach based on some predefined size limit has several flaws.
The first and most apparent being that an overestimated value
might induce a very large cooperation overhead, while an un-
derestimated one might completely inhibit the cooperation.
The second flaw comes from the observation that the size of
learnt clauses tends to increase over time (see section 3.1),
leading to an eventual halt of the cooperation. The third flaw
is related to the internal dynamic of modern solvers which
tend to focus on particular subproblems thanks to the activ-
ity/restart mechanisms. In parallel SAT, this can lead two
search processes toward completely different subproblems
where clause sharing becomes pointless.

We propose a dynamic clause sharing policy which uses
pairwise size limits to control the exchange between any pair
of processing units. Initially, high limits are used to en-
force the cooperation, and allow pairwise exchanges. On
a regular basis, each unit considers the number of foreign
clauses received from other units. If this number is be-
low/above a predefined threshold, the pairwise limits are in-
creased/decreased. This mechanism allows the system to
maintain a throughput. It addresses the flaws one and two.
To address the last flaw related to the poor relevance of the
shared clauses, we extend our policy to integrate the qual-
ity of the exchanges. Each unit evaluates the quality of the
received clauses, and the control is able to selectively in-
crease/decrease the pairwise limits based on the underlying
quality of the recently communicated clauses. The rationale
being that the information recently received from a particular
source is qualitatively linked to the information which could
be received from it in the very near future. The evolution
of the pairwise limits w.r.t., the throughput or quality cri-
terion follows an AIMD (Additive-Increase-Multiplicative-
Decrease) feedback control-based algorithm [Chiu and Jain,
1989].

The paper is organized as follows. After some prelimi-
naries (section 2), our dynamic control-based clause sharing
policies are motivated and presented in section 3. The section
4 presents extensive experimental evaluation of our policies
as opposed to a standard static one. The section 5 details pre-
vious parallel SAT works. Finally, we conclude by providing
some interesting future paths of research.

## 2 Technical background

In this section, we introduce the computational features of
modern SAT solvers. Then, we briefly describe the princi-
ple of the AIMD feedback control-based algorithm usually
applied to solve TCP congestion control problems.

## 2.1 Computational features of modern SAT solvers

Most of the state of the art SAT solvers are based on the
Davis, Putnam, Logemann and Loveland procedure, com-
monly called DPLL [Davis et al., 1962]. DPLL is a back-
track search procedure; at each node of the search tree, a de-
cision literal is chosen according to some branching heuris-
tic. Its assignment to one of the two possible values (true or
false) is followed by an inference step that deduces and prop-
agates some forced unit literal assignments. The assigned lit-
erals (decision literal and the propagated ones) are labeled
with the same decision level starting from 1 and increased at
each decision (or branching) until finding a model or reach-
ing a conflict (or a dead end). In the first case, the formula
is answered to be satisfiable, whereas in the second case, we
backtrack to the last decision level and assign the remaining
value to the last decision literal. After backtracking, some
variables are unassigned, and the current decision level is de-
creased accordingly. The formula is answered to be unsat-
isfiable when backtracking to level 0 occurs. In addition to
this basic scheme, modern SAT solvers use additional impor-
tant component such as restart policy, conflict driven clause
learning and activity based heuristics. Let us give some de-
tails on these last two important features. First, to learn from
conflict, they maintain a central data-structure, the implica-
tion graph, which records the partial assignment that is under
construction together with its implications. When a dead end
occurs, a conflict clause (called asserting clause) is generated
by resolution following a bottom-up traversal of the implica-
tion graph. The learning process stops, when a conflict clause
containing only one literal from the current decision level is
generated. Such a conflict clause (or learnt clause) expresses
that such a literal is implied at a previous level. Modern SAT
solvers backtrack to the implication level and assign that lit-
eral to true. Let us mention, that the activity of each variable
encountered during such resolution process is increased. The
variable with greatest activity is selected to be assigned next.

As the number of learnt clauses can grow exponentially,
even in the sequential case, modern SAT solvers regularly re-
duce the data-base of learnt clauses. In the SAT solver Min-
isat [Eén and Sörensson, 2003], such a reduction (called re-
duceDB) is achieved as follows. When the size of the learnt

data base exceeds a given upper bound (B), it is reduced by
half. The set of deleted clauses corresponds to the less active
ones. Initially, B is set to $\frac{1}{3} \times |\mathcal{F}|$ where $|\mathcal{F}|$ is the number
of clauses in the original formula $\mathcal{F}$. At each restart, B is
increased by 10%.

## 2.2 AIMD feedback control based algorithm

The Additive Increase/Multiplicative Decrease (AIMD) algo-
rithm is a feedback control algorithm used in TCP congestion
avoidance. The problem solved by AIMD is to guess the com-
munication bandwidth available between two communicating
nodes. The algorithm performs successive probes, increasing
the communication rate *w* linearly as long as no packet loss
is observed, and decreasing it exponentially when a loss is
encountered. More precisely, the evolution of *w* is defined by
the following *AIMD(a, b)* formula:

* $w = w - a \times w$, if loss is detected

* $w = w + \frac{b}{w}$, otherwise

Different proposals have been made in order to prevent
congestion in communication networks based on different
numbers for *a* and *b*. Today, AIMD is the major component
of TCP's congestion avoidance and control [Jacobson, 1988].
On probe of network bandwidth increasing too quickly will
overshoot limits (underlying capacities). On notice of con-
gestion, decreasing too slowly will not be reactive enough.

In the context of clause sharing, our control policies want
to achieve a particular throughput or a particular throughput
of maximum quality. Since any increase in the size limit
can potentially generate a very large number of new clauses,
AIMD's slow increase can help us to avoid a quick overshoot
of the throughput. Similarly, in case of overshooting, aggres-
sive decrease can help us to quickly reduce clause sharing by
a very large amount.

# 3 Control-based clause sharing in parallel
SAT solving

## 3.1 Motivation

To motivate further our proposed framework, we conducted a
simple experiment using the standard Minisat algorithm [Eén
and Sörensson, 2003]. In figure 1 we show the evolution of
the percentage of learnt clauses of size less than or equal to 8
on a particular family of 16 industrial instances *AProVE07*_*\*_*.
This limit represents the default static clause sharing limit the
ManySAT parallel solver [Hamadi et al., 2009].

This percentage is computed every 10000 conflicts, and as
it can be observed, it decreases over time<fnref n="1" />. Initially, nearly
17% of the learnt clauses could be exchanged but as search
goes on, this percentage falls below 4%. Our observation is
very general and can be performed on different instances with
similar or different clause size limits. It illustrates the second
flaw reported above: the size of learnt clauses tends to in-
crease over time. Consequently, in a parallel SAT setting, any
static limit might lead to an halt of the clause sharing process.
Therefore, if one wants to maintain a quantity of exchange

<footnote n="1">¹The regular small raises are the result of the cyclic reduction of the learnt base through reduceDB.</footnote>
<figure><img src="image_15.png" /><figcaption>Figure 1: Evolution of the percentage of learnt-clauses with size ≤ 8</figcaption></figure>

over time, there does not exist an optimal *static* policy for that. This clearly shows the importance of a dynamic control clause sharing policy.

## 3.2 Throughput and quality based control policies

In this section, we describe our dynamic control-based clause sharing policies which control the exchange between any pair of processing units through dynamic pairwise size limits.

The first policy controls the throughput of clause sharing. Each unit considers the number of foreign clauses received from other units. If this number is below/above a pre-defined throughput-threshold, the pairwise limits are all increased/decreased using an AIMD feedback algorithm. The second policy is an extension of the previous one. It introduces a measure of the quality of foreign clauses. With this information, the increase/decrease of the pairwise limits become proportional to the underlying quality of the clauses shared by each unit. The first (respectively second) policy allows the system to maintain a throughput (respectively throughput of better quality).

We consider a parallel SAT solver with $n$ different processing units. Each unit $u_i$ corresponds to a SAT solver with clause learning capabilities. Each solver can either work on a subspace of the original instance as in divide-and-conquer techniques, or on the full problem, as in ManySAT (see details in sections 5 and 4.1). We assume that these different units communicate through a shared memory (as in multicore architectures).

In our control strategy, we consider a control-time sequence as a set of steps $t_k$ with $t_0 = 0$ and $t_k = t_{k-1} + \alpha$ where $\alpha$ is a constant representing the time window defined in term of number of conflicts. The step $t_k$ of a given unit $u_i$ corresponds to the conflict number $k \times \alpha$ encountered by the solver associated to $u_i$. In the sequel, when there is no ambiguity, we sometimes note $t_k$ simply $k$. Then, each unit $u_i$ can be defined as a sequence of states $S_i^k = (\mathcal{F}, \Delta_i^k, R_i^k)$, where $\mathcal{F}$ is a CNF formula, $\Delta_i^k$ the set of its proper learnt clauses and $R_i^k$ the set of foreign clauses received from the other units between two consecutive steps $k-1$ and $k$. The different units achieve pairwise exchange using pairwise limits. Between two consecutive steps $k-1$ and $k$, a given unit $u_i$ receives from all the other remaining units $u_j$ where $0 \le j < n$ and $j \ne i$ a set of learnt clauses $\Delta_{j \to i}^k$ of length less or equal to

a size limit $e_{j \to i}^k$ i.e., $\Delta_{j \to i}^k = \{c \in \Delta_j^k / |c| \le e_{j \to i}^k\}$. Then, the set $R_i^k$ can be formally defined as $\cup_{0 \le j < n, j \ne i} \Delta_{j \to i}^k$.

Using a fixed throughput threshold $T$ of shared clauses, we describe our control-based policies which allow each unit $u_i$ to guide the evolution of the size limit $e_{j \to i}$ using an AIMD feedback mechanism.

### Throughput based control

As illustrated in figure 2, at step $k$ a given unit $u_i$ checks whether the throughput is exceeded or not. If $|R_i^k| < T$ (respectively $|R_i^k| > T$) the size limit $e_{j \to i}^{k+1}$ is additively increased (respectively multiplicatively decreased). More formally, the upper bound $e_{j \to i}^{k+1}$ on the size of clauses that a solver $j$ shares with the solver $i$ between $k$ and $k+1$ are changed using the following AIMD function:

$$ \begin{array}{l} \text{aimdT}(R_i^k) \{ \\ \quad \forall j | 0 \le j < n, j \ne i \\ \quad e_{j \to i}^{k+1} = \left\{ \begin{array}{ll} e_{j \to i}^k + \frac{b}{e_{j \to i}^k}, & \text{if } (|R_i^k| < T) \\ e_{j \to i}^k - a \times e_{j \to i}^k, & \text{if } (|R_i^k| > T) \end{array} \right\} \quad \text{where } a \\ \text{and } b \text{ are positive constants.} \end{array} $$

<figure><img src="image_16.png" /><figcaption>Figure 2: Throughput based control policy</figcaption></figure>

### Throughput and quality based control

In this policy, to control the throughput of a given unit $u_i$, we introduce a quality measure $Q_{j \to i}^k$ (see definition 1) to estimate the relative quality of the clauses received by $u_i$ from $u_j$. In the throughput and quality based control policy, the evolution of the size limit $e_{j \to i}^k$ is related to the estimated quality.

Our quality measure is defined using the activity of the variables at the basis of VSIDS heuristic [Moskewicz et al., 2001] another important component of modern SAT solvers. The variables with greatest activity represent those involved in most of the (recent)-conflicts. Indeed, when a conflict occurs, the activity of the variables whose literals appear in the clauses encountered during the generation of a learnt clause are updated. The most active variables are those related to the current part of the search space. Consequently, our quality measure exploits these activities to quantify the relevance of a clause learnt by unit $u_j$ to the current state of a given unit $u_i$. To define our quality measure, suppose that, at any
time of the search process, we have $A_i^{max}$ the current maximal activity of $u_i$'s variables, and $A_i(x)$ the current activity of a given variable $x$.

**Definition 1 (Quality)** Let $c$ be a clause and $\mathcal{L}_{A_i}(c) = \{x/x \in c \text{ s.t. } A_i(x) \ge \frac{A_i^{max}}{2}\}$ the set of active literals of $c$ with respect to unit $u_i$. We define $\mathcal{P}_{j \to i}^k = \{c/c \in \Delta_{j \to i}^k \text{ s.t. } |\mathcal{L}_{A_i}(c)| \ge Q\}$ be the set of clauses received by $i$ from $j$ between steps $k-1$ and $k$ with at least $Q$ active literals. We define the quality of clauses sent by $u_j$ to $u_i$ at a given step $k$

$$ \text{as } Q_{j \to i}^k = \frac{|\mathcal{P}_{j \to i}^k| + 1}{|\Delta_{j \to i}^k| + 1} $$

Our throughput and quality based control policy change the upper bound $e_{j \to i}^{k+1}$ on the size of clauses that a solver $j$ shares with the solver $i$ between $k$ and $k+1$ using the following AIMD function:

$$ \begin{array}{l} \text{aimdTQ}(R_i^k) \{ \\ \quad \forall j | 0 \le j < n, j \ne i \\ \quad e_{j \to i}^{k+1} = \begin{cases} e_{j \to i}^k + \left( \frac{Q_{j \to i}^k}{100} \right) \times \frac{b}{e_{j \to i}^k}, & \text{if } (|R_i^k| < T) \\ e_{j \to i}^k - \left( 1 - \frac{Q_{j \to i}^k}{100} \right) \times a \times e_{j \to i}^k, & \text{if } (|R_i^k| > T) \end{cases} \\ \} \text{ where } a \text{ and } b \text{ are positive constants.} \end{array} $$

As shown by the AIMD function of the throughput and quality based control policy, the adjustment of the size limit depends on the quality of shared clauses. Indeed, as it can be seen from the above formula, when the exchange quality between $u_j$ and $u_i$ ($Q_{j \to i}^k$) tends to 100% (respectively 0%), then the increase in the limit size tends to be maximal (respectively minimal) while the decrease tends to be minimal (respectively maximal). Our aim in this second policy is to maintain a throughput of good quality. The rationale being that the information recently received from a particular source is qualitatively linked to the information which could be received from it in the very near future.

# 4 Evaluation

## 4.1 The parallel SAT solver

Our policies were implemented and tested on top of the ManySAT parallel SAT solver [Hamadi et al., 2009] which won the parallel track of the 2008 SAT-Race<fnref n="2" />. ManySAT includes all the classical features like two-watched-literal, unit propagation, activity-based decision heuristics, lemma deletion strategies, and clause learning. In addition to the classical first-UIP scheme, it incorporates a new technique which extends the classical implication graph used during conflict-analysis to exploit the satisfied clauses of a formula [Audemard et al., 2008].

Unlike others parallel SAT solvers, ManySAT does not implement a divide-and-conquer strategy based on some dynamic partitioning of the search space. At contrary, it uses a portfolio philosophy which lets several sequential DPLLs compete and cooperate to be the first to solve the common instance. These DPLLs are differentiated in many ways. They

use different and complementary restart strategies, VSIDS and polarity heuristics, and learning schemes. Additionally, all the DPLLs are exchanging learnt clauses up to some static size limit.

## 4.2 Experiments

Our tests were done on Intel Xeon Quadcore machines with 16GB of RAM running at 2.3Ghz. We used a timeout of 1500 seconds for each problem. ManySAT was used with 4 DPLLs strategies each one running on a particular core (unit). To alleviate the effects of unpredictable threads scheduling, each problem was solved three times and the average was taken.

Our dynamic clause sharing policies were added to ManySAT and compared against ManySAT with its default static policy ManySAT e=8 which exchanges clauses up to size 8. Remark that since each pairwise limit is read by a unit, and updated by another one, our proposal can be integrated without any lock.

We have selected $a = 0.125$, $b = 8$ for aimdT and aimdTQ, associated to a time window of $\alpha = 10000$ conflicts. The throughput $T$ is set to $\frac{\alpha}{2}$ and the upper bound $Q$ on the number of active literals per clause $c$ is set to $\frac{|c|}{3}$ (see definition 1). Each pairwise limit $e_{j \to i}$ was initialized to 8.

## 4.3 Industrial problems

The Table 1 presents the results on the 100 industrial problems of the 2008 SAT-Race. The problem set contains families with several instances or individual instances.

From left to right we present, the family/instance name, the number of instances per family. Results associated to the standard ManySAT, with the number of problems solved before timeout, and the associated average runtime. The right part reports results for the two dynamic policies. For each dynamic policy we provide $\bar{e}$, the average of the $e_{j \to i}$ observed during the computation. The last row provides for each method, the total number of problems solved, and the cumulated runtime. For the dynamic policies, it also presents the average of the $\bar{e}$ values.

At that point we have to stress that the static policy ($e = 8$) is optimal in the way that it gives the best average performance on this set of problems. We can observe that the static policy solves 83 problems while the dynamic policies aimdT and aimdTQ solve respectively 86 and 89 problems. Except on the ibm\* and manol\* families, the dynamic policies always exhibit a runtime better or equivalent to the static one. Unsurprisingly, when the runtime is significant but does not drastically improve over the static policy, the values of $\bar{e}$ are often close to 8, i.e., equivalent to the static size limit. When we consider the last row, we can see that the aimdT is faster than the aimdTQ. However, this last policy solves more problems. We can explain this as follows. The quality-based policy intensifies the search by favoring the exchange of clauses related to the current exploration of each unit. This intensification leads to the resolution of more difficult problems. However, it increases the runtime on easier instances where a more diversified search is often more beneficial. Overall these results are very good since our dynamic policies are able to outperform the best possible static tuning.

<footnote n="2">²http://baldur.iti.uka.de/sat-race-2008/</footnote>
<table><caption>Table 1: SAT-Race 2008, industrial problems</caption><thead><tr><th rowspan="2">family/instance</th><th rowspan="2">#inst</th><th colspan="2">ManySAT e=8</th><th colspan="3">ManySAT aimdT</th><th colspan="3">ManySAT aimdTQ</th></tr><tr><th>#Solved</th><th>time(s)</th><th>#Solved</th><th>time(s)</th><th>e&#773;</th><th>#Solved</th><th>time(s)</th><th>e&#773;</th></tr></thead><tbody><tr><td>ibm.*</td><td>20</td><td>19</td><td><strong>204</strong></td><td>19</td><td>218</td><td>7</td><td>19</td><td>286</td><td>6</td></tr><tr><td>manol.*</td><td>10</td><td>10</td><td><strong>117</strong></td><td>10</td><td><strong>117</strong></td><td>8</td><td>10</td><td>205</td><td>7</td></tr><tr><td>mizh.*</td><td>10</td><td>6</td><td>762</td><td>7</td><td>746</td><td>6</td><td><strong>10</strong></td><td><strong>441</strong></td><td>5</td></tr><tr><td>post.*</td><td>10</td><td>9</td><td>325</td><td>9</td><td><strong>316</strong></td><td>7</td><td>9</td><td>375</td><td>7</td></tr><tr><td>velev.*</td><td>10</td><td>8</td><td>585</td><td>8</td><td><strong>448</strong></td><td>5</td><td>8</td><td>517</td><td>7</td></tr><tr><td>een.*</td><td>5</td><td>5</td><td>2</td><td>5</td><td>2</td><td>8</td><td>5</td><td>2</td><td>7</td></tr><tr><td>simon.*</td><td>5</td><td>5</td><td>111</td><td>5</td><td>84</td><td>10</td><td>5</td><td><strong>59</strong></td><td>9</td></tr><tr><td>bmc.*</td><td>4</td><td>4</td><td>7</td><td>4</td><td>7</td><td>7</td><td>4</td><td><strong>6</strong></td><td>9</td></tr><tr><td>gold.*</td><td>4</td><td>1</td><td>1160</td><td>1</td><td><strong>1103</strong></td><td>12</td><td>1</td><td>1159</td><td>12</td></tr><tr><td>anbul.*</td><td>3</td><td>2</td><td>742</td><td><strong>3</strong></td><td><strong>211</strong></td><td>11</td><td>3</td><td>689</td><td>11</td></tr><tr><td>babic.*</td><td>3</td><td>3</td><td>2</td><td>3</td><td>2</td><td>8</td><td>3</td><td>2</td><td>8</td></tr><tr><td>schup.*</td><td>3</td><td>3</td><td>129</td><td>3</td><td><strong>120</strong></td><td>5</td><td>3</td><td>160</td><td>5</td></tr><tr><td>fuhs.*</td><td>2</td><td>2</td><td>90</td><td>2</td><td><strong>59</strong></td><td>11</td><td>2</td><td>77</td><td>10</td></tr><tr><td>grieu.*</td><td>2</td><td>1</td><td>783</td><td>1</td><td><strong>750</strong></td><td>8</td><td>1</td><td><strong>750</strong></td><td>8</td></tr><tr><td>narain.*</td><td>2</td><td>1</td><td>786</td><td>1</td><td><strong>776</strong></td><td>8</td><td>1</td><td>792</td><td>8</td></tr><tr><td>palac.*</td><td>2</td><td>2</td><td>20</td><td>2</td><td><strong>8</strong></td><td>3</td><td>2</td><td>54</td><td>7</td></tr><tr><td>aloul-chnl11-13</td><td>1</td><td>0</td><td>1500</td><td>0</td><td>1500</td><td>11</td><td>0</td><td>1500</td><td>10</td></tr><tr><td>jarvi-eq-atree-9</td><td>1</td><td>1</td><td>70</td><td>1</td><td>69</td><td>25</td><td>1</td><td><strong>43</strong></td><td>17</td></tr><tr><td>marijn-philips</td><td>1</td><td>0</td><td>1500</td><td><strong>1</strong></td><td>1133</td><td>34</td><td>1</td><td><strong>1132</strong></td><td>29</td></tr><tr><td>maris-s03-gripper11</td><td>1</td><td>1</td><td>11</td><td>1</td><td>11</td><td>10</td><td>1</td><td>11</td><td>8</td></tr><tr><td>vange-col-abb313gpia-9-c</td><td>1</td><td>0</td><td>1500</td><td>0</td><td>1500</td><td>12</td><td>0</td><td>1500</td><td>12</td></tr></tbody><tfoot><tr><td>Total/(average)</td><td>100</td><td>83</td><td>10406</td><td>86</td><td>9180</td><td>(10.28)</td><td>89</td><td>9760</td><td>(9.61)</td></tr></tfoot></table>

## 4.4 Crafted problems

We present here results on the crafted category (201 problems) of the 2007 SAT-competition. These problems are hand made and many of them are designed to beat all the existing SAT solvers. It contains for example Quasi-group instances, forced random SAT instances, counting, ordering and pebbling instances, social golfer problems, etc.

The scatter plot (in log scale) given in figure 3 (left hand side) illustrates the comparative results of the static and dynamic throughput version of ManySAT. The x-axis (resp. y-axis) corresponds to the CPU time $tx$ (resp. $ty$) obtained by ManySAT e=8 (resp. ManySAT aimdT). Each dot with $(tx, ty)$ coordinates corresponds to a SAT instance. Dots below (resp. above) the diagonal indicate that ManySAT aimdT is faster (resp. slower) than ManySAT e=8. The results clearly exhibit that the throughput based policies outperform the static policy on the crafted category. These improvements are illustrated in the figure 3 (right hand side) which shows the time in seconds needed to solve a given number of instances ($\#instances$). We can observe that both aimdT ($\bar{e} = 23.14$ with a peak at 94) and aimdTQ ($\bar{e} = 26.17$ with a peak at 102) solve 7 more problems than the static policy. Like for the previous problem category, aimdT remains faster than aimdTQ. We can explain this as follows. It seems that since by definition, these problems do not have a structure which can be advantageously exploited by an intensification process, the higher diversification provided by aimdT allows better performances.

## 4.5 The dynamic of $\bar{e}$

It is interesting to consider the evolution of $\bar{e}$, the average of the $e_{j \to i}$ observed during the computation. In Figure 1 it was shown on the 16 instances of the AProVE07_* family that the size of learnt clauses was increasing over time.

We present in figure 4 the evolution of $\bar{e}$ with ManySAT aimdT on the same family. The evolution is given for each unit (core0 to core3), and the average of the units is also pre-

<figure><img src="image_17.png" /><figcaption>Figure 4: ManySAT aimdT: $\bar{e}$ on the AProVE07_* family</figcaption></figure>

sented (average). We can see that our dynamic policy overcomes the disappearing of “small” clauses by the incremental raising of the pairwise limits. It presents a typical saw tooth behavior that represents the probe for throughput $T$. This Figure and our results on the industrial and crafted problems show that the evolution of the pairwise limits if not bounded, does not reach unacceptable levels.

## 5 Previous works

We do not present parallel SAT solvers which predate the introduction of the modern DPLL architecture since these works did not use clause sharing.

The first parallel SAT solver based on a modern DPLL is Gradsat [Chrabakh and Wolski, 2003] which extends the zChaff solver with a master-slave model, and implements guiding-paths to divide the search space of a problem. These paths are represented by a set of unit clauses added to the original formula. Additionally, learned clauses are exchanged between all clients if they are smaller than a predefined limit on the number of literals.

[Blochinger et al., 2003] uses an architecture similar to
<figure><img src="image_18.png" /><figcaption>Figure 3: SAT-Competition 2007, crafted problems</figcaption></figure>

Gradsat. However, a client incorporates a foreign clause if it is not subsumed by the current guiding-path constraints.

MiraXT is designed for shared memory multiprocessors systems [Lewis *et al.*, 2007]. It uses a divide and conquer approach where threads share a unique clause database which represents the original and the learnt clauses. Therefore in this system all the learnt clauses are shared.

pMiniSat uses a standard divide-and-conquer approach based on guiding-paths [Chu and Stuckey, 2008]. It exploits these paths to improve clause sharing. When considered with the knowledge of the guiding path of a particular thread, a clause can become small and therefore highly relevant. This allows pMiniSat to extend the sharing of clauses since a large clause can become small in another search context.

Let us remark that pMiniSat and MiraXT were respectively ranked second and third of the 2008 SAT-Race while ManySAT (presented in section 4.1) finished first.

## 6 Conclusion

We have presented two dynamic clause sharing policies for parallel SAT solving. They use an AIMD feedback controlled algorithm to dynamically adjust the size of shared clauses between any pair of processing units. Our first policy maintains an overall number of exchanged clauses (throughput) whereas the second additionally exploits the relevance quality of shared clauses. These policies have been devised as an efficient answer to the various flaws of the classical static size limit policy. The experimental results comparing our proposed dynamic policies against the static policy show important improvements for the state-of-the-art parallel SAT solver ManySAT. It allows this solver to solve 6 more industrial and 7 more crafted problems. Our proposed framework opens interesting perspectives. For example, the design of new relevant quality measures for clause sharing is of great importance. It could benefit to sequential solver to improve their learnt base reduction strategy and as demonstrated by this work have an important impact in parallel SAT solving.

## References

[Audemard *et al.*, 2008] G. Audemard, L. Bordeaux, Y. Hamadi, S. Jabbour, and L. Sais. A generalized

framework for conflict analysis. In Proc. of SAT, pages 21–27, 2008.

[Blochinger *et al.*, 2003] W. Blochinger, C. Sinz, and W. Küchlin. Parallel propositional satisfiability checking with distributed dynamic learning. *Parallel Computing*, 29(7):969–994, 2003.

[Chiu and Jain, 1989] D-M Chiu and R. Jain. Analysis of the increase and decrease algorithms for congestion avoidance in computer networks. *Comp. Networks*, 17:1–14, 1989.

[Chrabakh and Wolski, 2003] W. Chrabakh and R. Wolski. GrADSAT: A parallel sat solver for the grid. Technical report, UCSB CS TR N. 2003-05, 2003.

[Chu and Stuckey, 2008] G. Chu and P. J. Stuckey. Pminisat: a parallelization of minisat 2.0. Technical report, SAT-Race 2008, solver description, 2008.

[Davis *et al.*, 1962] M. Davis, G. Logemann, and D. W. Loveland. A machine program for theorem-proving. *Comm. of the ACM*, 5(7):394–397, 1962.

[Eén and Sörensson, 2003] N. Eén and N. Sörensson. An extensive sat-solver. In Proc. of SAT’03, pages 502–518, 2003.

[Gomes *et al.*, 1998] C. P. Gomes, B. Selman, and H. Kautz. Boosting combinatorial search through randomization. In Proc. AAAI’98, pages 431–437, 1998.

[Hamadi *et al.*, 2009] Y. Hamadi, S. Jabbour, and L. Sais. ManySAT: a parallel SAT solver. *Journal on Satisfiability, Boolean Modeling and Computation (JSAT)*, to appear, 2009.

[Jacobson, 1988] V. Jacobson. Congestion avoidance and control. In Proc. SIGCOMM ’88, pages 314–329, 1988.

[Lewis *et al.*, 2007] M. Lewis, T. Schubert, and B. Becker. Multithreaded sat solving. In Proc. ASP DAC’07, 2007.

[Marques-Silva and Sakallah, 1996] J. P. Marques-Silva and K. A. Sakallah. GRASP - A New Search Algorithm for Satisfiability. In Proc. of IEEE/ACM CAD’96, pages 220–227, 1996.

[Moskewicz *et al.*, 2001] M.W. Moskewicz, C.F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In *DAC’01*, pages 530–535, 2001.
# Symmetries in Itemset Mining

Said Jabbour and Lakhdar Sais and Yakoub Salhi and Karim Tabia¹

**Abstract.** In this paper, we describe a new framework for breaking symmetries in itemset mining problems. Symmetries are permutations between items that leave invariant the transaction database. Such kind of structural knowledge induces a partition of the search space into equivalent classes of symmetrical itemsets. Our proposed framework aims to reduce the search space of possible interesting itemsets by detecting and breaking symmetries between items. Firstly, we address symmetry discovery in transaction databases. Secondly, we propose two different approaches to break symmetries in a preprocessing step by rewriting the transaction database. This approach can be seen as an original extension of the symmetry breaking framework widely used in propositional satisfiability and constraint satisfaction problems. Finally, we show that Apriori-like algorithms can be enhanced by dynamic symmetry reasoning. Our experiments clearly show that several itemset mining instances taken from the available datasets contain such symmetries. We also provide experimental evidence that breaking such symmetries reduces the size of the output on some families of instances.

## 1 Introduction

The problem of mining frequent itemsets is well-known and essential in data mining, knowledge discovery and data analysis. It has applications in various fields and becomes fundamental for data analysis as datasets and datastores are becoming very large. Since the first article of Agrawal [15] on association rules and itemset mining, the huge number of works, challenges, datasets and projects show the actual interest in this problem (see [17] for a recent survey of works addressing this problem). 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, episode mining, etc. Important progress has been achieved for data mining and knowledge discovery in terms of implementations, platforms, libraries, etc. Nevertheless, the majority of works developed solutions and tools specifically tuned and designed to achieve very specific goals on specific data mining tasks. The algorithmic issues represent the most important problem for the majority of works. As pointed out in [17], lot of works deal with designing highly scalable itemset mining algorithms for large scale datasets. The existing algorithms mainly differ in the way they explore the itemset search space, how the anti-monotonicity property is used and how the dataset is handled. Another important problem of itemset mining and data mining problems in general, concerns the huge size of the output, from which it is difficult to retrieve useful information. Consequently, for practical data mining, it is important to reduce the size of the output, by exploiting the structure of the itemsets data.

Computing for example, closed, maximal, condensed, discriminative itemset patterns are some of the well-known and useful techniques.

Symmetry between items is another kind of structural information that might be recovered from the transaction databases and used to further reduce the size of the output by limiting the search space. Symmetries are a fundamental concept in computer science, mathematics, physics and many other domains. Many human artifacts (e.g. classroom in a university, aircraft seats, circuit patterns) and entities in nature (e.g. plants, molecules, DNA sequences, atoms) exhibits symmetries. Such symmetries allow us to reason and to understand more complex entities and systems. For example, this kind of structures has been widely exploited in constraint satisfaction (CSP) and propositional satisfiability (SAT) problems. As far as we know, symmetry reasoning has been first introduced by Krishnamurthy [9] to shorten resolution proofs in propositional logic. He shows that a resolution proof system augmented with the symmetry rule is more powerful than resolution. In [2], the authors showed how dynamic symmetry detection and elimination can lead to significant improvements of several automated deduction techniques. In constraint satisfaction problems, a weaker form of symmetry called value interchangeability is first introduced by E. Freuder in [6], while variable and value symmetry are studied in [14]. Symmetry breaking using additional constraints has been proposed independently by James Crawford in the context of first order [3] and propositional [4] logic theories and by Jean-François Puget in CSP [14]. More recent contributions clearly show that symmetry remains an active research area in both CSP and SAT.

To the best of our knowledge, in the context of data mining and particularly for the itemset mining problem, symmetries have not received much attention. Let us mention two related works addressing a particular case of general symmetries considered in this paper [13, 12]. Indeed, this restricted form of symmetry, called pairwise items symmetry, is obtained by exchanging two items, while leaving the remaining items unchanged. This is clearly a restriction of the general symmetry principle. In [13], an efficient ZBDD algorithm for detecting pairwise symmetries is proposed and the property of symmetric items in transaction database are discussed. Pairwise items symmetries, called clone items, have been proposed by Medina and Nourine [7] to explain why sometimes, the number of rules of a minimum cover of a relation is exponential in the number of items of the relation. More recently, in the context of constraint programming for k-pattern set mining, Guns et al. [8] used symmetry breaking constraints to impose a strict ordering on the patterns in the pattern set.

In this paper, we propose a theoretical framework for dealing with general symmetries in itemset mining problems. We first propose an adaptation of the symmetry detection method usually used in propositional satisfiability [3, 1] to transaction databases. As this hidden structure can be very helpful for reducing the search space, we show how they can be integrated dynamically in Apriori-like al-

¹ Univ Lille Nord de France, F-59000 Lille, France. UArtois, CRIL UMR CNRS 8188, F-62300 Lens, France. {jabbour, sais, salhi, tabia}@cril.univ-artois.fr
gorithms to prune the set of possible candidate patterns. Then, we propose two symmetry breaking approaches to eliminate symmetries in transaction databases in a preprocessing step. Our proposed symmetry breaking methods eliminate items from the original transaction database. The frequent itemsets generated using the new transaction database together with the symmetry group can be used to retrieve the whole set of frequent itemsets of the original transaction database. This can be seen as a form of condensed representation of the output. A condensed representation is originally proposed by Mannila and Toivenen in [10]. For frequent itemsets, a condensed representation is a collection of itemsets that still contains the same information.

On the practical side and to show the usefulness of exploiting symmetries in itemset mining problems, we present an experimental evaluation of both symmetry detection and symmetry breaking on some benchmark instances.

## 2 Preliminary definitions and notations

Let $\mathcal{I}$ be a set of items. A set $I \subseteq \mathcal{I}$ is called an itemset. A transaction is a couple $(tid, I)$ where $tid$ is the transaction identifier and $I$ is an itemset. A transaction database is a finite set of transactions over $\mathcal{I}$ where for each two different transactions, they do not have the same transaction identifier. We note $\mathcal{T}_{id}(\mathcal{D}) = \{tid | (tid, I) \in \mathcal{D}\}$ the set of transaction identifiers associated to $\mathcal{D}$. We use $\mathcal{I}_{items}(\mathcal{O})$ to denote the set of all the items appearing in the syntactic object $\mathcal{O}$ (e.g. a transaction database, itemset, etc). We say that a transaction $(tid, I)$ supports an itemset $J$ if $J \subseteq I$.

The cover of an itemset $I$ in a transaction database $\mathcal{D}$ is the set of identifiers of transactions in $\mathcal{D}$ supporting $I$: $C(I, \mathcal{D}) = \{tid | (tid, J) \in \mathcal{D} \text{ and } I \subseteq J\}$. The support of an itemset $I$ in $\mathcal{D}$ is defined by: $\text{Supp}(I, \mathcal{D}) = |C(I, \mathcal{D})|$. Moreover, the frequency of $I$ in $\mathcal{D}$ is defined by: $\mathcal{F}(I, \mathcal{D}) = \frac{\text{Supp}(I, \mathcal{D})}{|\mathcal{D}|}$.

**Example 1** Let us consider the following transaction database over the set of items $\mathcal{I} = \{Spaghetti, Tomato, Parmesan, Beef, Olive oil, Mozzarella, Chili pepper, Anchovies, Eggs\}$:

<table><caption>**Table 1.** An example of transaction database $\mathcal{D}$</caption><thead><tr><td>tid</td><td>itemset</td></tr></thead><tbody><tr><td>001</td><td>Spaghetti, Olive oil, Tomato, Mozzarella</td></tr><tr><td>002</td><td>Spaghetti, Parmesan, Olive oil, Beef</td></tr><tr><td>003</td><td>Chili pepper, Anchovies</td></tr><tr><td>004</td><td>Eggs</td></tr></tbody></table>

For instance, we have $\text{Supp}(\{Spaghetti, Olive oil\}, \mathcal{D}) = |\{001, 002\}|=2$ and $\mathcal{F}(\{Spaghetti, Olive oil\}, \mathcal{D})=0.5$.

Let $\mathcal{D}$ be a transaction database over $\mathcal{I}$ and $\lambda$ a minimal support threshold.

**Proposition 1 (Anti-Monotonicity)** Let $I_1$ and $I_2$ be two itemsets such that $I_1 \subseteq I_2$. If $\text{Supp}(I_2, \mathcal{D}) \ge \lambda$ then $\text{Supp}(I_1, \mathcal{D}) \ge \lambda$.

**Definition 1 (Frequent Itemset Mining Problem)** The frequent itemset mining problem consists in computing the following set:

$$ \mathcal{FIM}(\mathcal{D}, \lambda) = \{I \subseteq \mathcal{I} | \text{Supp}(I, \mathcal{D}) \ge \lambda\} $$

**Definition 2 (Transaction Renaming)** Let $\mathcal{D}$ be a transaction database. A renaming $f$ over $\mathcal{T}_{id}(\mathcal{D})$ is a bijective mapping from $\mathcal{T}_{id}(\mathcal{D})$ to $\mathcal{T}_{id}(\mathcal{D})$.

We can extend a renaming $f$ to $\mathcal{D}$ as follows: $f(\mathcal{D}) = \{(f(tid), I)|(tid, I) \in \mathcal{D}\}$.

## 3 Symmetry in Frequent Itemset Mining

**Definition 3 (Permutation)** A permutation $\sigma$ over $\mathcal{I}$ is a bijective mapping from $\mathcal{I}$ to $\mathcal{I}$.

Let $\mathcal{D}$ be a transaction database. We can extend a permutation $\sigma$ to $\mathcal{D}$ as follows: $\sigma(\mathcal{D}) = \{(tid, \sigma(I))|(tid, I) \in \mathcal{D}\}$ where $\sigma(I) = \{\sigma(a)|a \in \mathcal{I}\}$.

We denote by $\mathcal{P}(\mathcal{I})$ the set of all the permutations over $\mathcal{I}$ and $\circ$ is the composition operation over the elements of $\mathcal{P}(\mathcal{I})$. It is easy to see that $(\mathcal{P}(\mathcal{I}), \circ)$ is a group where the identity permutation is a neutral element. $(S', \circ)$ is a sub-group of the group $(\mathcal{P}(\mathcal{I}), \circ)$ if and only if $(S', \circ)$ is a group and $S' \subseteq \mathcal{P}(\mathcal{I})$. A generating set of the group $(S, \circ)$ is a subset $\Sigma$ of $S$ such that every element of the group can be obtained from the combination of finitely many elements of $\Sigma$ and their inverses, and we write $S = \langle \Sigma \rangle$.

Each permutation $\sigma$ can be represented by a set of cycles $c_1, \dots, c_n$ where each cycle $c_i = (a_1, \dots, a_k)$ is a list of elements of $\mathcal{I}$ such that $\sigma(a_j) = a_{j+1}$ for $j = 1, \dots, k-1$, and $\sigma(a_k) = a_1$. In the sequel, for clarity reasons, we omit cycles of the form $(a, a)$ in the description of permutations and symmetries.

**Definition 4 (Orbit)** Let $(S, \circ)$ be a sub-group of $(\mathcal{P}(\mathcal{I}), \circ)$. The orbit $a^S$ of an item $a \in \mathcal{I}$ on which $(S, \circ)$ acts is $a^S = \{\sigma(a)|\sigma \in S\}$.

When there is no ambiguity, we note $a^S$ simply $[a]$.

**Definition 5 (Symmetry)** Let $\mathcal{D}$ be a transaction database. A symmetry of $\mathcal{D}$ is a permutation $\sigma \in \mathcal{P}(\mathcal{I})$ such that there exists a transaction renaming $f$ over $\mathcal{T}_{id}(\mathcal{D})$ where $\sigma(\mathcal{D}) = f(\mathcal{D})$ i.e. $f^{-1}(\sigma(\mathcal{D})) = \mathcal{D}$.

**Example 2** Let us consider again the transaction database given in Table 1. $\sigma = (\text{Tomato, Parmesan})(\text{Mozzarella, Beef})$ ($\text{Chili pepper, Anchovies}$) is a symmetry because $\sigma(\mathcal{D}) = f(\mathcal{D})$ where $f$ is a transaction renaming defined as follows:

$$ f(x) = \begin{cases} 002 & \text{if } x=001 \\ 001 & \text{if } x=002 \\ x & \text{otherwise} \end{cases} $$

Let $\mathcal{S}(\mathcal{D})$ be the set of all the symmetries. One can see that $(\mathcal{S}(\mathcal{D}), \circ)$ is a sub-group of $(\mathcal{P}(\mathcal{I}), \circ)$.

**Definition 6** Let $\mathcal{D}$ be a transaction database. Two items $a, b \in \mathcal{I}_{items}(\mathcal{D})$ are symmetric if there exists a symmetry $\sigma$ of $\mathcal{D}$ such that $\sigma(a) = b$.

The following proposition is immediate:

**Proposition 2** Let $\mathcal{D}$ be a transaction database and $a \in \mathcal{I}_{items}(\mathcal{D})$. All the items in $a^{\mathcal{S}(\mathcal{D})}$ are symmetrical two by two.

**Proposition 3** Let $\mathcal{D}$ be a transaction database, $\sigma$ a symmetry of $\mathcal{D}$, $\lambda$ a minimal support threshold and $I$ an itemset. $I \in \mathcal{FIM}(\mathcal{D}, \lambda)$ iff $\sigma(I) \in \mathcal{FIM}(\mathcal{D}, \lambda)$.

**Proof:** Since there exists a transaction renaming $f$ such that $\sigma(\mathcal{D}) = f(\mathcal{D})$, it is easy to see that $\sigma(I) \in \mathcal{FIM}(f(\mathcal{D}), \lambda)$ and consequently $\sigma(I) \in \mathcal{FIM}(\mathcal{D}, \lambda)$. $\square$
## 4 Symmetry Detection in Transaction Databases

In this section, we describe symmetry detection in transaction databases. One of the most popular means of discovering symmetries of a problem is to first convert the problem into a graph, and employ a general-purpose graph symmetry tool to uncover the symmetries [1]. These symmetries can then be reflected back into the original problem. The oldest and most established graph symmetry program is McKays Nauty [11]. Most of the available symmetry detection tools convert the original problem into a colored undirected graph, where vertices are labeled with colors. Such colored vertices are considered when searching for automorphism on the graph (i.e. vertices with different colors can not be permuted to each other).

**Definition 7** A colored undirected graph is a triplet $G = (V, E, \eta)$ with vertex set $V$ and edge set $E \in V^2$ and $\eta$ is a function from $V$ to $N$ that associates a positive integer (a color) to each vertex.

**Definition 8** A permutation $\sigma$ of $V$ is a symmetry of $G$ iff $\sigma(G) = G$ or equivalently $\sigma(E) = E$.

**Definition 9** A symmetry $\sigma$ of $G$ respects a partition $\pi$ of $V$ if for each $v \in V$, $v$ and $\sigma(v)$ belong to the same cell of $\pi$. The set of all symmetries of $G$ with respect to a partition $\pi$ is called the automorphism group of $G$ under $\pi$ and is denoted $A(G)_{\pi}$.

We now show how a transaction database can be encoded as a colored undirected graph.

**Definition 10 (From $D$ to $G$)** Let $\mathcal{I}$ be a set of items and $\mathcal{D}$ a transaction database over $\mathcal{I}$. We define the colored undirected graph $G$ associated to $\mathcal{D}$ as $G(\mathcal{D}) = (V, E, \eta)$ where $V = \mathcal{I} \cup T_{id}(\mathcal{D})$, $E = \{(tid, i) | \exists (tid, I) \in \mathcal{D}, i \in \mathcal{I}\}$ and $\forall v \in V$,

$$ \eta(v) = \begin{cases} 0 & \text{if } v \in \mathcal{I} \\ 1 & \text{otherwise } v \in T_{id}(\mathcal{D}) \end{cases} $$

Let us note that $\pi = \{\{v|v \in V, \eta(v) = 0\}, \{v|v \in V, \eta(v) = 1\}\}$ is the initial partition of $V$. Several refinements have been proposed to improve the partition $\pi$. The goal of these refinements is to reduce the search space by distinguishing as much as possible non symmetric vertices using vertex invariant such as vertex degree (e.g. [5]).

The conversion of the transaction database $\mathcal{D}$ given in Example 1 to a colored undirected graph $G(\mathcal{D})$ is depicted in Figure 1. For simplicity, we use the first letter of each item name in lower case (e.g. e for Eggs). In the figure we distinguish two kinds of nodes, items represented by circles (color 1) and transaction identifiers represented by rectangles (color 2).

<figure><img src="image_19.png" /><figcaption>**Figure 1.** From transaction database $\mathcal{D}$ to colored graph $G(\mathcal{D})$</figcaption></figure>

With this construction, there is a one to one mapping between symmetries in the transaction database and the automorphisms of

the colored undirected graph. Given $G(\mathcal{D})$ and an initial partition $\pi$, the goal is to compute $A(G(\mathcal{D}))_{\pi}$. Using NAUTY [11], one can find the automorphisms that leave $G(\mathcal{D})$ invariant. For example, $A = (t, p)(m, b)(c, a)(o)(s)(e) [(001, 002)(003)(004)]$ is an automorphism of $G(\mathcal{D})$. The corresponding symmetry $\sigma$ is obtained from $A$ by projection on the set of items $\mathcal{I}$ of $\mathcal{D}$.

## 5 Symmetry Pruning

In this section, we show how symmetries can be used by classical enumeration algorithms such as Apriori to reduce the set of possible candidate patterns.

The Apriori algorithm is an algorithm for mining frequent itemsets for association rules [15]. It proceeds by a level-wise search of the elements of $FIM(D, \lambda)$. Namely, it starts by computing the elements of $FIM(D, \lambda)$ of size one. Then, assuming the elements of $FIM(D, \lambda)$ of size $n$ known, it computes a set of candidates of size $n + 1$ so that $\mathcal{I}$ is a candidate if and only if all its subsets are in $FIM(D, \lambda)$. This procedure is iterated until no more candidate is found. Let $\mathcal{D}$ be a transaction database such that $\mathcal{I}_{item}(\mathcal{D}) =$

<figure><img src="image_20.png" /><figcaption>**Figure 2.** Symmetry pruning of the search space</figcaption></figure>

$\{A, B, C\}, \sigma = (B, C)$ and $\sigma' = (A, C)(B, D)$ two symmetries of $\mathcal{D}$ and $\lambda$ a minimal support threshold. We consider that we are in an intermediary step of an Apriori like algorithm and we have $\{A\}, \{B\}, \{C\}, \{D\} \in FIM(D, \lambda)$ and $\{A, B\} \notin FIM(D, \lambda)$. Using the anti-monotonicity property (Proposition 1), we know that for all itemset $\mathcal{I}$ containing $\{A, B\}, \mathcal{I} \notin FIM(D, \lambda)$, then we obtain $\{A, B, C\}, \{A, B, D\}, \{A, B, C, D\} \notin FIM(D, \lambda)$. Moreover, using the symmetries $\sigma$ and $\sigma'$, we know that $\{A, C\} \notin FIM(D, \lambda)$ and $\{C, D\} \notin FIM(D, \lambda)$. Indeed, this is a consequence of Proposition 3, $\sigma(\{A, B\}) = \{A, C\}$ and $\sigma'(\{A, B\}) = \{C, D\}$. Finally, using the anti-monotonicity property, we deduce that also $\{A, C, D\}, \{B, C, D\} \notin FIM(D, \lambda)$. This is illustrated in Figure 2 where the inclined dashed circles (nodes) correspond to the itemsets pruned by symmetry.

## 6 Symmetry Breaking

In this section, we propose two approaches for breaking symmetries in a preprocessing step. Our proposed symmetry breaking methods eliminate items from the original transaction database. The frequent itemsets generated using the new transaction database together with the symmetry group can be used to retrieve the whole set of frequent itemsets of the original transaction database. This can be seen as a form of condensed representation of the output.
## 6.1 Orbit-based Symmetry Breaking

**Definition 11** Let $\mathcal{D}$ be a transaction database and $[a]$ an orbit following $(S(\mathcal{D}), \circ)$. $\mathcal{D}^a$ is the transaction database obtained from $\mathcal{D}$ as follows: $\forall b \in [a]$ such that $b \neq a$ and for every transaction $T = (tid, I) \in \mathcal{D}$, if $b \in I$ and $a \notin I$, then $b$ is removed from $I$ in the transaction $T$.

Let $\mathcal{D}$ be a transaction database, $a$ an item and $\lambda$ a minimal support threshold, we denote by $\mathcal{FIM}^a(\mathcal{D}, \lambda)$ all the elements of $\mathcal{FIM}(\mathcal{D}, \lambda)$ containing $a$.

**Proposition 4** Let $\mathcal{D}$ be a transaction database, $a, b \in \mathcal{I}_{items}(\mathcal{D})$ such that they are in the same orbit following the group $(S(\mathcal{D}), \circ)$ and $\lambda$ a minimal support threshold. There exists a symmetry $\sigma$ such that $\mathcal{FIM}^b(\mathcal{D}, \lambda) = \sigma(\mathcal{FIM}^a(\mathcal{D}, \lambda))$.

*Proof:* Since $a$ and $b$ are in the same orbit, there exists a symmetry $\sigma$ such that $b = \sigma(a)$. Using Proposition 3, we have (1) $\mathcal{FIM}^b(\mathcal{D}, \lambda) \supseteq \sigma(\mathcal{FIM}^a(\mathcal{D}, \lambda))$ and (2) $\mathcal{FIM}^a(\mathcal{D}, \lambda) \supseteq \sigma^{-1}(\mathcal{FIM}^b(\mathcal{D}, \lambda))$. Using (2), we have $\sigma(\mathcal{FIM}^a(\mathcal{D}, \lambda)) \supseteq \mathcal{FIM}^b(\mathcal{D}, \lambda)$. Therefore, $\mathcal{FIM}^b(\mathcal{D}, \lambda) = \sigma(\mathcal{FIM}^a(\mathcal{D}, \lambda))$ holds. $\square$

**Proposition 5** Let $\mathcal{D}$ be a transaction database, $[a]$ an orbit following $(S(\mathcal{D}), \circ)$ of size $n$ and $\lambda$ a minimal support threshold. Then, there exist $n$ symmetries $\sigma_1, \dots, \sigma_n$ such that $\mathcal{FIM}(\mathcal{D}, \lambda) = \mathcal{FIM}(\mathcal{D}^a, \lambda) \cup \sigma_1(\mathcal{FIM}(\mathcal{D}^a, \lambda)) \cup \dots \cup \sigma_n(\mathcal{FIM}(\mathcal{D}^a, \lambda))$.

*Proof:* By induction on $n$ (it is a consequence of Proposition 4). $\square$

Let $\mathcal{D}$ be a transaction database, $\mathcal{O} = \{[a_1], \dots, [a_k]\}$ the set of all the orbits following $(S(\mathcal{D}), \circ)$ and $\lambda$ a minimal support threshold. Then, the transaction database $(\dots(\mathcal{D}^{a_1})\dots)^{a_k}$ and $(S(\mathcal{D}), \circ)$ are sufficient to compute $\mathcal{FIM}(\mathcal{D}, \lambda)$. This is a direct consequence of Proposition 5.

Let us take again the transaction database given in Example 1 and the associated symmetry $\sigma$ given in section 2. Using the orbit $[\textit{Tomato}]^\sigma$, we eliminate *Parmesan* in transaction 002 as it does not contain the item *Tomato*. While using the orbit $[\textit{Mozarella}]^\sigma$, we eliminate the item *Beef* from transaction 002 as it does not contain *Mozarella*. However, using the orbit $[\textit{Chili pepper}]^\sigma$ the item *Anchovies* can not be eliminated from the transaction 003 as both items, *Chili pepper* and *Anchovies*, occur together in the same transaction.

## 6.2 Itempair-Based Symmetry Breaking

In this section, we propose another method to reduce the search space of possible interesting itemsets by detecting and breaking symmetries between itempairs.

We only consider the particular case of the symmetries with binary cycles in our description. Moreover, we fix an order $\preceq$ on $\mathcal{I}$ and we denote by $\min(I)$, with $I$ an itemset, the least item of $I$ following $\preceq$.

**Definition 12 (Ordered Symmetry)** Let $\mathcal{D}$ be a transaction database and $\sigma = (a_1, a'_1) \cdots (a_k, a'_k)$ be a symmetry of $\mathcal{D}$. $\sigma$ is an ordered symmetry iff for all $i, j \in \{1, \dots, k\}$ such that $i \le j$, $a_i \preceq a'_i$ and $a_i \le a'_j$.

In the rest of this paper, we consider all symmetries as ordered. Let $\mathcal{D}$ be a transaction database and $\sigma = (a_1, a'_1) \cdots (a_k, a'_k)$ be a symmetry of $\mathcal{D}$, the set of items $\mathcal{L}(\sigma)$ ($\mathcal{L}$ for Left) is defined by $\mathcal{L}(\sigma) = \{a_1, \dots, a_k\}$, $\mathcal{R}(\sigma)$ ($\mathcal{R}$ for Right) by $\mathcal{R}(\sigma) = \{a'_1, \dots, a'_k\}$ and $\mathcal{H}(\sigma)$ by $\mathcal{H}(\sigma) = \{\{a_i, a'_j\}|a_i \in \mathcal{L}(\sigma), a'_j \in \mathcal{R}(\sigma) \text{ and } i \le j\}$. Moreover, let $E$ be a set of itempairs, we denote by $E(\sigma)$ the following set of itempairs: $\sigma(E) = \{\{x, y\} \in E | x, y \notin \mathcal{R}(\sigma) \text{ or } \{x, y\} \in \mathcal{H}(\sigma)\}$. Intuitively, $\sigma(E)$ is obtained from $E$ by removing itempairs that can be recovered using $\sigma$.

In the following two propositions, we particularly show how some itempairs can be recovered from the others using symmetries. This will allow us to reduce transaction databases by removing items.

**Proposition 6** Let $\mathcal{D}$ be a transaction database, $\Sigma = \{\sigma_1, \dots, \sigma_n\}$ a set of symmetries of $\mathcal{D}$, $E_\Sigma = \{\{x, y\}|x, y \in \mathcal{I}_{items}(\Sigma)\}$ and $W_\Sigma = \sigma_1(\sigma_2(\cdots(\sigma_n(E_\Sigma))\cdots))$. Then, for all $\{x, y\} \in \mathcal{I}_{items}(\Sigma)$, there exist $\{x', y'\} \in W_\Sigma$ and a symmetry $\sigma$ such that $\sigma(\{x', y'\}) = \{x, y\}$.

*Proof:* One can easily prove that $W_\Sigma = \sigma_1(E_\Sigma) \cap \cdots \cap \sigma_n(E_\Sigma)$ (by induction on the value of $n$). Let $x', y' \in \mathcal{I}_{items}(\Sigma)$ such that (1) there exists a symmetry $\sigma$ where $\sigma(\{x', y'\}) = \{x, y\}$, (2) and for all symmetry $\sigma'$, there are no $x'', y'' \in \mathcal{I}_{items}(\Sigma)$ such that $x'' \prec x'$ (that means in particular $x' \prec y'$) and $\sigma'(\{x'', y''\}) = \{x, y\}$. Intuitively, $\{x', y'\}$ is the smallest itempair allowing to recover $\{x, y\}$. If $\{x', y'\} \notin W_\Sigma$, then there exists $\sigma_i \in \Sigma$ such that $x', y' \in \mathcal{R}(\sigma_i)$ or $\{x', y'\} \notin \mathcal{H}(\sigma_i)$. In both cases, there exists $\{x'', y''\} \in \sigma_i(E_\Sigma)$ such that $x'' \prec x'$ and $\sigma_i(\{x'', y''\}) = \{x', y'\}$. Thus, $\sigma(\sigma_i(\{x'', y''\})) = \sigma(\{x', y'\}) = \{x, y\}$ holds and we get a contradiction. $\square$

**Proposition 7** Let $\mathcal{D}$ be a transaction database, $\Sigma = \{\sigma_1, \dots, \sigma_n\}$ be a set of symmetries of $\mathcal{D}$, $E = \{\{x, y\}|x, y \in \mathcal{I}_{items}(\mathcal{D})\}$ and $W = \sigma_1(\sigma_2(\cdots(\sigma_n(E_\Sigma))\cdots))$. The three following properties are satisfied:

1. there exists $x \in \mathcal{I}_{items}(W)$ such that for all $y \in \mathcal{I}_{items}(\mathcal{D}) \setminus \mathcal{I}_{items}(\Sigma)$, $\{x, y\} \in W$;

2. for all $x \in \mathcal{I}_{items}(\mathcal{D})$, there exists $y \in \mathcal{I}_{items}(W)$ and a symmetry $\sigma$ such that $x = \sigma(y)$;

3. for all $\{x, y\} \in E \setminus W$, there exists $\{x', y'\} \in W$ and a symmetry $\sigma$ such that $\sigma(\{x', y'\}) = \{x, y\}$.

*Proof:* The first property is proved by taking $x = \min(\mathcal{I}_{items}(\Sigma))$. Indeed, by construction of $W$ we have $\min(\mathcal{I}_{items}(\Sigma))$ is in $\mathcal{I}_{items}(W)$ and for all $y \in \mathcal{I}_{items}(\mathcal{D}) \setminus \mathcal{I}_{items}(\Sigma)$, $\{x, y\} \in W$. The second property is proved by using the fact that the minimum of each set of the items symmetrical two by two is in $W$. Let us now prove the third property. If $x \notin \mathcal{I}_{items}(\Sigma)$ (resp. $y \notin \mathcal{I}_{items}(\Sigma)$) then by using the second property we know that there exist $y' \in W$ (resp. $x' \in W$) and a symmetry $\sigma$ such that $\sigma(\{x, y'\}) = \{x, y\}$ (resp. $\sigma(\{x', y\}) = \{x, y\}$). Otherwise, $x$ and $y$ are in $\mathcal{I}_{items}(\Sigma)$ and, by using Proposition 6, the property is satisfied. $\square$

**Definition 13** Let $\mathcal{D}$ be a transaction database, $\Sigma = \{\sigma_1, \dots, \sigma_n\}$ be a set of symmetries of $\mathcal{D}$, $E = \{\{x, y\}|x, y \in \mathcal{I}_{items}(\mathcal{D})\}$ and $W = \sigma_1(\sigma_2(\cdots(\sigma_n(E_\Sigma))\cdots))$. $\mathcal{D}[W]$ is the transaction database obtained from $\mathcal{D}$ as follows: for all $a \in \mathcal{I}_{items}(\mathcal{D})$ and for all transaction $T = (tid, I) \in \mathcal{D}$ with $|I| \ge 2$ and $a \in I$, if for all $b \in I$ we have $\{a, b\} \notin W$, then $a$ is removed from $I$ in the transaction $T$.
Let $\lambda$ be a minimal support threshold. From Proposition 3 and Proposition 7 (Property 3), we deduce that the transaction database $D[W]$ and $\Sigma$ are sufficient to compute $\mathcal{FIM}(D, \lambda)$.

Let us show an example where Itempair-Based Symmetry Breaking approach eliminates more items in the transaction database than the Orbit-based Symmetry Breaking one. Let $D$ be a transaction database and $\sigma_1 = (a, b)$, $\sigma_2 = (b, c)$ and $\sigma_3 = (c, d)$ three symmetries of $D$. It is easy to see that $a, b, c$ and $d$ are in the same orbit. Thus, using orbit-based symmetry breaking, $\mathcal{FIM}(D, \lambda)$ can be computed from the transaction database obtained from $D$ by removing $b, c$ and $d$ from all transactions that do not contain $a$. However, using the itempair-based symmetry breaking, we can remove more items from $D$. Indeed, in $D[\sigma_1(\sigma_2(\sigma_3(E)))]$, with $E = \{\{x, y\}|x, y \in \mathcal{I}_{items}(D)\}$, $c$ and $d$ are removed from all transactions, and $b$ is removed from all transactions that do not contain $a$.

# 7 Experimental evaluation

Our experimental studies are carried out on both real, public and simulated datasets widely used in the data-mining community. We provide several experiments in order to show the improvements that can be achieved using our symmetry breaking-based itemset mining approach. In particular, we provide experiments on challenging high dimensional data with thousands of items.

## 7.1 Experimentation setup

In our study, we carried out a series of three experimentations using different datasets:

1. **Simulated datasets:** In this experimentation, we use the well-known IBM itemset data generator to generate data with different features (such as dataset size, density, etc.). Note that this generator is open source and publically available<fnref n="2" />. We generated different datasets with different parameters regarding the number of transactions, average number of items per transaction, number of different items, etc. In Table 2, we provide the features of each simulated dataset.

2. **Public datasets:** The datasets used in this evaluation are from the well-known itemset FIMI repository<fnref n="3" />. However, the datasets from FIMI are mostly simulated and not high dimensional. Therefore, we used *SIDO1*, a dataset containing pharmacology real data form the *Causality challenge*<fnref n="4" />. This dataset contains massive data of 12678 transactions with 4932 items.

3. **Real datasets:** In this experimentation, we used real data regarding intrusion detection alerts. The raw data is collected from real and recent alert log files produced by Snort intrusion detection system (IDS)<fnref n="5" /> monitoring a university campus network. These alert logs represent three months activity. The alert log files are preprocessed into alert windows. Each alert window represents 1 hour of alerts in dataset *Alert1h* and 8 hours in dataset *Alert8h*. In the obtained datasets, each transaction represents the alerts triggered during an alert window.

In our experiments, we exploit Saucy<fnref n="6" />, a new implementation of the Nauty system. It is originally proposed in [1] and significantly im-

proved in [5]. The latest version of Saucy outperforms all the existing tools by many orders of magnitude, in some cases improving runtime from several days to a fraction of a second.

Because of lack of space, we only provide experiments using itempair-based symmetry breaking approach.

In the sequel, we note, $|D|$ (resp. $|I|$) the number of transactions (resp. different items) in the dataset $D$. $|Iocc|$ denotes the total number of item occurrences in $D$, while % dens represents the density of the input transaction dataset. $time(s)$ denotes the cumulated time in seconds required to search and break symmetries. $|Irem|$ represents the number of removed item occurrences from the initial dataset. #sym denotes the number of symmetries discovered in the dataset. Finally, $Iset$ and $Isset$ corresponds to the number of frequent itemsets obtained on the transaction dataset before and after breaking symmetries respectively.

## 7.2 Results on simulated datasets

Table 2 provides details on the generated datasets and the results of our symmetry breaking approach.

<table><caption>**Table 2.** Details and results on simulated datasets</caption><thead><tr><th>Dataset</th><th>|D|</th><th>|I|</th><th>|Iocc|</th><th>% dens</th><th>time(s)</th><th>|Irem|</th><th>#sym</th></tr></thead><tbody><tr><td>Dataset1</td><td>100</td><td>1006</td><td>1020</td><td>0.099%</td><td>1.29</td><td>894</td><td>899</td></tr><tr><td>Dataset2</td><td>778</td><td>3506</td><td>4089</td><td>0.011%</td><td>1.67</td><td>2774</td><td>2642</td></tr><tr><td>Dataset3</td><td>6110</td><td>13680</td><td>30886</td><td>0.014%</td><td>2.64</td><td>10577</td><td>8371</td></tr><tr><td>Dataset4</td><td>7822</td><td>17266</td><td>40506</td><td>0.023%</td><td>2.89</td><td>7520</td><td>9415</td></tr><tr><td>Dataset5</td><td>10000</td><td>26445</td><td>200102</td><td>0.075%</td><td>3.87</td><td>8330</td><td>9283</td></tr><tr><td>Dataset6</td><td>60808</td><td>27141</td><td>246817</td><td>0.073%</td><td>7.72</td><td>13396</td><td>9074</td></tr><tr><td>Dataset7</td><td>100</td><td>27151</td><td>199869</td><td>7.37%</td><td>8.5</td><td>13032</td><td>11607</td></tr></tbody></table>

Table 2 clearly shows the significant improvements (in terms of the number of removed item occurrences) that can be performed as the number of symmetries grows. For instance, in experimentation on *Dataset3* with 6110 transactions, the number of symmetries is 8371. The second point to mention is that on the generated datasets, the number of symmetries is important in datasets with low densities.

In Table 3, we provide results pointing out the correlation between the size of the preprocessed datasets (in terms of item occurrences) and the size of outputs (in terms of frequent itemsets) with the number of discovered symmetries. Note that this experiment is carried out on datasets we simulated specifically to involve interesting symmetries. To compare the output size, we use the *LCMv3* itemset mining implementation<fnref n="7" /> [16] on each dataset before and after preprocessing.

<table><caption>**Table 3.** Comparison of the number of removed item occurrences and output size in the number of discovered symmetries.</caption><thead><tr><th>#sym</th><th>|I|</th><th>|Irem|</th><th>λ</th><th>|Iset|</th><th>|Isset|</th></tr></thead><tbody><tr><td>6</td><td>900</td><td>421</td><td>5</td><td>1015830</td><td>4370</td></tr><tr><td>10</td><td>5586</td><td>3711</td><td>90</td><td>17467891</td><td>12952</td></tr><tr><td>16</td><td>37350</td><td>32482</td><td>375</td><td>2679034</td><td>467</td></tr><tr><td>22</td><td>148471</td><td>128471</td><td>900</td><td>1462982</td><td>1232</td></tr><tr><td>26</td><td>311850</td><td>289847</td><td>1450</td><td>22156</td><td>33</td></tr></tbody></table>

One can see for instance in Table 3 that as the number of symmetries in the dataset increases, the size of the preprocessed dataset is significantly reduced. In particular, in our simulated dataset, when the number of symmetries equals 26, the item occurrences is reduced from 311850 to 66272 (ensuring a reduction rate of 78%). Note also that the output size (see the number of frequent itemsets $|Iset|$ before preprocessing and the number frequent itemsets $|Isset|$ on the preprocessed dataset) is significantly reduced on all the datasets of Table 3. The output size is computed for each dataset using the same support $\lambda$.

<footnote n="2">2 IBM Quest Market-Basket Synthetic Data Generator: http://sourceforge.net/projects/ibmquestdatagen/</footnote>

<footnote n="3">3 Frequent Itemset Mining Implementations Repository: http://fimi.ua.ac.be/</footnote>

<footnote n="4">4 http://www.causality.inf.ethz.ch/challenge.php</footnote>

<footnote n="5">5 http://snort.org</footnote>

<footnote n="6">6 Saucy2: Fast symmetry discovery http://vlsicad.eecs.umich.edu/BK/SAUCY/</footnote>

<footnote n="7">7 http://research.nii.ac.jp/~uno/codes.htm</footnote>
## 7.3 Results on public datasets

In Table 4, we provide details on the used datasets and the obtained results. The results of Table 4 show that in the tested public datasets,

<table><caption>**Table 4.** Details and results on public datasets</caption><thead><tr><th>Dataset</th><th>D</th><th>I</th><th>Iocc</th><th>%dens</th><th>Irem</th><th>#sym</th></tr></thead><tbody><tr><td>Mushroom</td><td>8124</td><td>186852</td><td>198169866</td><td>13%</td><td>1208</td><td>11</td></tr><tr><td>Retail</td><td>88162</td><td>908576</td><td>4106009</td><td>0.005%</td><td>89</td><td>217</td></tr><tr><td>BMS-<br>WebView2</td><td>77512</td><td>3341</td><td>358278</td><td>0.14%</td><td>4</td><td>10</td></tr><tr><td>BMS-<br>POS</td><td>515597</td><td>1658</td><td>3367020</td><td>0.4%</td><td>3</td><td>16</td></tr><tr><td>SIDO1</td><td>9297</td><td>4926</td><td>4514145</td><td>9.85%</td><td>568</td><td>190</td></tr></tbody></table>

symmetries can be found. For instance, the *SIDO1* dataset contains 190 symmetries allowing to remove 568 item occurrences from the initial dataset. However, the number of symmetries is not as important as in some simulated datasets of Table 2. Also, the number of removed item occurrences is not significant, consequently the size of the outputs in terms of the number of frequent itemsets is not significantly reduced.

## 7.4 Results on real datasets

In Table 5, we find details on the used alert datasets and the results of our approach. In Table 5, we see that our datasets regarding real in-

<table><caption>**Table 5.** Details and results on the alert dataset</caption><thead><tr><th>Dataset</th><th>D</th><th>I</th><th>Iocc</th><th>%dens</th><th>Irem</th><th>#sym</th></tr></thead><tbody><tr><td>Alert1h</td><td>22203</td><td>167</td><td>27049</td><td>0.73%</td><td>86</td><td>23</td></tr><tr><td>Alert8h</td><td>123</td><td>167</td><td>3453</td><td>16.81%</td><td>248</td><td>19</td></tr></tbody></table>

trusion detection alerts contain some symmetries. More importantly, on the dataset *Alert8h*, the size of the output in terms of the number of frequent itemsets (with a support $\lambda=60$) is decreased by a ratio of 50%. The two datasets have different densities and the number of removed items does not depend only on the number of discovered symmetries but also on the nature of the data itself.

Let us summarize the experimental evaluation of our symmetry framework for frequent itemset mining problems. From the obtained results, we can make several interesting observations:

* Several datasets contain symmetries and are discovered by our symmetry detection method in a reasonable amount of time.

* The size of the output (number of frequent itemsets) can be significantly reduced by our symmetry-based framework.

* The reduction rate in terms of the number of eliminated item occurrences in the transaction database does not depend only on the number of found symmetries but also on their form. Indeed, some of the discovered symmetries are made of permutations of items in the same transactions, leading to no reduction using our symmetry breaking approaches. Such kind of symmetries can be better exploited in a dynamic way by Apriori-like algorithms as explained in Section 5 (symmetry pruning). This issue will be a subject of future investigations. The goal is to combine both symmetry breaking and symmetry pruning in the same framework.

## 8 Conclusion and Future Works

Symmetry is an important structural property widely exploited to reduce the search space of many combinatorial problems. In this paper, we have presented the theoretical foundation for discovering and using symmetries in the context of itemset mining problems. This study is important for several reasons. First, this kind of structures can be present in structured data and can be exploited for reducing both the search space and the size of the output. Secondly, even if such output

is reduced, the eliminated combinatorial structures can be recovered by symmetry. Symmetries can also be used to help the user for computing either non-symmetric or symmetric patterns. The symmetries discovered from a given set of data, might be valuable in analyzing data themselves. Our theoretical framework includes symmetry detection, symmetry breaking and symmetry pruning. Our experimental results, demonstrate that this kind of structure can be hidden in some classes of transaction databases. We also show that when symmetries are present, their exploitation leads to interesting reduction of the output size.

The symmetry framework proposed in this paper for the itemset mining problem opens interesting research directions in data mining in general. We plan to extend our symmetry framework to other data mining problems such as sequence, tree or graph mining. In the context of itemset mining, there remains many rooms for future improvements. The integration of symmetry pruning in Apriori-like algorithm is clearly an important issue as many datasets contain symmetries between items appearing in the same transactions.

## REFERENCES

[1] Fadi A. Aloul, Arathi Ramani, Igor L. Markov, and Karem A. Sakallah, 'Solving difficult instances of boolean satisfiability in the presence of symmetry', Transactions on Computer Aided Design, (2003).

[2] B. Benhamou and L. Sas, 'Tractability through symmetries in propositional calculus', Journal of Automated Reasoning, 12(1), 89-102, (1994).

[3] J. Crawford, 'A theoretical analysis of reasoning by symmetry in first order logic', in Workshop on Tractable Reasoning (AAAI'92), pp. 17-22, (1992).

[4] J. Crawford, M. L. Ginsberg, E. Luck, and A. Roy, 'Symmetry-breaking predicates for search problems', in Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR'96), 148-159, Morgan Kaufmann, (1996).

[5] Paul T. Darga, Karem A. Sakallah, and Igor L. Markov, 'Faster symmetry discovery using sparsity of symmetries', in Proceedings of the 45th Design Automation Conference (DAC'08), pp. 149-154, (2008).

[6] Eugene C. Freuder, 'Eliminating interchangeable values in constraint satisfaction problems', in Proceedings of the 9th National Conference on Artificial Intelligence (AAAI'91), pp. 227-233, (1991).

[7] Alain Gély, Raoul Medina, Lhouari Nourine, and Yoan Renaud, 'Uncovering and reducing hidden combinatorics in guigues-duquenne bases', in Proceedings of the third International Conference Formal Concept Analysis (ICFCA'05), pp. 235-248, (2005).

[8] Tias Guns, Siegfried Nijssen, and Luc de Raedt, 'k-pattern set mining under constraints', IEEE TKDE, 99 (PrePrints), (2011).

[9] Balakrishnan Krishnamurthy, 'Shorts proofs for tricky formulas', Acta Informatica, 22, 253-275, (1985).

[10] H. Mannila and H. Toivonen, 'Multiple uses of frequent sets and condensed representations', in KDD, pp. 189-194, (1996).

[11] B. D. McKay, 'Practical graph isomorphism', Congressus Numerantium, 30, 47-87, (1981).

[12] Raoul Medina, Caroline Noyer, and Olivier Raynaud, 'Efficient algorithms for clone items detection', in CLA'05, pp. 70-81, (2005).

[13] Shin-ichi Minato, 'Symmetric item set mining based on zero-suppressed bdds', in DS'06, pp. 321-326, (2006).

[14] Jean-Francois Puget, 'On the satisfiability of symmetrical constrained satisfaction problems', in Proceedings of the 7th International Symposium on Methodologies for Intelligent Systems (ISMIS'93), pp. 350-361, (1993).

[15] T. Imielinski R. Agrawal and A. N. Swami, 'Mining association rules between sets of items in large databases', in ACM SIGMOD International Conference on Management of Data, pp. 207-216, Baltimore, (1993). ACM Press.

[16] H. Arimura T. Uno, M. Kiyomi, 'Lcm ver.3: Collaboration of array, bitmap and prefix tree for frequent itemset mining', in OSDM Workshop on Frequent Pattern Mining Implementations, (2005).

[17] A. Tiwari, RK Gupta, and DP Agrawal, 'A survey on frequent pattern mining: Current status and challenging issues', Inform. Technol. J, 9, 1278-1293, (2010).
# Mining-Based Compression Approach of Propositional Formulae

Said Jabbour, Lakhdar Sais, Yakoub Salhi

CRIL - CNRS, University of Artois

F-62307 Lens Cedex, France

`{jabbour, sais, salhi}@cril.fr`

Takeaki Uno

National Institute of Informatics

2-1-2, Hitotsubashi, Chiyoda-ku

Tokyo 101-8430, Japan

uno@nii.jp

## ABSTRACT

In this paper, we propose a first application of data mining techniques to propositional satisfiability. Our proposed mining based compression approach aims to discover and to exploit hidden structural knowledge for reducing the size of propositional formulae in conjunctive normal form (CNF). It combines both frequent itemset mining techniques and Tseitin's encoding for a compact representation of CNF formulae. The experimental evaluation of our approach shows interesting reductions of the sizes of many application instances taken from the last SAT competitions.

## Categories and Subject Descriptors

F.4.1 [Mathematical logic and formal languages]: Mathematical Logic—Logic and constraint programming; H.2.8 [Database management]: Database applications—Data mining

## Keywords

Compression; Data mining; Propositional satisfiability and modeling

## 1. INTRODUCTION

Propositional satisfiability (SAT) i.e., the problem of checking whether a Boolean formula in conjunctive normal form (CNF) is satisfiable or not, became a core technology in many application domains, such as formal verification, planning and various new applications derived by the recent impressive progress in practical SAT solving. SAT has gained a considerable audience with the advent of a new generation of solvers able to solve SAT instances with millions of

variables and clauses [9, 4]. Today, these solvers represent an important low-level building block for many important fields, e.g., SAT modulo theory, Theorem proving, Model checking, Quantified Boolean formulas, Maximum Satisfiability, Pseudo Boolean, 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 in bioinformatics, cryptography and data mining.

Propositional formulae in CNF is the standard input format for propositional satisfiability. Indeed, most of the state-of-the-art SAT solvers are based on this normal form. Such convenient CNF representation is derived from a general Boolean formula using the well-known Tseitin encoding [14]. In practice, the general Boolean formula itself is usually derived from high level language in which problem structure is explicit.

Two important flaws were identified on the CNF form and largely discussed in the literature (e.g. [6]). First, it is often argued that by encoding arbitrary propositional formulae in CNF, structural properties of the original problem are not reflected in the CNF formula. Secondly, even if such translation is linear in the size of the original formula, a huge CNF formula might result when encoding real-world problems. Some instances exceed the capacity of the available memory, and even if the instance can be stored, the time needed for reading the input instance might be higher than its solving time. The obstacle here is not the potential difficulty of the instance, but its size. The growing success obtained in solving real-world SAT problems highlights a real transition to industrial and commercial scale. This results in a rapid growth in the size of the CNF instances encoding real-world problems. Consequently, the design of new efficient models for representing and for solving SAT instances of very large sizes ("Big" instances) is clearly an important challenge.

To address this problem, developing a more compact representation of CNF formulae is an interesting research issue. By compact encoding of formulae, we have in mind a representation model which through its use of structural knowledge results in the most compact possible formula equivalent with respect to satisfiability. By structural knowledge, we mean patterns that can be recognized or discovered. To be useful, such algorithm must be incremental.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

CIKM'13, Oct. 27-Nov. 1, 2013, San Francisco, CA, USA.

Copyright 2013 ACM 978-1-4503-2263-8/13/10$15.00.

http://dx.doi.org/10.1145/2505515.2505576
Two promising models were proposed these last years. The first, proposed by H. Dixon et al [3], uses group theory to represent several classical clauses by a single clause called an "augmented clause". The second model was proposed by M. L. Ginsberg et al [5], called QPROP ("quantified propositional logic"), which may be seen as a propositional formula extended by the introduction of quantifications over finite domains, i.e. first order logic limited to finite types and without functional symbols. The problem rises in finding efficient solving techniques of formulae encoded using such models.

More recently, an original approach for compacting sets of binary clauses was proposed by J. Rintanen in [12]. Binary clauses are ubiquitous in propositional formulae that represent real-world problems ranging from model-checking problems in computer-aided verification to AI planning problems. In [12], using auxiliary variables, it is shown how constraint graphs that contain big cliques or bi-cliques of binary clauses can be represented more compactly than the quadratic and explicit representation. The main limitation of this approach lies in its restriction to particular sets of binary clauses whose constraints graph represents cliques or bi-cliques. Such particular regularities can be caused by the presence of an at-most-one constraint over a subset of Boolean variables, forbidding more than one of them to be true at a time.

In the data mining community, several models and techniques for discovering interesting patterns in large databases has been proposed in the last few years. The problem of mining frequent itemsets is well-known and essential in data mining, knowledge discovery and data analysis. Since the first article of Agrawal [1] on association rules and itemset mining, the huge number of works, challenges, datasets and projects show the actual interest in this problem (see [13] for a recent survey).

Our goal in this work is to address the problem of finding a compact representation of CNF formulae. Our proposed mining based compression approach aims to discover hidden structures from arbitrary CNF formulae and to exploit them to reduce the overall size of the CNF formula while preserving satisfiability. It is the first application of data mining techniques to Boolean Satisfiability.

Recently, a first constraint programming (CP) based data mining framework was proposed by Luc De Raedt et al. in [11, 2]. This new framework offers a declarative and flexible representation model. It allows data mining problems to benefit from several generic and efficient CP solving techniques [8]. This first study leads to the first CP approach for itemset mining displaying nice declarative opportunities while opening interesting perspectives to cross fertilization between data-mining, constraint programming and propositional satisfiability.

In this paper, we are particularly interested in the other side of this innovative connection between these two research domains, namely how data-mining can be helpful for SAT. We present the first data-mining approach for Boolean Satisfiability. We show that itemset mining techniques are very suitable for discovering interesting patterns from CNF formulae. Such patterns are then used to rewrite the CNF formula more compactly. We also show how sets of binary clauses can be also compacted by our approach. We also prove that our approach can automatically achieve similar reductions as in [12], on bi-cliques and cliques of binary

<table><caption>Table 1: An example of transactions database $\mathcal{D}$</caption><thead><tr><td>tid</td><td>itemset</td></tr></thead><tbody><tr><td>1</td><td>Joyce, Beckett, Proust</td></tr><tr><td>2</td><td>Faulkner, Hemingway, Melville</td></tr><tr><td>3</td><td>Joyce, Proust</td></tr><tr><td>4</td><td>Hemingway, Melville</td></tr><tr><td>5</td><td>Flaubert, Zola</td></tr><tr><td>6</td><td>Hemingway, Golding</td></tr></tbody></table>

clauses. It is also important to note, that our proposed mining4SAT approach is incremental. Indeed, our method can be applied incrementally or in parallel on the subsets of any partition of the original CNF formula. This will be particularly helpful for huge CNF formula that can not be entirely stored in memory.

## 2. FREQUENT ITEMSET MINING PROBLEM

### 2.1 Preliminary Notations and Definitions

Let $\mathcal{I}$ be a set of items. A set $I \subseteq \mathcal{I}$ is called an itemset. A transaction is a couple $(tid, I)$ where $tid$ is the transaction identifier and $I$ is an itemset. A transactions database $\mathcal{D}$ is a finite set of transactions over $\mathcal{I}$ where for all two different transactions, they do not have the same transaction identifier. We say that a transaction $(tid, I)$ supports an itemset $J$ if $J \subseteq I$.

The cover of an itemset $I$ in a transactions database $\mathcal{D}$ is the set of identifiers of transactions in $\mathcal{D}$ supporting $I$: $C(I, \mathcal{D}) = \{tid | (tid, J) \in \mathcal{D} \text{ and } I \subseteq J\}$. The support of an itemset $I$ in $\mathcal{D}$ is defined by: $S(I, \mathcal{D}) = |C(I, \mathcal{D})|$. Moreover, the frequency of $I$ in $\mathcal{D}$ is defined by: $\mathcal{F}(I, \mathcal{D}) = \frac{S(I, \mathcal{D})}{|\mathcal{D}|}$.

For example, let us consider the transactions database in Table 1. Each transaction corresponds to the favorite writers of a library member. For instance, we have:

$$S(\{Hemingway, Melville\}, \mathcal{D}) = |\{2, 4\}| = 2 \text{ and} \\ \mathcal{F}(\{Hemingway, Melville\}, \mathcal{D}) = \frac{1}{3}.$$

Let $\mathcal{D}$ be a transactions database over $\mathcal{I}$ and $\lambda$ a minimal support threshold. The frequent itemset mining problem consists of computing the following set: $\mathcal{FIM}(\mathcal{D}, \lambda) = \{I \subseteq \mathcal{I} | S(I, \mathcal{D}) \geq \lambda\}$.

The problem of computing the number of frequent itemsets is $\#P$-hard [7]. The complexity class $\#P$ corresponds to the set of counting problems associated with a decision problem in $NP$. For example, counting the number of models satisfying a CNF formula is a $\#P$ problem.

### 2.2 Maximal and Closed Frequent Itemsets

Let us now recall two popular condensed representations of the set of all frequent itemsets: maximal and closed frequent itemsets.

**DEFINITION 1 (MAXIMAL FREQUENT ITEMSET).** Let $\mathcal{D}$ be a transactions database, $\lambda$ a minimal support threshold and $I \in \mathcal{FIM}(\mathcal{D}, \lambda)$. $I$ is called maximal when for all $I' \supset I, I' \notin \mathcal{FIM}(\mathcal{D}, \lambda)$ ($I'$ is not a frequent itemset).

We denote by $\mathcal{MAX}(\mathcal{D}, \lambda)$ the set of all maximal frequent itemsets in $\mathcal{D}$ with $\lambda$ as a minimal support threshold. For instance, in the previous example, we have $\mathcal{MAX}(\mathcal{D}, 2) = \{\{Joyce, Proust\}, \{Hemingway, Melville\}\}$.
**DEFINITION 2 (CLOSED FREQUENT ITEMSET).** Let $\mathcal{D}$ be a transactions database, $\lambda$ a minimal support threshold and $I \in \mathcal{FIM}(\mathcal{D}, \lambda)$. $I$ is called closed when for all $I' \supset I$, $C(I, \mathcal{D}) \neq C(I', \mathcal{D})$.

We denote by $\mathcal{CLO}(\mathcal{D}, \lambda)$ the set of all closed frequent itemsets in $\mathcal{D}$ with $\lambda$ as a minimal support threshold. For instance, we have $\mathcal{CLO}(\mathcal{D}, 2) = \{\{Hemingway\}, \{Joyce, Proust\}, \{Hemingway, Melville\}\}$. In particular, let us note that we have $C(\{Hemingway\}, \mathcal{D}) = \{2, 4, 6\}$ and $C(\{Hemingway, Melville\}, \mathcal{D}) = \{2, 4\}$. That explains why $\{Hemingway\}$ and $\{Hemingway, Melville\}$ are both closed. One can easily see that if all the closed (resp. maximal) frequent itemsets are computed, then all the frequent itemsets can be computed without using the corresponding transactions database. Indeed, the frequent itemsets correspond to all the subsets of the closed (resp. maximal) frequent itemsets.

The number of maximal (resp. closed) frequent itemsets is significantly smaller than the number of frequent itemsets. Nonetheless, this number is not always polynomial in the size of the database [16]. In particular, the problem of counting the number of maximal frequent itemsets is \#P-complete (see also [16]).

Many algorithm has been proposed for enumerating frequent closed itemsets. One can cite Apriori-like algorithm, originally proposed in [1] for mining frequent itemsets for association rules. It proceeds by a level-wise search of the elements of $\mathcal{FIM}(\mathcal{D}, \lambda)$. Indeed, it starts by computing the elements of $\mathcal{FIM}(\mathcal{D}, \lambda)$ of size one. Then, assuming the element of $\mathcal{FIM}(\mathcal{D}, \lambda)$ of size $n$ is known, it computes a set of candidates of size $n+1$ so that $I$ is a candidate if and only if all its subsets are in $\mathcal{FIM}(\mathcal{D}, \lambda)$. This procedure is iterated until no more candidates are found. Obviously, this basic procedure is enhanced using some properties such as the anti-monotonicity property that allow us to reduce the search space. Indeed, if $I \notin \mathcal{FIM}(\mathcal{D}, \lambda)$, then $I' \notin \mathcal{FIM}(\mathcal{D}, \lambda)$ for all $I' \supset I$. In our experiments, we consider one of the state-of-the-art algorithms LCM for mining frequent closed itemsets proposed by Takeaki Uno et al. in [15]. In theory, the authors prove that LCM exactly enumerates the set of frequent closed itemsets within polynomial time per closed itemset in the total input size. Let us mention that LCM algorithm obtained the best implementation award of FIMI'2004 (Frequent Itemset Mining Implementations).

### 3. FROM CNF FORMULA TO TRANSACTION DATABASE

We first introduce the satisfiability problem and some necessary notations. We consider the conjunctive normal form (CNF) representation for the propositional formulas. A CNF formula $\Phi$ is a conjunction of clauses, where a clause is a disjunction of literals. A literal is a positive ($p$) or negated ($\neg p$) propositional variable. The two literals $p$ and $\neg p$ are called complementary. A CNF formula can also be seen as a set of clauses, and a clause as a set of literals. The size of the CNF formula $\Phi$ is defined as $|\Phi| = \sum_{c \in \Phi} |c|$, where $|c|$ is equal to the number of literals in $c$. A unit clause is a clause containing only one literal (called unit literal), while a binary clause contains exactly two literals. A formula containing only binary clauses is called 2-CNF formula.

An empty clause, denoted $\perp$, is interpreted as false (unsatisfiable), whereas an empty CNF formula, denoted $\top$, is interpreted as true (satisfiable).

Let $c_1$ and $c_2$ be two clauses of a formula $\Phi$. We say that $c_1$ subsumes $c_2$ iff $c_1 \subseteq c_2$. If $c_1$ subsumes $c_2$, then the clause $c_2$ can be deleted from $\Phi$ while preserving satisfiability. A CNF formula $\Phi$ is closed under subsumption iff $\forall c \in \Phi, \neg c' \in \Phi$ such that $c \neq c'$ and $c'$ subsumes $c$. We denote by $\Phi^s$, the formula obtained from $\Phi$ by eliminating all the subsumed clauses.

We note $\bar{l}$ the complementary literal of $l$. More precisely, if $l = p$ then $\bar{l}$ is $\neg p$ and if $l = \neg p$ then $\bar{l}$ is $p$. Let us recall that any propositional formula can be translated to CNF using Tseitin's linear encoding [14]. We denote by $\mathcal{V}_{\Phi}$ the set of propositional variables appearing in $\Phi$, while the set of literals of $\Phi$ is defined as $\mathcal{L}_{\Phi}$.

An interpretation $\mathcal{B}$ of a propositional formula $\Phi$ is a function which associates a value $\mathcal{B}(p) \in \{0, 1\}$ ($0$ corresponds to false and $1$ to true) to the variables $p \in \mathcal{V}_{\Phi}$. A model of a formula $\Phi$ is an interpretation $\mathcal{B}$ that satisfies the formula: $\mathcal{B}(\Phi) = 1$. The SAT problem consists in deciding if a given CNF formula admits a model or not.

We define $\Phi|_x$ as the formula obtained from $\Phi$ by assigning $x$ the truth-value $1$. Formally $\Phi|_x = \{c \mid c \in \Phi, \{x, \neg x\} \cap c = \emptyset\} \cup \{c \setminus \{\neg x\} \mid c \in \Phi, \neg x \in c\}$. $\Phi^*$ denotes the formula $\Phi$ closed under unit propagation, defined recursively as follows: (1) $\Phi^* = \Phi$ if $\Phi$ does not contain any unit clause, (2) $\Phi^* = \perp$ if $\Phi$ contains two unit-clauses $\{x\}$ and $\{\neg x\}$, (3) otherwise, $\Phi^* = (\Phi|_x)^*$ where $x$ is the literal appearing in a unit clause of $\Phi$.

A CNF formula can be considered as a transactions database, called CNF database, where the items correspond to literals and the transactions to clauses. Note that complementary literals correspond to two different items.

**DEFINITION 3 (CNF TO D).** Let $\Phi = \bigwedge_{1 \le i \le n} c_i$ be a CNF formula. The set of items $\mathcal{I} = \mathcal{L}_{\Phi}$ and the transactions database associated to $\Phi$ is defined as $\mathcal{D}_{\Phi}^c = \{(tid_i, c_i) | 1 \le i \le n\}$

For instance, the CNF formula $(x_1 \lor \neg x_2 \lor \neg x_3) \land (x_1 \lor \neg x_2 \lor x_4) \land x_1 \land (x_3 \lor \neg x_4)$ corresponds to the following transactions database:

<table><thead><tr><td>tid</td><td>itemset</td></tr></thead><tbody><tr><td>1</td><td>x<sub>1</sub>, &not;x<sub>2</sub>, &not;x<sub>3</sub></td></tr><tr><td>2</td><td>x<sub>1</sub>, &not;x<sub>2</sub>, x<sub>4</sub></td></tr><tr><td>3</td><td>x<sub>1</sub></td></tr><tr><td>4</td><td>x<sub>3</sub>, &not;x<sub>4</sub></td></tr></tbody></table>

In this context, a frequent itemset corresponds to a frequent set of literals: the number of clauses containing these literals is greater or equal to the minimal support threshold. For instance, if we set the minimal threshold $\lambda$ to 2, we get $\{x_1, \neg x_2\}$ as a frequent itemset in the previous database. The set of maximal frequent itemsets is the smallest set of frequent set of literals where each frequent set of literals is included in at least one of its elements. For instance, the unique maximal frequent itemset in the previous example is $\{x_1, \neg x_2\}$ ($\lambda = 2$). Furthermore, the set of closed frequent itemsets is the smallest set of frequent set of literals where each frequent itemset is included in at least one of its elements having the same support. For instance, the set of the closed frequent itemsets is $\{\{x_1, \neg x_2\}, \{x_1\}\}$.
In the definition of a transaction database, we did not require that the set of items in a transaction to be unique. Indeed, two different transactions can have the same set of items and different identifiers. A CNF formula may contain the same clause more than once, but in practice this does not provide any information about satisfiability. Thus, we can consider a CNF database as just a set of itemsets (sets of literals).

# 4. MINING-BASED APPROACH FOR SIZE-REDUCTION OF CNF FORMULAE

In this section, we describe our mining based approach, called Mining4SAT, for reducing the size of CNF formulae. The key idea consists in searching for frequent sets of literals (sub-clauses) and substituting them with new variables using Tseitin's encoding [14].

## 4.1 Tseitin's Encoding

Tseitin's encoding consists in introducing fresh variables to represent sub-formulae in order to represent their truth values. For example, given a Boolean formula, containing the variables $a$ and $b$, and $v$ a fresh variable, one can add the definition $v \leftrightarrow a \lor b$ (called extension) to the formula while preserving satisfiability. Tseitin's extension principle is at the basis of the linear transformation of general Boolean formulae into CNF. Two decades later, after Tseitin's seminal paper, Plaisted and Greenbaum presented an improved CNF translation that essentially produces a subset of Tseitin's representation [10]. They noticed that by keeping track of polarities of sub-formulae, one can remove large parts of Tseitin translation. In the sequel, we use Plaisted and Greenbaum improvement. More precisely, as the disjunction $a \lor b$ is a sub-clause with positive polarity, it is sufficient to add the formula $v \rightarrow a \lor b$ i.e. a clause ($\neg v \lor a \lor b$).

Let consider the following DNF formula (Disjunctive Normal Form: a disjunction of conjunctions):

$$ (x_1 \land \dots \land x_l) \lor (y_1 \land \dots \land y_m) \lor (z_1 \land \dots \land z_n) $$

A naive way of converting such a formula to a CNF formula consists in using the distributivity of disjunction over conjunction ($A \lor (B \land C) \leftrightarrow (A \lor B) \land (A \lor C)$):

$$ (x_1 \lor y_1 \lor z_1) \land (x_1 \lor y_1 \lor z_2) \land \dots \land (x_l \lor y_m \lor z_n) $$

Such a naive approach is clearly exponential in the worst case. In Tseitin's transformation, fresh propositional variables are introduced to prevent such combinatorial explosion, mainly caused by the distributivity of disjunction over conjunction and vice versa. With additional variables, the obtained CNF formula is linear in the size of the original formula. However the equivalence is only preserved w.r.t satisfiability:

$$ (t_1 \lor t_2 \lor t_3) \land (t_1 \rightarrow (x_1 \land \dots \land x_l)) \land (t_2 \rightarrow (y_1 \land \dots \land y_m)) \land (t_3 \rightarrow (z_1 \land \dots \land z_n)) $$

## 4.2 A Size-Reduction Method

Let us now describe in more details, how itemset mining techniques can be combined with Tseitin's principle to compress CNF formula.

To illustrate the main ideas behind our mining based compression approach, we consider the CNF formula $\Phi$:

$$ (x_1 \lor \dots \lor x_n \lor \alpha_1) \land \dots \land (x_1 \lor \dots \lor x_n \lor \alpha_k) $$

where $n \ge 2$, $k > \frac{n+1}{n-1}$ and $\alpha_1, \dots, \alpha_k$ are clauses. As we can observe, the sub-clause $(x_1 \lor \dots \lor x_n)$ appears in each clause of $\Phi$. Using Tseitin's encoding, we can rewrite $\Phi$ as follows:

$$ (y \lor \alpha_1) \land \dots \land (y \lor \alpha_k) \land (x_1 \lor \dots \lor x_n \lor \neg y) $$

where $y$ is a fresh propositional variable. Indeed, $n \times k$ literals are replaced with $k+n+1$ literals leading to a gain in terms of number of literals of $(n \times k) - (n+k+1)$.

Now, if we consider the CNF database corresponding to $\Phi$, $\{x_1, \dots, x_n\}$ is a frequent itemset where the minimal support threshold is greater or equal to $k$. It is easy to see that to reduce the number of literals $n$ must be greater or equal to 2. Indeed, if $n < 2$ then there is no reduction of the number of literals, on the contrary, their number is increased. Regarding the value of $k$, one can also see that such a transformation is interesting only when $k > \frac{n+1}{n-1}$. Thus, there are three cases : if $n=2$, then $k \ge 4$, else if $n=3$ then $k \ge 3$, $k \ge 2$ otherwise. Therefore, the number of literals is always reduced when $k \ge 4$.

Obviously, a boolean interpretation is a model of the formula obtained after reduction if and only if it is a model of $\Phi$.

In the previous example, we illustrate how the problem of finding frequent itemsets can be used to reduce the size of a CNF formula. One can see that, in general, it is more interesting to consider a condensed representation of the frequent itemsets (closed and maximal) to reduce the number of literals. Indeed, by using a condensed representation, we consider all the frequent itemsets and the number of fresh propositional variables and new clauses (in our example, $y$ and $(x_1 \lor \dots \lor x_n \lor \neg y)$) introduced is smaller than that of those introduced by using all the frequent itemsets. For instance, in the previous formula, it is not interesting to introduce a fresh propositional variable for each subset of $\{x_1, \dots, x_n\}$.

**EXAMPLE 1.** Let us consider a formula $\Phi$ containing the following 8 clauses:

$$ \begin{array}{l@{\qquad}l} \begin{array}{@{}c@{\quad}c@{}} \neg & x_0 \lor x_2 \\ \neg & x_1 \lor x_4 \\ \neg & x_3 \lor x_4 \\ \neg & x_5 \lor x_6 \end{array} & \begin{array}{@{}c@{\quad}c@{}} \multicolumn{2}{@{}c@{}}{\text{----------}} \\ \multicolumn{2}{@{}c@{}}{\text{----------}} \end{array} \\ \begin{array}{@{}c@{\quad}c@{}} \neg & x_0 \lor x_1 \quad \lor \quad x_3 \\ \neg & x_1 \lor x_2 \quad \lor \quad x_3 \end{array} & \begin{array}{@{}c@{\quad}c@{}} x_4 \lor x_5 \lor x_6 & \\ x_4 \lor x_5 \lor x_6 & \end{array} \\ \begin{array}{@{}c@{\quad}c@{}} \neg & x_0 \lor x_2 \\ \neg & x_1 \lor x_4 \\ \neg & x_3 \lor x_4 \\ \neg & x_5 \lor x_6 \end{array} & \begin{array}{@{}c@{\quad}c@{}} x_4 \lor x_5 \lor x_6 & \\ x_4 \lor x_5 \lor x_6 & \end{array} \end{array} $$

Suppose that the minimal support threshold is less than 4, then the sub-clause $(x_4 \lor x_5 \lor x_6)$ is frequent. Using our approach, the formula $\Phi$ can be rewritten as:

$$ \begin{array}{l@{\qquad}l} \begin{array}{@{}c@{\quad}c@{}} \neg & x_0 \lor x_2 \\ \neg & x_1 \lor x_4 \\ \neg & x_3 \lor x_4 \\ \neg & x_5 \lor x_6 \end{array} & \begin{array}{@{}c@{\quad}c@{}} \multicolumn{2}{@{}c@{}}{\text{---}} \\ \multicolumn{2}{@{}c@{}}{\text{---}} \end{array} \\ \begin{array}{@{}c@{\quad}c@{}} \neg & x_0 \lor x_1 \quad \lor \quad x_3 \\ \neg & x_1 \lor x_2 \quad \lor \quad x_3 \end{array} & \begin{array}{@{}c@{\quad}c@{}} | & \mathbf{y} \\ | & \mathbf{y} \\ | & \mathbf{y} \\ | & \mathbf{y} \end{array} \\ \begin{array}{@{}c@{\quad}c@{}} \neg & x_0 \lor x_2 \\ \neg & x_1 \lor x_3 \end{array} & \begin{array}{@{}c@{\quad}c@{}} | & \mathbf{y} \\ | & \mathbf{y} \end{array} \\ \multicolumn{2}{@{}c@{}}{\text{---}} \\ \multicolumn{2}{@{}c@{}}{\neg \mathbf{y} \quad \lor \quad x_4 \lor x_5 \lor x_6} \end{array} $$
In this simple example, the original formula contains 27 literals, while the new formula involves only 23 literals.

## Closed vs. Maximal.

In Section 2.2, we introduced two condensed representations of the frequent itemsets: closed and maximal. The question is, which condensed representation is better? We know that the set of maximal frequent itemsets is included in that of the closed ones. Thus, a small number of fresh variables and new clauses are introduced using the maximal frequent itemsets. However, there are cases where the use of the closed frequent itemsets is more suitable. For example, let us consider the following formula:

$$ 
\begin{array}{lcl}
(x_1 \lor \dots \lor x_k \lor \dots \lor x_n \lor \alpha_1) & \land & \\
\vdots & & \\
(x_1 \lor \dots \lor x_k \lor \dots \lor x_n \lor \alpha_m) & \land & \\
(x_1 \lor \dots \lor x_k \lor \beta_1) & \land & \\
\vdots & & \\
(x_1 \lor \dots \lor x_k \lor \beta_{m'}) & \land & \\
\end{array}
$$

where $k \ge 2$, $m, m' \ge 4$ and $n > k$. We assume that the frequent itemsets are only the subsets of $\{x_1, \dots, x_n\}$. Therefore, $\{x_1, \dots, x_n\}$ is the unique maximal itemset and the closed itemsets are $\{x_1, \dots, x_n\}$ and $\{x_1, \dots, x_k\}$. Let us start by using the closed frequent itemset $\{x_1, \dots, x_n\}$ in the reduction of the number of literals:

$$ 
\begin{array}{lcl}
(y \lor \alpha_1) & \land & \\
\vdots & & \\
(y \lor \alpha_m) & \land & \\
(x_1 \lor \dots \lor x_k \lor \beta_1) & \land & \\
\vdots & & \\
(x_1 \lor \dots \lor x_k \lor \beta_{m'}) & \land & \\
(x_1 \lor \dots \lor x_n \lor \neg y) & \land & \\
\end{array}
$$

Now, by using $\{x_1, \dots, x_k\}$, we get the following formula:

$$ 
\begin{array}{lcl}
(y \lor \alpha_1) & \land & \\
\vdots & & \\
(y \lor \alpha_m) & \land & \\
(z \lor \beta_1) & \land & \\
\vdots & & \\
(z \lor \beta_{m'}) & \land & \\
(z \lor x_{k+1} \lor \dots \lor x_n \lor \neg y) & \land & \\
(x_1 \lor \dots \lor x_k \lor \neg z) & \land & \\
\end{array}
$$

In this example, it is more interesting to consider the closed frequent itemsets in our Mining4SAT approach.

In fact, a (closed) frequent itemset $I$ and one of its subsets $I'$ (which can be closed) are both interesting if $S(I') - S(I) > \frac{|I'|+1}{|I'|-1} - 1$. Indeed, if we apply our transformation using $I$, then the support of $I'$ in the resulting formula is equal to $S(I') - S(I) + 1$, and we know that $I'$ is interesting in the resulting formula if its support is greater to $\frac{|I'|+1}{|I'|-1}$.

## Overlap.

Let $\Phi$ be a set of itemsets. Two itemsets $I$ and $I'$ of $\Phi$ overlap if $I \cap I' \ne \emptyset$. Moreover, $I$ and $I'$ are in the same

overlap class if there exist $k$ itemsets $I_1, \dots, I_k$ of $\Phi$ such that $I = I_1, I_k = I'$ and for all $1 \le i \le k-1$, $I_i$ and $I_{i+1}$ overlap.

In our transformation, one can have some problems when two frequent itemsets overlap. For example, if $\{x_1, x_2, x_3\}$ and $\{x_2, x_3, x_4\}$ are two frequent itemsets (3 is the minimal support threshold) such that $S(\{x_1, x_2, x_3\}) = 3$, $S(\{x_2, x_3, x_4\}) = 3$ and $S(\{x_1, x_2, x_3, x_4\}) = 2$, then if we apply our transformation using $\{x_1, x_2, x_3\}$, then the support of $\{x_2, x_3, x_4\}$ is equal to 2 (infrequent) in the resulting formula and vice versa. Thus, we can not use both of them in the transformation.

Let us note that the overlap notion can be seen as a generalization of the subset one. Let $I$ and $I'$ be frequent itemsets such that they overlap. They are both interesting in our transformation if:

1. $S(I) - S(I \cup I') > \frac{|I|+1}{|I|-1} - 1$ or $S(I') - S(I \cup I') > \frac{|I'|+1}{|I'|-1} - 1$. This comes from the fact that if we apply the transformation using $I$ (resp. $I'$), then the support of $I'$ (resp. $I$) is equal to $S(I') - S(I \cup I') + 1$ (resp. $S(I) - S(I \cup I') + 1$).

2. $|I \setminus I'| \ge k$ (resp. $|I' \setminus I| \ge k$) where $k = 2$ if $S(I) \ge 4$ (resp. $S(I') \ge 4$), $k = 3$ if $S(I) = 3$ (resp. $S(I') = 3$), $k = 4$ otherwise. Indeed, in the previous cases, $I \setminus I'$ (resp. $I' \setminus I$) can be used in our transformation.

## Mining4SAT algorithm.

We now describe our compression algorithm, called Mining4SAT, using the set of closed frequent itemsets. Let us note that the optimal transformation using the set of all the closed frequent itemsets can be obtained by an optimal transformation using separately the overlap classes of this set. Actually, since any two distinct overlap classes do not share any literal, the reduction applied to a given formula using the elements of an overlap class does not affect the supports of the elements of the other classes. Moreover, one can easily compute the set of all the overlap classes of the set of the closed frequent itemsets: let $G = (V, E)$ be an undirected graph such that $V$ is the set of the closed frequent itemsets and $(I_1, I_2)$ is an edge of $G$ if and only if $I_1$ and $I_2$ overlap; $C$ is an overlap class if and only if it corresponds to the set of vertices of a connected component of $G$ which is not included in any other connected component of $G$. For this reason, we restrict here our attention to the reductions that can be obtained using a single overlap class. The whole size reduction process can be performed by iterating on all the overlap classes.

Let $I$ be a closed frequent itemset, we denote by $\alpha(I)$ the value $S(I) \times (|I|-1) - |I|-1$ that corresponds to the number of literals reduced by applying our transformation with $I$ on a CNF formula.

Algorithm 1 takes as input a CNF formula $\phi$ and an overlap class $C$, and returns $\phi$ after applying size-reduction transformations. It iterates until there is no element in $C$. In each iteration, it first selects one of the most interesting elements in $C$ (line 2): an element $I$ of $C$ such that there is no element $I' \in C$ satisfying $\alpha(I') > \alpha(I)$. Note that this element is not necessarily unique in $C$. This instruction means that Algorithm 1 is a greedy algorithm because it makes a locally optimal choice at each iteration. Then, it applies
**Algorithm 1 Size Reduction**

**Require:** A formula $\phi$, an overlap class of closed frequent itemsets $C$

1: while $C \neq \emptyset$ do

2: $I \leftarrow MostInterestingElement(C)$;

3: replace($\phi$, $I$, $x$);

4: Add($\phi$, $I$, $x$);

5: remove($C$, $I$);

6: replaceSubset($C$, $I$, $x$);

7: removeUninterestingElements($C$);

8: updateSupports($C$);

9: end while

10: return $\phi$

our transformation using $I = \{y_1, \dots, y_n\}$: it replaces the occurrences of $I$ with a fresh propositional variable $x$ (line 3); and it adds the clause $y_1 \lor \dots \lor y_n \lor \neg x$ to $\phi$ (line 4). It next removes $I$ from $C$ (line 5) and replaces $I$ in the other elements of $C$ with $x$ (line 6). The next instruction (line 7) consists in removing the elements of $C$ that could increase the number of literals: the elements that overlap with $I$ and are not included in $I$. As explained before, an element of $C$ overlapping with $I$ does not necessarily increase the number of literals. Thus, by removing elements from $C$ because only they overlap with $I$, our algorithm can remove closed frequent itemsets decreasing the number of literals. A partial solution to this problem consists in recomputing the closed frequent itemsets in the formula returned by Algorithm 1. The last instruction in the while loop (line 8) consists in updating the supports of the elements remaining in $C$ following the new value of $\phi$: a support of an element $I'$ remaining in $C$ changes only when it is included in $I$ and its new support is equal to $S(I') - S(I) + 1$. This instruction also removes all the elements of $C$ becoming uninteresting because of the new supports and sizes.

## 5. APPLICATION: A COMPACT REPRESENTATION OF SETS OF BINARY CLAUSES

Binary clauses (2-CNF formula) are ubiquitous in CNF formula encoding real-world problems. Some of them contain more than 90% of binary clauses. One of the main reason is that the encoding of several kinds of constraints to CNF leads to big sets of binary clauses. As an example, expressing that the variables $x_1, \dots, x_n$ must take different values in $\{v_1, \dots, v_m\}$ can leads to $n^2 \times m^2$ binary clauses (cliques of binary clauses) with a naive encoding. For $n = 100$ and $m = 10$, we get about one million of binary clauses or 10 Megabytes if each binary clause takes 10 bytes. Another example given by Rintanen in [12], concerns the encoding of planning problem to SAT and particularly of some invariants such as the one expressing that an object cannot be in two locations at the same time. For $n$ state variables there are $\frac{n \times (n-1)}{2}$ invariants that are binary clauses. In the case of a planning problem with $n = 5000$ state variables and a formula that encodes the search for plans of 100 time points, if only one of the state variables is true at any given time, the total size of the set of binary clauses is about 12 Gigabytes.

Table 2 illustrates the proportion of binary clauses on a sample of SAT instances (application category) taken from the last SAT competitions [17]. For each instance (first column), we give the total number of clauses (#cls), the number of binary clauses (#bin) and the ratio of binary clauses (($\%$)bin).

<table><caption>**Table 2: Ratio of binary clauses in some SAT instances**</caption><thead><tr><th>instance</th><th>#cls</th><th>#bin</th><th>(%) bin</th></tr></thead><tbody><tr><td>velev-pipe-o-uns-1.1-6</td><td>304026</td><td>268354</td><td>88,26%</td></tr><tr><td>9dlx_vliw_at_b.iq2</td><td>542253</td><td>500227</td><td>92,24%</td></tr><tr><td>1dlx_c.iq57_a</td><td>8562505</td><td>7567948</td><td>88,38%</td></tr><tr><td>7pipe_k</td><td>751116</td><td>722278</td><td>96,16%</td></tr><tr><td>SAT dat.k100.debugged</td><td>670701</td><td>523153</td><td>78,00%</td></tr><tr><td>BM_FV_2004_rule_batch</td><td>445444</td><td>339588</td><td>76,23%</td></tr><tr><td>sokoban-sequential-p145-*.040-*</td><td>1413816</td><td>1364160</td><td>96,48%</td></tr><tr><td>openstacks-*.p30_1.085-*</td><td>1621926</td><td>1601145</td><td>98,71%</td></tr><tr><td>aaai10-planning-ipc5-*.12-step16</td><td>1029036</td><td>991140</td><td>96,31%</td></tr><tr><td>k2fix_gr_rcs_w8.shuffled</td><td>271393</td><td>270136</td><td>99,53%</td></tr><tr><td>homer17.shuffled</td><td>1742</td><td>1716</td><td>98,50%</td></tr><tr><td>gripper13u.shuffled-as.sat03-395</td><td>38965</td><td>35984</td><td>92,34%</td></tr><tr><td>grid-strips-grid-y-3.045-*</td><td>2750755</td><td>2695230</td><td>97,98%</td></tr></tbody></table>

In our Mining4SAT general approach presented previously, binary clauses are not taken into account. Indeed, to reduce the size of a formula, we only search for itemsets of size at least two. The case where a binary clause representing a closed frequent itemset can be considered by our Mining4SAT algorithm is when it appears at least four times in a formula $\Phi$. For example, when $\Phi$ contains the following clauses $c_1 = (a \lor b)$, $c_2 = (a \lor b \lor \alpha_1)$, $c_3 = (a \lor b \lor \alpha_2)$, and $c_4 = (a \lor b \lor \alpha_3)$, where $\alpha_i$ for $1 \le i \le 3$ are clauses. In this case, the last three clauses are subsumed by the first binary clause. The clauses $c_2$, $c_3$ and $c_4$ are redundant and can be eliminated from $\Phi$. Consequently, if we suppose that a formula is closed under subsumption, this case do not happen. Let us give a more general formulation of this particular case. Let $\Phi$ be the following formula:

$$ \begin{array}{l} (x_1 \lor \dots \lor x_n) \quad \wedge \\ (x_1 \lor \dots \lor x_n \lor \alpha_1) \quad \wedge \\ \vdots \\ (x_1 \lor \dots \lor x_n \lor \alpha_k) \quad \vdots \\ \end{array} $$

where $\alpha_1, \dots, \alpha_k$ are clauses. As we can see, the first clause subsumes all the remaining clauses. Then we obtain the formula closed under subsumption $\Phi^s = (x_1 \lor \dots \lor x_n)$. Suppose that $I = \{x_1, \dots, x_n\}$ is a frequent closed itemset of $D_{\Phi}^c$. Using $I$, we obtain the following formula $\Phi'$:

$$ (y) \land (y \lor \alpha_1) \land \dots \land (y \lor \alpha_k) \land (\neg y \lor x_1 \lor \dots \lor x_n) $$

Applying unit propagation, we obtain $\Phi'^* = (x_1 \lor \dots \lor x_n)$. As we can remark $\Phi^s = \Phi'^*$. To summarize, our general Mining4SAT can derive unit literals ($y$). Then by applying unit propagation closure, some redundant clauses are eliminated automatically.

## 5.1 Compacting Arbitrary Sets of Binary Clauses

In this section, we first show how our mining based approach can be used to achieve a compact representation of arbitrary set of binary clauses. Then, we consider two interesting special cases corresponding to sets of binary clauses representing either a clique or a bi-clique. It is important to note that, in [12], the authors investigated only these particular cases.
The itemset mining process is done on the conjunctive part of $B_{\nu[\wedge]}^{1}(\Phi)$ represented in the transactions database. Setting the minimum support threshold to 4, we get as a frequent itemset $\{x_5, x_6, x_7\}$. Using 2-CNF compression algorithm described above, we can rewrite $B_{\nu(\wedge)}^{1}(\Phi)$ as $B_{\nu(\wedge)}^{2}(\Phi)$:

$$B_{\nu[\wedge]}^{2}(\Phi) = \{[x_1 \lor (x_2 \land x_3 \land y)], \\ [x_2 \lor (x_3 \land x_4 \land y)], \\ [x_3 \lor (x_4 \land y)], \\ [x_5 \lor (x_6 \land x_7)], \\ [x_6 \lor (x_7)], \\ [\neg y \lor (x_5 \land x_6 \land x_7)]\}$$

Finally a simple encoding of $B_{\nu(\wedge)}^{2}(\Phi)$ as CNF formula leads to following compressed 2-CNF formula:

$$\Phi = (x_1 \lor x_2) \land (x_1 \lor x_3) \land (x_1 \lor x_4) \land (x_2 \lor x_3) \land \\ (x_2 \lor x_4) \land (x_3 \lor x_4) \land (x_5 \lor x_6) \land (x_5 \lor x_7) \land \\ (x_6 \lor x_7) \land \\ (x_1 \lor y) \land (x_2 \lor y) \land (x_3 \lor y) \land (x_4 \lor y) \land \\ (x_5 \lor \neg y) \land (x_6 \lor \neg y) \land (x_7 \lor \neg y)$$

The substitution of the itemset $\{x_5, x_6, x_7\}$ allows us to reduce the size of the 2-CNF formula $\Phi$. Indeed, the resulting 2-CNF contains 5 binary clauses less.

## 5.2 Special Case of (Bi-)cliques of Binary Clauses

In [12], J. Rintanen addressed the problem of representing big sets of binary clauses compactly. He particularly shows that constraint graphs arising from practically interesting applications (eg. AI planning) contain big cliques or bi-cliques of binary clauses. An identified bi-clique involving the two sets of literals $\mathcal{X} = \{x_1, x_2, \dots, x_n\}$ and $\mathcal{Y} = \{y_1, y_2, \dots, y_m\}$ expresses the propositional formula $\Phi = (x_1 \land x_2 \land \dots \land x_n) \lor (y_1 \land y_2 \land \dots \land y_m)$, while a clique involving the literals $\mathcal{X} = \{x_1, x_2, \dots, x_n\}$ expresses that at-most one literal from $\mathcal{X}$ is false.

### Bi-cliques of Binary Clauses.

Let us explain how a bi-clique can be compacted with Mining4Binary method. Let $\Phi = [(x_1 \lor y_1) \land (x_1 \lor y_2) \lor \dots \lor (x_1 \lor y_m)] \dots [(x_n \lor y_1) \land (x_n \lor y_2) \lor \dots \lor (x_n \lor y_m)]$ a bi-clique of $n \times m$ binary clauses (see Figure 1). Considering the complete order relation defined by: $f(x_i) = i, f(y_j) = n + j$. Using this order relation $B_{\nu(\wedge)}(\Phi)$ corresponds exactly to $\{(x_i \lor [y_1 \land y_2 \land \dots \land y_m])|1 \le i \le n\}$. Obviously, the transactions database $D_{\Phi}^b$ contains a single closed frequent itemset $\{y_1, y_2, \dots, y_m\}$. Applying our algorithm leads to the following compact representation of $\Phi' = [\bigwedge_{1 \le i \le n} (x_i \lor z)] \land [\bigwedge_{1 \le j \le m} (\neg z \lor y_j)]$. We obtain exactly the same gain as in [12] ($O(n+m)$ binary clauses and one additional variable).

### Cliques of Binary Clauses.

Let $\Phi = \bigwedge_{1 \le i \le n-1} [(x_i \lor x_{i+1}) \land \dots \land (x_i \lor x_n)]$ be a clique of $n^2$ binary clauses (see Figure 2). The set $B_{\nu(\wedge)}(\Phi) = \{[x_i \lor (x_{i+1} \land \dots \land x_n)]|1 \le i \le n-1\}$ using the order relation defined by: $f(x_i) = i$. If we take a closer look to $D_{\Phi}^b$, the closed frequent itemset $I$ with the greatest value $\alpha(I)$ corresponds to $\{x_{n/2}, \dots, x_n\}$. In the first $\frac{n}{2}$ rows of $D_{\Phi}^b$, $I$ is substituted by a fresh variable $x$ and a new set of binary clauses $[x \lor (x_n \land \dots \land x_n)]$ is added to it, leading to two subproblems of size $\frac{n}{2} + 1$. Obviously, the same treatment is done on the set $B_{\nu(\wedge)}(\Phi)$. Consequently, the number of variables is defined by the following recurrence equation:

<figure><img src="image_21.png" /><figcaption>Figure 1: Bi-clique representation of the $n \times m$ clauses</figcaption></figure>

$$\mathcal{V}(n) = 2 \times \mathcal{V}(\frac{n}{2} + 1) + 1 \quad (1)$$

$$\mathcal{V}(6) = 1. \qquad (2)$$

The basic case is reached for $n=6$, where the last fresh variable is introduced to represent the conjunction $x_4 \land x_5 \land x_6$. For $n < 6$ no fresh variable is introduced because no frequent closed itemset can lead to a reduction of the size of the formula. Consequently, from the solution of the previous recurrence equation, we obtain that our encoding is in $O(n)$ auxiliary variables. Using the same reasoning, we also obtain the same complexity $O(n)$ for the number of binary clauses. This corresponds to the complexity obtained in [12].

<figure><img src="image_22.png" /><figcaption>Figure 2: Clique representation of $n^2$ clauses</figcaption></figure>

The two special cases of cliques and bi-cliques of binary clauses considered in this section, allow us to show that when a constraint is not well encoded, our approach can be used to correct and to derive a more efficient and compact encodings automatically.

## 6. EXPERIMENTS

In this section, we present an experimental evaluation of our proposed approaches. Two kind of experiments have been conducted. The first one deals with size reduction of arbitrary CNF formulas using Mining4SAT algorithm, while the second one attempts to reduce the size of the 2-CNF sub-formulas only, using Mining4Binary algorithm.

Both algorithms are tested on different benchmarks taken from the last SAT challenge 2012. From the 600 instances
<table><caption>Table 3: Results of Mining4SAT: a general approach</caption><thead><tr><th>Instance</th><th>orig.</th><th>comp.</th><th>% red</th></tr></thead><tbody><tr><td>1dlx_c_iq57_a</td><td>190 Mb</td><td>164 Mb</td><td>13.68 %</td></tr><tr><td>6pipe_6_ooo.*-as.sat03-413</td><td>11 Mb</td><td>7.7 Mb</td><td>30.00 %</td></tr><tr><td>9dlx_vliw_at_b_iq6.*-*04-347</td><td>76 Mb</td><td>65 Mb</td><td>14.47 %</td></tr><tr><td>abb313GPIA-9-c.*.sat04-317</td><td>21 Mb</td><td>6.9 Mb</td><td>67.14 %</td></tr><tr><td>E05F18</td><td>3.7 Mb</td><td>2.2 Mb</td><td>40.54 %</td></tr><tr><td>eq.atree.braun.11.unsat</td><td>120 Kb</td><td>72 Kb</td><td>40.00 %</td></tr><tr><td>eq.atree.braun.12.unsat</td><td>144 Kb</td><td>88 Kb</td><td>38.88 %</td></tr><tr><td>k2mul.miter.*-as.sat03-355</td><td>1.5 Mb</td><td>1.3 Mb</td><td>13.33 %</td></tr><tr><td>korf-15</td><td>1.2 Mb</td><td>752 Kb</td><td>37.33 %</td></tr><tr><td>rbcl_xits_08_UNSAT</td><td>1.1 Mb</td><td>856 Kb</td><td>22.18 %</td></tr><tr><td>SAT_dat.k45</td><td>3.5 Mb</td><td>2.6 Mb</td><td>25.71 %</td></tr><tr><td>traffic_b_unsat</td><td>18 Mb</td><td>12 Mb</td><td>33.33 %</td></tr><tr><td>x1mul.miter.*-as.sat03-359</td><td>1.1 Mb</td><td>928 Kb</td><td>15.63 %</td></tr><tr><td>9dlx_vliw_at_b_iq3</td><td>19 Mb</td><td>15 Mb</td><td>21.05 %</td></tr><tr><td>9dlx_vliw_at_b_iq4</td><td>31 Mb</td><td>26 Mb</td><td>16.12 %</td></tr><tr><td>AProVE07-09</td><td>2.8 Mb</td><td>2.7 Mb</td><td>3.57 %</td></tr><tr><td>eq.atree.braun.10.unsat</td><td>96 Kb</td><td>56 Kb</td><td>41.66 %</td></tr><tr><td>goldb-heqc-frg1mul</td><td>348 Kb</td><td>328 Kb</td><td>5.74 %</td></tr><tr><td>minand128</td><td>7.7 Mb</td><td>2.6 Mb</td><td>66.23 %</td></tr><tr><td>ndhf_xits_09_UNSAT</td><td>2.6 Mb</td><td>2.1 Mb</td><td>19.23 %</td></tr><tr><td>velev-pipe-o-uns-1.1-6</td><td>5.5 Mb</td><td>4.4 Mb</td><td>20.00 %</td></tr></tbody></table>

of the application category submitted to this challenge, we selected 100 instances while taking at least one instance from each family. All tests were made on a Xeon 3.2GHz (2 GB RAM) cluster and the timeout was set to 4 hours.

In Table 3 and Table 4, we indicate the size in Kilobytes (Kb) or Megabytes (Mb) of each SAT instance before (orig.) and after reduction (comp.). We also provide %red, the reduction percentage.

Table 3 highlights the results obtained by Mining4SAT general approach. In this experiments, and to allow possible reductions, we only search for frequent closed itemsets of size greater or equal to 4. Consequently, binary clauses are not considered. As we can observe, our Mining4SAT reduction approach allows us to reduce the size more than 20% on the majority of instances. Let us also note that the maximum (67.14 %) is reached in the case of the instance *abb313GPIA-9-c.*.sat04-317: its original size is 21 Mb and its size after reduction is 6.9 Mb.

In Table 4, we present a sample of the results obtained by Mining4Binary algorithm on compacting only binary clauses. We observe similar behavior as in the first experiment in terms of size reduction.

To study the influence of our size reduction approaches on the solving time, we also run the SAT solver MiniSAT 2.2 on both the original instance and on those obtained after reduction. As a summary, our approach achieve significant reductions in the size of instances without losing solving effectiveness.

In our experiments, we have presented the two compression algorithms, Mining4SAT (for clauses of arbitrary size) and Mining4Binary (for 2-CNF formulae). As the two algorithms can be applied independently, we have not presented the results using a two steps compression algorithm: application of the general Mining4SAT algorithm in the first step on the original formula, followed by the specialized Mining4Binary algorithm on the compressed formula derived in the first step. The results can be derived by cumulating the reductions obtained in both steps. For example, if we take the SAT instance `1dlx_c_iq57_a` presented in both Table 3 and Table 4, the reduction by the two steps algorithm is

<table><caption>Table 4: Results of Mining4Binary: a 2-CNF approach</caption><thead><tr><th>Instance</th><th>orig.</th><th>comp.</th><th>% red</th></tr></thead><tbody><tr><td>velev-pipe-o-uns-1.1-6</td><td>5.5 Mb</td><td>3.2 Mb</td><td>41.81 %</td></tr><tr><td>9dlx_vliw_at_b_iq2</td><td>11 Mb</td><td>6 Mb</td><td>44.45 %</td></tr><tr><td>1dlx_c_iq57_a</td><td>190 Mb</td><td>124 Mb</td><td>34.73 %</td></tr><tr><td>7pipe_k</td><td>14 Mb</td><td>5.4 Mb</td><td>61.42 %</td></tr><tr><td>SAT_dat.k100.debugged</td><td>16 Mb</td><td>13 Mb</td><td>18.75 %</td></tr><tr><td>IBM_FV_2004_rule_batch_2.31_L_SAT_dat.k80.debugged</td><td>9.7 Mb</td><td>7.5 Mb</td><td>22.68 %</td></tr><tr><td>sokoban-sequential-p145-*.040-*</td><td>24 Mb</td><td>14 Mb</td><td>41.66 %</td></tr><tr><td>openstacks-*p30_1.085-*</td><td>30 Mb</td><td>26 Mb</td><td>13.33 %</td></tr><tr><td>aaai10-planning-ipc5-*-12-step16</td><td>17 Mb</td><td>12 Mb</td><td>29.41 %</td></tr><tr><td>k2fix_gr_rcs_w8.shuffled</td><td>3.4 Mb</td><td>1.7 Mb</td><td>50.00 %</td></tr><tr><td>homer17.shuffled</td><td>20 Kb</td><td>16 Kb</td><td>20.00 %</td></tr><tr><td>gripper13u.shuffled-as.sat03-395</td><td>524 Kb</td><td>364 Kb</td><td>30.35 %</td></tr><tr><td>grid-strips-grid-y-3.045-*</td><td>52 Mb</td><td>42 Mb</td><td>19.23 %</td></tr></tbody></table>

computed as follows: $(190 - 164) + (190 - 124) = 92Mb$. The reduction ratio is equal to 48.42%.

## 7. AKNOWLEDGMENTS

We thank the reviewers for their helpful comments. This work has been supported in part by the French ANR project "DAG: Declarative Approaches for Enumerating Interesting Patterns" under the Défis program 2009.

## 8. CONCLUSION AND FUTURE WORKS

In this paper, we propose the first data-mining approach, called Mining4SAT, for reducing the size of Boolean formulae in conjunctive normal form (CNF). It can be seen as a preprocessing step that aims to discover hidden structural knowledge that are used to decrease the number of literals and clauses. Mining4SAT combines both frequent itemset mining techniques for discovering interesting substructures, and Tseitin-based approach for a compact representation of CNF formulae using these substructures. Thus, we show in this work, inter alia, that frequent itemset mining techniques are very suitable for discovering interesting patterns in CNF formulae.

Since we use a greedy algorithm in our approach, the formula obtained after transformation is not guaranteed to be optimal w.r.t. size. An important open question, which we will study in future works, is how to optimally use the closed frequent itemsets ranging in an overlap class. For the special case of sets of binary clauses, finding a better complete ordering leading to an optimal compression is clearly an important challenge.

Finally, our framework can be extended to constraint satisfaction problems (CSP), Pseudo Boolean etc.

## 9. REFERENCES

[1] R. Agrawal, T. Imielinski, and A. N. Swami. Mining association rules between sets of items in large databases. In *ACM SIGMOD International Conference on Management of Data*, pages 207–216, Baltimore, 1993. ACM Press.

[2] E. Coquery, S. Jabbour, L. Saïs, and Y. Salhi. A sat-based approach for discovering frequent, closed and maximal patterns in a sequence. In *Proceedings of the 20th European Conference on Artificial Intelligence (ECAI 2012)*, pages 258–263, 2012.
[3] H. E. Dixon, M. L. Ginsberg, D. K. Hofer, E. M. Luks, and A. J. Parkes. Implementing a generalized version of resolution. In *Proceedings of the Nineteenth National Conference on Artificial Intelligence (AAAI 2004)*, pages 55–60, 2004.

[4] N. Eén and N. Sörensson. An extensible sat-solver. In *Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing (SAT'03)*, pages 502–518, 2003.

[5] M. L. Ginsberg and A. J. Parkes. Search, subsearch and qprop. In *Proceedings of the Seventh International Conference on Principles of Knowledge Representation and Reasoning (KR 2000)*, 2000.

[6] É. Grégoire, R. Ostrowski, B. Mazure, and L. Saïs. Automatic extraction of functional dependencies. In *Proceedings of the Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT'04)*, pages 122–132, 2004.

[7] D. Gunopulos, R. Khardon, H. Mannila, S. Saluja, H. Toivonen, and R. S. Sharma. Discovering all most specific sentences. *ACM Trans. Database Syst.*, 28(2):140–174, June 2003.

[8] T. Guns, S. Nijssen, and L. D. Raedt. Itemset mining: A constraint programming perspective. *Artif. Intell.*, 175(12-13):1951–1983, 2011.

[9] M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient sat solver. In *DAC*, pages 530–535, 2001.

[10] D. A. Plaisted and S. Greenbaum. A structure-preserving clause form translation. *Journal of Symbolic Computation*, 2(3):293–304, 1986.

[11] L. D. Raedt, T. Guns, and S. Nijssen. Constraint programming for itemset mining. In *ACM SIGKDD*, pages 204–212, 2008.

[12] J. Rintanen. Compact representation of sets of binary constraints. In *Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006)*, pages 143–147. IOS Press, 2006.

[13] A. Tiwari, R. Gupta, and D. Agrawal. A survey on frequent pattern mining: Current status and challenging issues. *Inform. Technol. J*, 9:1278–1293, 2010.

[14] G. Tseitin. On the complexity of derivations in the propositional calculus. In H. Slesenko, editor, *Structures in Constructives Mathematics and Mathematical Logic, Part II*, pages 115–125, 1968.

[15] T. Uno, M. Kiyomi, and H. Arimura. Lcm ver. 2: Efficient mining algorithms for frequent/closed/maximal itemsets. In R. J. B. Jr., B. Goethals, and M. J. Zaki, editors, *FIMI*, volume 126 of CEUR Workshop Proceedings. CEUR-WS.org, 2004.

[16] G. Yang. The complexity of mining maximal frequent itemsets and maximal frequent patterns. In *Proceedings of the tenth ACM SIGKDD international conference on Knowledge discovery and data mining*, KDD '04, pages 344–353, New York, NY, USA, 2004.

[17] International sat competition. http://www.satcompetition.org. Organized in conjunction with the International Conference on Theory and Applications of Satisfiability Testing.
# Boolean Satisfiability for Sequence Mining

Said Jabbour
jabbour@cril.fr

Lakhdar Sais
sais@cril.fr

Yakoub Salhi
salhi@cril.fr

CRIL - CNRS, University of Artois
F-62307 Lens Cedex
France

## ABSTRACT

In this paper, we propose a SAT-based encoding for the problem of discovering frequent, closed and maximal patterns 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]: Mathematical Logic—Logic and constraint programming; H.2.8 [Database management]: Database applications—Data mining

## Keywords

Data mining; Propositional satisfiability and modeling

## 1. INTRODUCTION

Frequent sequence data mining is the problem of discovering frequent patterns shared across time among an input data-sequence. Sequence mining is a central task in computational biology, temporal sequence analysis and text mining.

In this paper, we consider the pattern discovery problem for a specific class of patterns with wildcards in a sequence. The data-sequence can be seen as a sequence of items, while the pattern can be seen as a subsequence that might contain wildcards or jokers in the sense that they match any item [18, 20, 2]. At the first sight, allowing wildcards to occur in a pattern can be seen as an even more restrictive type

of patterns in general. However as argued in [18] "studying patterns with wildcards has the merit of capturing one important aspect of biological features that often concerns isolated positions inside a motif that are not part of the biological feature being captured". The enumeration problem for maximal and closed motifs with wildcards has been investigated recently by several authors [19, 20, 2, 8]. One of the major problem is that the number of motifs can be of exponential size. This combinatorial explosion is tackled using different approaches. For example, in Parida et al. [18], the number of patterns is reduced by introducing the maximal non-redundant q-patterns (patterns occurring at least q times in a sequence). Arimura and Uno [2] proposed a polynomial space and polynomial delay algorithm MaxMotif for maximal pattern discovery of the class of motifs with wildcards.

In this work, we follow the constraint programming (CP) based data mining framework proposed recently by Luc De Raedt et al. in [10] for itemset mining. This new framework offers a declarative and flexible representation model. New constraints often require new implementations in specialized approaches, while they can be easily integrated in such a CP framework. It allows data mining problems to benefit from several generic and efficient CP solving techniques. The authors show how some typical constraints (e.g. frequency, maximality, monotonicity) used in itemset mining can be formulated for use in CP [14]. This first study leads to the first CP approach for itemset mining displaying nice declarative opportunities without neglecting efficiency. More recently, Coquery et al. [8] have proposed a SAT-Based approach for Discovering for enumerating frequent, closed and maximal patterns with wildcards in a sequence of items. In this paper, we first propose a new SAT encoding of the problem of enumerating frequent, closed and maximal patterns with wildcards in a sequence of items. Our contribution can be seen as an improvement of the approach proposed in [8]. Indeed, the experimental results clearly show that the new encoding is significantly better than the original SAT encoding proposed in [8].

Encouraged by these promising results, we propose in our second contribution a new variant of the problem of discovering patterns with wildcards in a sequence, by considering a sequence of itemsets instead of a sequence of items. In this extension the emptyset will simply play the same role as the wildcard symbol. Indeed, one can use the emptyset to match any itemset. This new problem admits some similarities and differences with the classical sequential pattern

<footnote>Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

CIKM'13, Oct. 27-Nov. 1, 2013, San Francisco, CA, USA.

Copyright 2013 ACM 978-1-4503-2263-8/13/10$15.00.

http://dx.doi.org/10.1145/2505515.2505577.</footnote>