research-article

Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling

Authors:

Kuldeep S. MeelAuthors Info & Claims

ICCAD '22: Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design

Article No.: 71, Pages 1 - 9

https://doi.org/10.1145/3508352.3549406

Published: 22 December 2022 Publication History

Abstract

Given a Boolean formula ϕ over the set of variables X and a projection set P ⊆ X, then if I ⊆ P is independent support of P, then if two solutions of ϕ agree on I, then they also agree on P. The notion of independent support is related to the classical notion of definability dating back to 1901, and have been studied over the decades. Recently, the computational problem of determining independent support for a given formula has attained importance owing to the crucial importance of independent support for hashing-based counting and sampling techniques.

In this paper, we design an efficient and scalable independent support computation technique that can handle formulas arising from real-world benchmarks. Our algorithmic framework, called Arjun¹, employs implicit and explicit definability notions, and is based on a tight integration of gate-identification techniques and assumption-based framework. We demonstrate that augmenting the state-of-the-art model counter ApproxMC4 and sampler UniGen3 with Arjun leads to significant performance improvements. In particular, ApproxMC4 augmented with Arjun counts 576 more benchmarks out of 1896 while UniGen3 augmented with Arjun samples 335 more benchmarks within the same time limit.

References

[1]

Baluta, T., Shen, S., Shinde, S., Meel, K.S., Saxena, P.: Quantitative verification of neural networks and its security applications. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security. pp. 1249--1264 (2019)

Digital Library

[2]

Balyo, T., Heule, M.J.H., Järvisalo, M.: Preface. In: Balyo, T., Heule, M.J.H., Järvisalo, M. (eds.) Proceedings of SAT Competition 2017: Solver and Benchmark Descriptions. pp. 3--3 (2017)

[3]

Beth, E.W.: On Padoa's method in the theory of definition. In: Journal of Symbolic Logic 21. pp. 194--195. No. 2 (1956)

[4]

Biere, A.: Lingeling, Plingeling and Treengeling entering the SAT Competition 2013. In: Balint, A., Belov, A., Heule, M.J.H., Järvisalo, M. (eds.) Proceedings of SAT Competition 2013: Solver and Benchmark Descriptions. pp. 51--52 (2013)

[5]

Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable and nearly uniform generator of SAT witnesses. In: Proc. of CAV. pp. 608--623 (2013)

[6]

Chakraborty, S., Meel, K.S., Vardi, M.Y.: A scalable approximate model counter. In: Proc. of CP. pp. 200--216 (2013)

[7]

Chakraborty, S., Meel, K.S., Vardi, M.Y.: Balancing scalability and uniformity in SAT witness generator. In: Proc. of DAC. pp. 1--6 (2014)

[8]

De Morgan, A.: Trigonometry and Double Algebra. Taylor, Walton, and Malbery, London (1849)

[9]

Duenas-Osorio, L., Meel, K.S., Paredes, R., Vardi, M.Y.: Counting-based reliability estimation for power-transmission grids. In: Proc. of AAAI (2017)

[10]

Eén, N., Sörensson, N.: An extensible SAT-solver. In: International conference on theory and applications of satisfiability testing. pp. 502--518. Springer (2003)

[11]

Ermon, S., Gomes, C., Sabharwal, A., Selman, B.: Low-density parity constraints for hashing-based discrete integration. In: International Conference on Machine Learning. pp. 271--279. PMLR (2014)

[12]

Gomes, C.P., Hoffmann, J., Sabharwal, A., Selman, B.: Short XORs for model counting: from theory to practice. In: International Conference on Theory and Applications of Satisfiability Testing. pp. 100--106. Springer (2007)

[13]

Iser, M.: Recognition and Exploitation of Gate Structure in SAT Solving. Ph.D. thesis, Karlsruhe Institute of Technology, Germany (2020)

[14]

Ivrii, A., Malik, S., Meel, K.S., Vardi, M.Y.: On computing minimal independent support and its applications to sampling and counting. Constraints pp. 1--18 (2015).

Digital Library

[15]

Lagniez, J.M., Lonca, E., Marquis, P.: Improving model counting by leveraging definability. In: IJCAI. pp. 751--757 (2016)

[16]

Lagniez, J.M., Lonca, E., Marquis, P.: Definability for model counting. Artificial Intelligence 281, 103229 (2020)

[17]

Liffiton, M.H., Sakallah, K.A.: Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning 40(1), 1--33 (2008)

Digital Library

[18]

Malik, S., Zhao, Y., Madigan, C.F., Zhang, L., Moskewicz, M.W.: Chaff: Engineering an efficient SAT solver. Design Automation Conference pp. 530--535 (2001).

[19]

Meel, K.S., Akshay, S.: Sparse hashing for scalable approximate model counting: theory and practice. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 728--741 (2020)

Digital Library

[20]

Meel, K.S., Soos, M.: Model counting and uniform sampling instances. (May 2020). https://doi.org/10.5281/zenodo.3793090

[21]

Naveh, Y., Emek, R.: Random Stimuli Generation for Functional Hardware Verification as a CP Application. In: Proc. of CP. Lecture Notes in Computer Science, vol. 3709, pp. 882--882. Springer (2005)

[22]

Ostrowski, R., Grégoire, É., Mazure, B., Sais, L.: Recovering and exploiting structural knowledge from CNF formulas. In: Proc. of CP. Lecture Notes in Computer Science, vol. 2470, pp. 185--199. Springer (2002)

[23]

Padoa, A.: Essai d'une théorie algébrique des nombres entiers, précédé d'une introduction logique à une theorie déductive quelconque. In: Bibliothèque du Congrès international de philosophie. vol. 3, pp. 309--365 (1901)

