Symmetric Component Caching for Model Counting on Combinatorial Instances

Authors

  • Timothy van Bremen KU Leuven
  • Vincent Derkinderen KU Leuven
  • Shubham Sharma Nutanix Software India Pvt. Ltd.
  • Subhajit Roy Indian Institute of Technology Kanpur
  • Kuldeep S. Meel National University of Singapore

Keywords:

Satisfiability, Solvers and Tools

Abstract

Given a propositional formula ψ, the model counting problem, also referred to as #SAT, seeks to compute the number of satisfying assignments (or models) of ψ. Modern search-based model counting algorithms are built on conflict-driven clause learning, combined with the caching of certain subformulas (called components) encountered during the search process. Despite significant progress in these algorithms over the years, state-of-the-art model counters often struggle to handle large but structured instances that typically arise in combinatorial settings. Motivated by the observation that these counters do not exploit the inherent symmetries exhibited in such instances, we revisit the component caching architecture employed in current counters and introduce a novel caching scheme that focuses on identifying symmetric components. We first prove the soundness of our approach, and then integrate it into the state-of-the-art model counter GANAK. Our extensive experiments on hard combinatorial instances demonstrate that the resulting counter, SymGANAK, leads to improvements over GANAK both in terms of PAR-2 score and the number of instances solved.

Downloads

Published

2021-05-18

How to Cite

van Bremen, T., Derkinderen, V., Sharma, S., Roy, S., & Meel, K. S. (2021). Symmetric Component Caching for Model Counting on Combinatorial Instances. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5), 3922-3930. Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/16511

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization