Abstract
Constrained sampling and counting are two fundamental problems arising in domains ranging from artificial intelligence and security, to hardware and software testing. Recent approaches to approximate solutions for these problems rely on employing SAT solvers and universal hash functions that are typically encoded as XOR constraints of length n/2 for an input formula with n variables. As the runtime performance of SAT solvers heavily depends on the length of XOR constraints, recent research effort has been focused on reduction of length of XOR constraints. Consequently, a notion of Independent Support was proposed, and it was shown that constructing XORs over independent support (if known) can lead to a significant reduction in the length of XOR constraints without losing the theoretical guarantees of sampling and counting algorithms. In this paper, we present the first algorithmic procedure (and a corresponding tool, called MIS) to determine minimal independent support for a given CNF formula by employing a reduction to group minimal unsatisfiable subsets (GMUS). By utilizing minimal independent supports computed by MIS, we provide new tighter bounds on the length of XOR constraints for constrained counting and sampling. Furthermore, the universal hash functions constructed from independent supports computed by MIS provide two to three orders of magnitude performance improvement in state-of-the-art constrained sampling and counting tools, while still retaining theoretical guarantees.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.References
Ignatiev, A., Previti, A., Liffiton, M., & Marques-Silva, J. (2015). Smallest mus extraction with minimal hitting set dualization. In Proceedings of CP (To Appear).
Bacchus, F., Dalmao, S., & Pitassi, T. (2003). Algorithms and complexity results for #SAT and Bayesian inference. In Proceedings of FOCS (pp. 340–351).
Belov, A., & Marques-Silva, J. (2012). Generalizing redundancy in propositional logic: Foundations and hitting sets duality. CoRR abs/1207.1257.
Belov, A., & Marques-Silva, J. (2012). Muser2: an efficient MUS extractor. JSAT, 8(3/4), 123–128.
Carter, J. L., & Wegman, M. N. (1977). Universal classes of hash functions. In Proceedings of ACM symposium on Theory of computing (pp. 106–112). ACM.
Chakraborty, S., Fremont, D.J., Meel, K. S., Seshia, S.A., & Vardi, M.Y. (2014). Distribution-aware sampling and weighted model counting for SAT. In Proceedings of AAAI (pp. 1722–1730).
Chakraborty, S., Meel, K.S., & Vardi, M.Y. (2013). A scalable and nearly uniform generator of SAT witnesses. In Proceedings of CAV (Vol. 8044 pp. 608–623).
Chakraborty, S., Meel, K.S., & Vardi, M.Y. (2013). A scalable approximate model counter. In Proceedings of CP (Vol. 8124 pp. 200–216). Springer.
Chakraborty, S., Meel, K.S., & Vardi, M.Y. (2014). Balancing scalability and uniformity in SAT witness generator. In Proceedings of DAC (pp. 1–6).
Chakraborty, S., Fremont, D.J., Meel, K.S., Seshia, S.A., & Vardi, M.Y. (2015). On parallel scalable uniform sat witness generation. In: Proceedings of TACAS (pp. 304–319).
Domshlak, C., & Hoffmann, J. (2007). Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research, 30(1), 565–620.
Ermon, S., Gomes, C., Sabharwal, A., & Selman, B. (2014). Low-density parity constraints for hashing-based discrete integration. In Proceedings of ICML (pp. 271–279).
Ermon, S., Gomes, C., Sabharwal, A., & Selman, B. (2013). Embed and project: Discrete sampling with universal hashing. In Proceedings of NIPS (pp. 2085–2093).
Ermon, S., Gomes, C.P., Sabharwal, A., & Selman, B. (2013). Taming the curse of dimensionality: Discrete integration by hashing and optimization. In Proceedings of ICML (pp. 334–342).
Fu, Z., & Malik, S. (2007). Extracting logic circuit structure from conjunctive normal form descriptions. In Professional of VLSID (pp. 37–42).
Gomes, C.P., Hoffmann, J., Sabharwal, A., & Selman, B. (2007). Short xors for model counting: from theory to practice. In Proceedings of SAT (100–106).
Grosse, I., Bernaola-Galván, P., Carpena, P., Román-Roldán, R., Oliver, J., & Stanley, H.E. (2002). Analysis of symbolic sequences using the Jensen-Shannon divergence. Physical Review E, 65(4), 041905.
Jerrum, M., & Sinclair, A. (1996). The Markov Chain Monte Carlo method: an approach to approximate counting and integration. In Approximation algorithms for NP-hard problems (pp. 482–520).
Jerrum, M., Valiant, L., & Vazirani, V. (1986). Random generation of combinatorial structures from a uniform distribution. Theoretical Computer Science, 43 (2–3), 169–188.
Kitchen, N., & Kuehlmann, A. (2007). Stimulus generation for constrained random simulation. In Proceedings of ICCAD (pp. 258–265).
Liberatore, P. (2005). Redundancy in logic I: CNF propositional formulae. Artificial Intelligence, 163(2), 203–232.
Liffiton, M.H., Mneimneh, M.N., Lynce, I., Andraus, Z.S., Marques-Silva, J., & Sakallah, K.A. (2009). A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas. Constraints, 14(4), 415–442.
Liffiton, M.H., & Sakallah, K.A. (2008). Algorithms for computing minimal unsatisfiable subsets of constraints. Journal of Automated Reasoning, 40(1), 1–33.
Maier, D. (1983). The theory of relational databases. Rockville: Computer Science Press.
Marques-Silva, J. (2012). Computing minimally unsatisfiable subformulas: State of the art and future directions. Multiple-Valued Logic and Soft Computing, 19(1–3), 163–183.
Nadel, A. (2010). Boosting minimal unsatisfiable core extraction. In Proceedings 10th international conference on formal methods in computer-aided design (pp. 221–229).
Naveh, Y., Rimon, M., Jaeger, I., Katz, Y., Vinov, M., Marcus, E., & Shurek, G. (2006). Constraint-based random stimuli generation for hardware verification. In Proceedings of IAAI (pp. 1720–1727).
Gomes, C.P., Sabharwal, A., & Selman, B. (2007). Near-uniform sampling of combinatorial spaces using XOR constraints. In Proceedings of NIPS (pp. 670–676).
Russell, S., & Norvig, P. (2009). Artificial intelligence: A modern approach (3rd Ed.). Prentice Hall.
Sang, T., Bacchus, F., Beame, P., Kautz, H., & Pitassi, T. (2004). Combining component caching and clause learning for effective model counting. In Proceedings of SAT.
Sang, T., Bearne, P., & Kautz, H. (2005). Performing bayesian inference by weighted model counting. In Professional of AAAI (pp. 475–481).
Valiant, L. (1979). The complexity of enumeration and reliability problems. SIAM Journal on Computing, 8(3), 410–421.
Xue, Y., Choi, A., & Darwiche, A. (2012). Basing decisions on sentences in decision diagrams. In Proceedings of AAAI.
Author information
Authors and Affiliations
Corresponding author
Additional information
The author list has been sorted alphabetically by last name; this should not be used to determine the extent of authors’ contributions.
Rights and permissions
About this article
Cite this article
Ivrii, A., Malik, S., Meel, K.S. et al. On computing minimal independent support and its applications to sampling and counting. Constraints 21, 41–58 (2016). https://doi.org/10.1007/s10601-015-9204-z
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10601-015-9204-z