skip to main content
10.1145/2505515.2505576acmconferencesArticle/Chapter ViewAbstractPublication PagescikmConference Proceedingsconference-collections
research-article

Mining-based compression approach of propositional formulae

Published: 27 October 2013 Publication History

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.

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 Satisc ability 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.

Cited By

View all
  • (2023)A Bloom Filter-based Algorithm for Fast Detection of Common Variables2023 International Conference on Frontiers of Robotics and Software Engineering (FRSE)10.1109/FRSE58934.2023.00015(50-56)Online publication date: Jun-2023
  • (2020)Feature selection based bee swarm meta-heuristic approach for combinatorial optimisation problems: a case-study on MaxSATMemetic Computing10.1007/s12293-020-00310-912:4(283-298)Online publication date: 22-Oct-2020
  • (2018)Accelerating Boolean Satisfiability (SAT) solving by common subclause eliminationArtificial Intelligence Review10.1007/s10462-016-9530-649:3(439-453)Online publication date: 1-Mar-2018
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
CIKM '13: Proceedings of the 22nd ACM international conference on Information & Knowledge Management
October 2013
2612 pages
ISBN:9781450322638
DOI:10.1145/2505515
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 [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 October 2013

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. compression
  2. data mining
  3. propositional satisfiability and modeling

Qualifiers

  • Research-article

Conference

CIKM'13
Sponsor:
CIKM'13: 22nd ACM International Conference on Information and Knowledge Management
October 27 - November 1, 2013
California, San Francisco, USA

Acceptance Rates

CIKM '13 Paper Acceptance Rate 143 of 848 submissions, 17%;
Overall Acceptance Rate 1,861 of 8,427 submissions, 22%

Upcoming Conference

CIKM '25

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)4
  • Downloads (Last 6 weeks)0
Reflects downloads up to 22 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2023)A Bloom Filter-based Algorithm for Fast Detection of Common Variables2023 International Conference on Frontiers of Robotics and Software Engineering (FRSE)10.1109/FRSE58934.2023.00015(50-56)Online publication date: Jun-2023
  • (2020)Feature selection based bee swarm meta-heuristic approach for combinatorial optimisation problems: a case-study on MaxSATMemetic Computing10.1007/s12293-020-00310-912:4(283-298)Online publication date: 22-Oct-2020
  • (2018)Accelerating Boolean Satisfiability (SAT) solving by common subclause eliminationArtificial Intelligence Review10.1007/s10462-016-9530-649:3(439-453)Online publication date: 1-Mar-2018
  • (2015)Mining to Compress Table ConstraintsProceedings of the 2015 IEEE 27th International Conference on Tools with Artificial Intelligence (ICTAI)10.1109/ICTAI.2015.68(405-412)Online publication date: 9-Nov-2015
  • (2014)Sliced Table Constraints: Combining Compression and Tabular ReductionIntegration of AI and OR Techniques in Constraint Programming10.1007/978-3-319-07046-9_9(120-135)Online publication date: 2014

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media