Document Open Access Logo

Transformations of Boolean Functions

Authors Jeffrey M. Dudek , Dror Fried

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2019.39.pdf
  • Filesize: 491 kB
  • 14 pages

Document Identifiers

Author Details

Jeffrey M. Dudek
  • Department of Computer Science, Rice University, Houston, TX, USA
Dror Fried
  • Department of Mathematics and Computer Science, The Open University of Israel, Ra’anana, Israel

Funding

  • Dudek, Jeffrey M.: Supported by NSF grants DMS-1547433 and IIS-1527668, by the Big-Data Private-Cloud Research Cyberinfrastructure MRI-award funded by NSF under grant CNS-1338099, by the Ken Kennedy Institute Computer Science & Engineering Enhancement Fellowship funded by the Rice Oil & Gas HPC Conference, and by the Ken Kennedy Institute 2017/18 Cray Graduate Fellowship.

Acknowledgements

We would like to thank Kuldeep S. Meel, Moshe Y. Vardi, and Rice’s Computer-Aided Verification Group for useful discussions.

Cite As Get BibTex

Jeffrey M. Dudek and Dror Fried. Transformations of Boolean Functions. In 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 39:1-39:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSTTCS.2019.39

Abstract

Boolean functions are characterized by the unique structure of their solution space. Some properties of the solution space, such as the possible existence of a solution, are well sought after but difficult to obtain. To better reason about such properties, we define transformations as functions that change one Boolean function to another while maintaining some properties of the solution space. We explore transformations of Boolean functions, compactly described as Boolean formulas, where the property is to maintain is the number of solutions in the solution spaces. We first discuss general characteristics of such transformations. Next, we reason about the computational complexity of transforming one Boolean formula to another. Finally, we demonstrate the versatility of transformations by extensively discussing transformations of Boolean formulas to "blocks," which are solution spaces in which the set of solutions makes a prefix of the solution space under a lexicographic order of the variables.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
Keywords
  • Boolean Formulas
  • Boolean Functions
  • Transformations
  • Model Counting

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Manindra Agrawal and Thomas Thierauf. The formula isomorphism problem. SIAM Journal on Computing, 30(3):990-1009, 2000. Google Scholar
  2. S. Akshay and Kuldeep S. Meel. Scalable Approximate Model Counting via Concentrated Hashing. Under submission. Google Scholar
  3. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, New York, NY, USA, 1st edition, 2009. Google Scholar
  4. Armin Biere. Preprocessing and Inprocessing Techniques in SAT. In Proceedings of HVC, page 1, 2011. URL: https://doi.org/10.1007/978-3-642-34188-5_1.
  5. Armin Biere, Marijn Heule, and Hans van Maaren. Handbook of satisfiability, volume 185. IOS Press, 2009. Google Scholar
  6. Elmar Böhler, Edith Hemaspaandra, Steffen Reith, and Heribert Vollmer. Equivalence and isomorphism for Boolean constraint satisfaction. In International Workshop on Computer Science Logic, pages 412-426. Springer, 2002. Google Scholar
  7. Michele Boreale and Daniele Gorla. Approximate Model Counting, Sparse XOR Constraints and Minimum Distance, 2019. URL: http://arxiv.org/abs/1907.05121.
  8. Randal E Bryant. Graph-based algorithms for boolean function manipulation. Technical report, Cargnegie-Mellon University, 2001. Google Scholar
  9. Supratik Chakraborty, Dror Fried, Kuldeep S Meel, and Moshe Y Vardi. From weighted to unweighted model counting. In Proceedings of IJCAI, 2015. Google Scholar
  10. Supratik Chakraborty, Dror Fried, Lucas M. Tabajara, and Moshe Y. Vardi. Functional Synthesis via Input-Output Separation. In Proceedings of FMCAD, pages 1-9, 2018. Google Scholar
  11. Yves Crama and Peter L Hammer. Boolean functions: Theory, algorithms, and applications. Cambridge University Press, 2011. Google Scholar
  12. Carmel Domshlak and Jörg Hoffmann. Probabilistic planning via heuristic forward search and weighted model counting. J. of AI Research, 30:565-620, 2007. Google Scholar
  13. Lance Fortnow. Counting complexity. Complexity theory retrospective II, pages 81-107, 1997. Google Scholar
  14. Dror Fried, Axel Legay, Joël Ouaknine, and Moshe Y. Vardi. Sequential Relational Decomposition. In Proceedings of LICS, pages 432-441, 2018. Google Scholar
  15. Maurice Karnaugh. The map method for synthesis of combinational logic circuits. Transactions of the American Institute of Electrical Engineers, Part I: Communication and Electronics, 72(5):593-599, 1953. Google Scholar
  16. Yehuda Naveh, Michal Rimon, Itai Jaeger, Yoav Katz, Michael Vinov, Eitan Marcu, and Gil Shurek. Constraint-based random stimuli generation for hardware verification. AI Magazine, 28(3):13-13, 2007. Google Scholar
  17. Umut Oztok and Adnan Darwiche. A top-down compiler for sentential decision diagrams. In Proceedings of IJCAI, pages 3141-3148, 2015. Google Scholar
  18. B.V. Rao and M.N. Sarma. Isomorphism testing of read-once functions and polynomials. In Proceedings of FSTTCS, 2011. Google Scholar
  19. Tian Sang, Fahiem Bacchus, Paul Beame, Henry A Kautz, and Toniann Pitassi. Combining component caching and clause learning for effective model counting. In Proceedings of SAT, pages 20-28, 2004. Google Scholar
  20. Larry Stockmeyer. The complexity of approximate counting. In Proceedings of STOC, pages 118-126. ACM, 1983. Google Scholar
  21. Leslie G Valiant. The complexity of enumeration and reliability problems. SIAM J. on Computing, 8(3):410-421, 1979. Google Scholar
  22. Ingo Wegener. The complexity of Boolean functions. BG Teubner, 1987. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact