Document

# Transformations of Boolean Functions

## File

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

## Acknowledgements

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

## Cite As

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

## References

1. Manindra Agrawal and Thomas Thierauf. The formula isomorphism problem. SIAM Journal on Computing, 30(3):990-1009, 2000.
2. S. Akshay and Kuldeep S. Meel. Scalable Approximate Model Counting via Concentrated Hashing. Under submission.
3. Sanjeev Arora and Boaz Barak. Computational Complexity: A Modern Approach. Cambridge University Press, New York, NY, USA, 1st edition, 2009.
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.
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.
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.
9. Supratik Chakraborty, Dror Fried, Kuldeep S Meel, and Moshe Y Vardi. From weighted to unweighted model counting. In Proceedings of IJCAI, 2015.
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.
11. Yves Crama and Peter L Hammer. Boolean functions: Theory, algorithms, and applications. Cambridge University Press, 2011.
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.
13. Lance Fortnow. Counting complexity. Complexity theory retrospective II, pages 81-107, 1997.
14. Dror Fried, Axel Legay, Joël Ouaknine, and Moshe Y. Vardi. Sequential Relational Decomposition. In Proceedings of LICS, pages 432-441, 2018.
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.
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.
17. Umut Oztok and Adnan Darwiche. A top-down compiler for sentential decision diagrams. In Proceedings of IJCAI, pages 3141-3148, 2015.
18. B.V. Rao and M.N. Sarma. Isomorphism testing of read-once functions and polynomials. In Proceedings of FSTTCS, 2011.
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.
20. Larry Stockmeyer. The complexity of approximate counting. In Proceedings of STOC, pages 118-126. ACM, 1983.
21. Leslie G Valiant. The complexity of enumeration and reliability problems. SIAM J. on Computing, 8(3):410-421, 1979.
22. Ingo Wegener. The complexity of Boolean functions. BG Teubner, 1987.
X

Feedback for Dagstuhl Publishing