Skip to main content
SpringerLink
Log in

A Moderately Exponential Time Algorithm for k-IBDD Satisfiability

  • Published:
Algorithmica Aims and scope Submit manuscript

Abstract

We present a satisfiability algorithm for k-indexed binary decision diagrams (k-IBDDs). The proposed exponential space and deterministic algorithm solves the satisfiability of k-IBDDs, i.e., k-IBDD SAT, for instances with n variables and cn nodes in \(O\left( 2^{(1-\mu _k(c))n}\right) \) time, where \(\mu _k(c) = \varOmega \left( \frac{1}{(k^2 2^k\log {c})^{2^{k-1}-1}}\right) \). We also provide a polynomial space and deterministic algorithm that solves a k-IBDD SAT of polynomial size for any constant \(k \ge 2\) in \(O\left( 2^{ n - n^{ 1/2^{k-1} }}\right) \) time. In addition, the proposed algorithm is applicable to equivalence checking of two IBDDs.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

References

  1. Arvind, V., Schuler, R.: The quantum query complexity of 0–1 knapsack and associated claw problems. In: Proceedings of the 14th International Symposium on Algorithms and Computation (ISAAC), pp. 168–177 (2003)

  2. Barrington, D.A.M.: Bounded-width polynomial-size branching programs recognize exactly those languages in nc\({^1}\). J. Comput. Syst. Sci. 38(1), 150–164 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bergroth, L., Hakonen, H., Raita, T.: A survey of longest common subsequence algorithms. In: SPIRE, pp. 39–48 (2000)

  4. Bollig, B., Sauerhoff, M., Sieling, D., Wegener, I.: On the power of different types of restricted branching programs. In: Electronic Colloquium on Computational Complexity (ECCC), TR94-026 (1994)

  5. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677–691 (1986)

    Article  MATH  Google Scholar 

  6. Calabro, C., Impagliazzo, R., Paturi, R.: A duality between clause width and clause density for SAT. In: Proceedings of the 21st Annual IEEE Conference on Computational Complexity (CCC), pp. 252–260 (2006)

  7. Chen, R., Kabanets, V., Kolokolova, A., Shaltiel, R., Zuckerman, D.: Mining circuit lower bound proofs for meta-algorithms. Electronic Colloquium on Computational Complexity (ECCC) TR13-057 (2013). Also In: Proceedings of the 29th Conference on Computational Complexity (CCC), pp. 262–273, (2014)

  8. Dantsin, E., Hirsch, E.A., Wolpert, A.: Algorithms for SAT based on search in hamming balls. In: Proceedings of the 21st Annual Symposium on Theoretical Aspects of Computer Science (STACS), pp. 141–151 (2004)

  9. Dantsin, E., Hirsch, E.A., Wolpert, A.: Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms. In: Proceedings of the 6th International Conference on Algorithms and Complexity (CIAC), pp. 60–68 (2006)

  10. Erdös, P., Szakeres, G.: A combinatorial problem in geometry. Compos. Math. 2, 463–470 (1935)

    MathSciNet  Google Scholar 

  11. Hirsch, E.A.: Exact algorithms for general CNF SAT. In: Kao, M.Y. (ed.) Encyclopedia of Algorithms, pp. 286–289. Springer, New York (2008)

    Chapter  Google Scholar 

  12. Impagliazzo, R., Matthews, W., Paturi, R.: A satisfiability algorithm for AC\(^0\). In: Proceedings of the 23rd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pp. 961–972 (2012)

  13. Impagliazzo, R., Paturi, R., Schneider, S.: A satisfiability algorithm for sparse depth two threshold circuits. In: Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp. 479–488 (2013)

  14. Jain, J., Bitner, J.R., Abadir, M.S., Abraham, J.A., Fussell, D.S.: Indexed BDDs: algorithmic advances in techniques to represent and verify boolean functions. IEEE Trans. Comput. 46(11), 1230–1245 (1997)

    Article  MathSciNet  Google Scholar 

  15. Santhanam, R.: Fighting perebor: New and improved algorithms for formula and QBF satisfiability. In: Proceedings of the 51th Annual IEEE Symposium on Foundations of Computer Science (FOCS), pp. 183–192 (2010)

  16. Schuler, R.: An algorithm for the satisfiability problem of formulas in conjunctive normal form. J. Algorithms 54(1), 40–44 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  17. Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM, Philadelphia (2000)

    Book  MATH  Google Scholar 

  18. Williams, R.: Improving exhaustive search implies superpolynomial lower bounds. SIAM J. Comput. 42(3), 1218–1244 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  19. Williams, R.: Nonuniform ACC circuit lower bounds. J. ACM 61(1), 2:1–2:32 (2014)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

This work was supported by MEXT KAKENHI JP24106003, JSPS KAKENHI JP26730007, JST, ERATO, Kawarabayashi Large Graph Project.

Author information

Authors and Affiliations

  1. The University of Electro-Communications, Chofu, Japan

    Atsuki Nagao

  2. Seikei University, Musashino, Japan

    Kazuhisa Seto

  3. National Institute of Informatics, Tokyo, Japan

    Junichi Teruyama

  4. JST, ERATO, Kawarabayashi Large Graph Project, Tokyo, Japan

    Junichi Teruyama

Authors
  1. Atsuki Nagao
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Kazuhisa Seto
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Junichi Teruyama
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Atsuki Nagao.

Additional information

A preliminary version of this paper appeared in the Proceedings of the 14th Workshop on Algorithms and Data Structures (WADS 2015).

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Nagao, A., Seto, K. & Teruyama, J. A Moderately Exponential Time Algorithm for k-IBDD Satisfiability. Algorithmica 80, 2725–2741 (2018). https://doi.org/10.1007/s00453-017-0332-2

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00453-017-0332-2

Keywords

Search

Navigation