[24]

Pipatsrisawat, K., Darwiche, A.: A lightweight component caching scheme for satisfiability solvers. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. pp. 294--299. Springer (2007)

Digital Library

[25]

Sashittal, P., El-Kebir, M.: Sharptni: counting and sampling parsimonious transmission networks under a weak bottleneck. bioRxiv p. 842237 (2019)

[26]

Sharma, S., Roy, S., Soos, M., Meel, K.S.: Ganak: A scalable probabilistic exact model counter. In: IJCAI. vol. 19, pp. 1169--1176 (2019)

[27]

Slivovsky, F.: Interpolation-based semantic gate extraction and its applications to QBF preprocessing. In: International Conference on Computer Aided Verification. pp. 508--528. Springer (2020)

Digital Library

[28]

Soos, M., Gocht, S., Meel, K.S.: Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: International Conference on Computer Aided Verification. pp. 463--484. Springer (2020)

Digital Library

[29]

Soos, M., Meel, K.S.: Bird: Engineering an efficient CNF-XOR sat solver and its applications to approximate model counting. In: Proc. of the AAAI (2019)

[30]

Valiant, L.G.: The complexity of enumeration and reliability problems. SIAM Journal on Computing 8(3), 410--421 (1979)

Digital Library

Cited By

Tan YYang JSoos MMyreen MMeel K(2024)Formally Certified Approximate Model CountingComputer Aided Verification10.1007/978-3-031-65627-9_8(153-177)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_8
Althaus ESchnurbusch D(2024)Reducing Treewidth for SAT-Related Problems Using Simple LiftingsCombinatorial Optimization10.1007/978-3-031-60924-4_14(175-191)Online publication date: 22-May-2024
https://dl.acm.org/doi/10.1007/978-3-031-60924-4_14
Akshay SBasa EChakraborty SFried D(2024)On Dependent Variables in Reactive SynthesisTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_8(123-143)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57246-3_8
Show More Cited By

Index Terms

Arjun: An Efficient Independent Support Computation Technique and its Applications to Counting and Sampling

Index terms have been assigned to the content through auto-classification.

Recommendations

Sibuya copulas

A new class of copulas referred to as ''Sibuya copulas'' is introduced and its properties are investigated. Members of this class are of a functional form which was first investigated in the work of M. Sibuya. The construction of Sibuya copulas is based ...
Tail dependence functions and vine copulas

Tail dependence and conditional tail dependence functions describe, respectively, the tail probabilities and conditional tail probabilities of a copula at various relative scales. The properties as well as the interplay of these two functions are ...
Construction and sampling of Archimedean and nested Archimedean Lévy copulas

The class of Archimedean Lévy copulas is considered with focus on the construction and sampling of the corresponding Lévy processes. Furthermore, the class of nested Archimedean Lévy copulas is introduced. This class allows one to model hierarchical ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ICCAD '22: Proceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design

October 2022

1467 pages

ISBN:9781450392174

DOI:10.1145/3508352

Conference Chair:
Tulika Mitra
National University of Singapore
,
Program Chairs:
Evangeline Young
The Chinese University of Hong Kong
,
Jinjun Xiong
University at Buffalo (UB)

Copyright © 2022 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Sponsors

SIGDA: ACM Special Interest Group on Design Automation

In-Cooperation

IEEE-EDS: Electronic Devices Society
IEEE CAS
IEEE CEDA

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 22 December 2022

Check for updates

Qualifiers

Research-article

Funding Sources

Conference

ICCAD '22

Sponsor:

SIGDA

ICCAD '22: IEEE/ACM International Conference on Computer-Aided Design

October 30 - November 3, 2022

California, San Diego

Acceptance Rates

Overall Acceptance Rate 457 of 1,762 submissions, 26%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
86
Total Downloads

Downloads (Last 12 months)35
Downloads (Last 6 weeks)2

Reflects downloads up to 29 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Tan YYang JSoos MMyreen MMeel K(2024)Formally Certified Approximate Model CountingComputer Aided Verification10.1007/978-3-031-65627-9_8(153-177)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65627-9_8
Althaus ESchnurbusch D(2024)Reducing Treewidth for SAT-Related Problems Using Simple LiftingsCombinatorial Optimization10.1007/978-3-031-60924-4_14(175-191)Online publication date: 22-May-2024
https://dl.acm.org/doi/10.1007/978-3-031-60924-4_14
Akshay SBasa EChakraborty SFried D(2024)On Dependent Variables in Reactive SynthesisTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-57246-3_8(123-143)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57246-3_8
Latour ASen AMeel KElkind E(2023)Solving the identifying code set problem with grouped independent supportProceedings of the Thirty-Second International Joint Conference on Artificial Intelligence10.24963/ijcai.2023/219(1971-1978)Online publication date: 19-Aug-2023
https://dl.acm.org/doi/10.24963/ijcai.2023/219
Lagniez JMarquis P(2023)Boosting Definability Bipartition Computation Using SAT WitnessesLogics in Artificial Intelligence10.1007/978-3-031-43619-2_47(697-711)Online publication date: 20-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-43619-2_47
Yang JMeel K(2023)Rounding Meets Approximate Model CountingComputer Aided Verification10.1007/978-3-031-37703-7_7(132-162)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37703-7_7
Yang JChakraborty SMeel K(2022)Projected Model Counting: Beyond Independent SupportAutomated Technology for Verification and Analysis10.1007/978-3-031-19992-9_11(171-187)Online publication date: 25-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19992-9_11

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten