We use cookies to improve your experience with our site.

Indexed in:

SCIE, EI, Scopus, INSPEC, DBLP, CSCD, etc.

Submission System
(Author / Reviewer / Editor)
Advanced Search
Volume 38 Issue 3
May  2023
Turn off MathJax
Article Contents
Abstract
References
Related Articles
Supplements
Pan HY, Chu ZF. A semi-tensor product based all solutions Boolean satisfiability solver. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY 38(3): 702−713 May 2023. DOI: 10.1007/s11390-022-1981-4.
Citation: Pan HY, Chu ZF. A semi-tensor product based all solutions Boolean satisfiability solver. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY 38(3): 702−713 May 2023. DOI: 10.1007/s11390-022-1981-4.
shu

A Semi-Tensor Product Based All Solutions Boolean Satisfiability Solver

  • Faculty of Electrical Engineering and Computer Science, Ningbo University, Ningbo 315211, China

Funds: This work was supported in part by the National Natural Science Foundation of China under Grant No. 61871242 and in part by the State Key Laboratory of ASIC (Application Specific Integrated Circuit) & System of China under Grant No. 2021KF008.
More Information
  • Author Bio:

    Hong-Yang Pan received his B.S. degree in electrical engineering and automation from Ningbo University, Ningbo, in 2019. Now he is pursuing his M.S. degree in electronic science and technology

    Zhu-Fei Chu received his B.S. degree in electronic engineering from Shandong University, Weihai, in 2008, and his M.S. and Ph.D. degrees in communication and information system from Ningbo University, Ningbo, in 2011 and 2014, respectively. He was a postdoctoral fellow at the Ecole Polytechnique Fedederale de Lausanne (EPFL), Lausanne, from 2016 to 2017. He is currently a professor at Ningbo University, Ningbo. His current research interests include many aspects of logic synthesis and its applications. Dr. Chu serves as the Proceedings Chair from 2019 to 2021 and the Finance Chair in 2022 for the International Workshop on Logic and Synthesis (IWLS), and also a technical program committee member for IWLS, International Conference on VLSI Design (VLSID), China Semiconductor Technology International Conference (CSTIC), and China Computer Federation Integrated Circuit Design and Automation Conference (CCFDAC). He is actively maintaining the logic synthesis framework ALSO (https://github.com/nbulsi/also)

  • Corresponding author:

    chuzhufei@nbu.edu.cn

  • Received Date: October 31, 2021
  • Accepted Date: December 06, 2022
    Abstract

  • Boolean satisfiability (SAT) is widely used as a solver engine in electronic design automation (EDA). Typically, SAT is used to determine whether one or more groups of variables can be combined to form a true formula. All solutions SAT (AllSAT) is a variant of the SAT problem. In the fields of formal verification and pattern generation, AllSAT is particularly useful because it efficiently enumerates all possible solutions. In this paper, a semi-tensor product (STP) based AllSAT solver is proposed. The solver can solve instances described in both the conjunctive normal form (CNF) and circuit form. The implementation of our method differs from incremental enumeration because we do not add blocking conditions for existing solutions, but rather compute the matrices to obtain all the solutions in one pass. Additionally, the logical matrices support a variety of logic operations. Results from experiments with MCNC benchmarks using CNF-based and circuit-based forms show that our method can accelerate CPU time by 8.1x (238x maximum) and 19.9x (72x maximum), respectively.

    • FullText(HTML)
    • References (24)
  • [1]
    Cook S A. The complexity of theorem-proving procedures. In Proc. the 3rd Annual ACM Symposium on Theory of Computing, May 1971, pp.151–158. DOI: 10.1145/800157.805047.
    [2]
    Eén N, Sörensson N. An extensible SAT-solver. In Proc. the 6th International Conference on Theory and Applications of Satisfiability Testing, May 2004, pp.502–518. DOI: 10.1007/978-3-540-24605-3_37.
    [3]
    Moskewicz M W, Madigan C F, Zhao Y, Zhang L T, Malik S. Chaff: Engineering an efficient SAT solver. In Proc. the 38th Annual Design Automation Conference, Jun. 2001, pp.530–535. DOI: 10.1145/378239.379017.
    [4]
    Mishchenko A, Chatterjee S, Brayton R, Een N. Improvements to combinational equivalence checking. In Proc. the 2006 IEEE/ACM International Conference on Computer Aided Design, Nov. 2006, pp.836–843. DOI: 10.1109/ICCAD.2006.320087.
    [5]
    Froleyks N, Heule M, Iser M, Järvisalo M, Suda M. SAT competition 2020. Artificial Intelligence, 2021, 301: 103572.
    [6]
    Davis M, Logemann G, Loveland D. A machine program for theorem-proving. Communications of the ACM, 1962, 5(7): 394–397. DOI: 10.1145/368273.368557.
    [7]
    Legg A, Narodytska N, Ryzhyk L. A SAT-based counterexample guided method for unbounded synthesis. In Proc. the 28th International Conference on Computer Aided Verification, Jul. 2016, pp.364–382. DOI: 10.1007/978-3-319-41540-6_20.
    [8]
    Lowry M, Loh T H. Quantifying bicycle network connectivity. Preventive Medicine, 2017, 95 Supp.: S134–S140. DOI: 10.1016/j.ypmed.2016.12.007.
    [9]
    Han J W, Cheng H, Xin D, Yan X F. Frequent pattern mining: Current status and future directions. Data Mining and Knowledge Discovery, 2007, 15(1): 55–86. DOI: 10.1007/s10618-006-0059-1.
    [10]
    Toda T, Soh T. Implementing efficient all solutions SAT solvers. ACM Journal of Experimental Algorithmics, 2016, 21: Article No. 1.12. DOI: 10.1145/2975585.
    [11]
    Ren X Q, Guo W X, Mo Z Q, Tian W H. A divide and conquer approach to all solutions satisfiability problem. In Proc. the 4th IEEE International Conference on Computer and Communications (ICCC), Dec. 2018, pp.2590–2595. DOI: 10.1109/CompComm.2018.8780746.
    [12]
    Zhang Y L, Pu G G, Sun J. Accelerating all-SAT computation with short blocking clauses. In Proc. the 35th IEEE/ACM International Conference on Automated Software Engineering, Feb. 2020, pp.6–17. DOI: 10.1145/3324884.3416569.
    [13]
    Thiffault C, Bacchus F, Walsh T. Solving non-clausal formulas with DPLL search. In Proc. the 10th International Conference on Principles and Practice of Constraint Programming, Oct. 2004, pp.663–678. DOI: 10.1007/978-3-540-30201-8_48.
    [14]
    Marques-Silva J, Lynce I, Malik S. Conflict-driven clause learning SAT solvers. In Handbook of Satisfiability, Biere A, Heule M, van Maaren H, Walsh T (eds.), IOS Press, 2009, pp.133–182. DOI: 10.3233/978-1-58603-929-5-131.
    [15]
    Ganai M K, Ashar P, Gupta A, Zhang L T, Malik S. Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver. In Proc. the 39th Annual Design Automation Conference, Jun. 2002, pp.747–750. DOI: 10.1145/513918.514105.
    [16]
    Cheng D Z, Qi H S, Xue A C. A survey on semi-tensor product of matrices. Journal of Systems Science and Complexity, 2007, 20(2): 304–322. DOI: 10.1007/s11424-007-9027-0.
    [17]
    Bai Z W, Li Y, Zhou M L, Li D, Wang D, Połap D, Woźniak M. Bilinear semi-tensor product attention (BSTPA) model for visual question answering. In Proc. the 2020 International Joint Conference on Neural Networks (IJCNN), Jul. 2020. DOI: 10.1109/IJCNN48605.2020.9206964.
    [18]
    Fu W, Li S T. Semi-tensor compressed sensing for hyperspectral image. In Proc. the 2018 IEEE International Geoscience and Remote Sensing Symposium, Jul. 2018, pp.2737–2740. DOI: 10.1109/IGARSS.2018.8519360.
    [19]
    Han X G, Chen Z Q, Liu Z X, Zhang Q. Calculating basis siphons of Petri nets based on semi-tensor product of matrices. In Proc. the 35th Chinese Control Conference, Jul. 2016, pp.2331–2336. DOI: 10.1109/ChiCC.2016.7553712.
    [20]
    Cheng D Z, Qi H S, Zhao Y. An Introduction to Semi-Tensor Product of Matrices and Its Applications. World Scientific, 2012. DOI: 10.1142/8323.
    [21]
    Van Loan C F. The ubiquitous Kronecker product. Journal of Computational and Applied Mathematics, 2000, 123(1/2): 85–100. DOI: 10.1016/S0377-0427(00)00393-9.
    [22]
    Cheng D Z. On logic-based intelligent systems. In Proc. the 2005 International Conference on Control and Automation, Jun. 2005, pp.71–76. DOI: 10.1109/ICCA.2005.1528094.
    [23]
    Siddiqi S. An extensible circuit-based SAT solver. Journal of Experimental & Theoretical Artificial Intelligence, 2020, 32(5): 751–768. DOI: 10.1080/0952813X.2019.1672798.
    [24]
    Yang S. Logic Synthesis and Optimization Benchmarks User Guide: Version 3.0. Research Triangle Park, NC, USA: Microelectronics Center of North Carolina (MCNC), 1991.
    • Relative Articles

  • Related Articles

    [1]Zhen Liang, Wan-Wei Liu, Fu Song, Bai Xue, Wen-Jing Yang, Ji Wang, Zheng-Bin Pang. Qualitative and Quantitative Model Checking Against Recurrent Neural Networks[J]. Journal of Computer Science and Technology, 2024, 39(6): 1292-1311. DOI: 10.1007/s11390-023-2703-2
    [2]Zhen-Hua Duan, Maciej Koutny. A Framed Temporal Logic Programming Language[J]. Journal of Computer Science and Technology, 2004, 19(3).
    [3]Li Minglu, Sun Yongqiang, Sheng Huany. Nondeterministic Temporal Relations in Multimedia Data[J]. Journal of Computer Science and Technology, 1997, 12(3): 244-251.
    [4]Zhong Shaochun, Liu Dayou. Processing of Uncertainty Temporal Relations[J]. Journal of Computer Science and Technology, 1996, 11(1): 72-82.
    [5]Sun Yuan. The Modelling of Temporal Data in the Relational Database Environment[J]. Journal of Computer Science and Technology, 1995, 10(2): 163-174.
    [6]Shuai Dianxun. High-Order Two-Dimension Cluster Competitive Activation Mechanisms Used for Performing Symbolic Logic Algorithms of Problem Solving[J]. Journal of Computer Science and Technology, 1995, 10(2): 124-133.
    [7]Zhao Zhaokeng, Dai Jun, Chen Wendan. Automated Theorem Proving in Temporal Logic:T-Resolution[J]. Journal of Computer Science and Technology, 1994, 9(1): 53-62.
    [8]Lin Huimin, Gong Chun, Xie Hongliang. Abstract Implementation of Algebraic Specifications in a Temporal Logic Language[J]. Journal of Computer Science and Technology, 1991, 6(1): 11-20.
    [9]Xie Hongliang, Gong Jie, C.S.Tang. A Structured Temporal Logic Language:XYZ/SE[J]. Journal of Computer Science and Technology, 1991, 6(1): 1-10.
    [10]Li Renwei. A Natural Deduction System of Temporal Logic[J]. Journal of Computer Science and Technology, 1988, 3(3): 173-185.
    • Supplements (3)

  • Others

  • Cited by

    Periodical cited type(21)

    1. Zhen Liang, Taoran Wu, Changyuan Zhao, et al. BIRDNN: Behavior-Imitation Based Repair for Deep Neural Networks. Neural Networks, 2025, 183: 106949. DOI:10.1016/j.neunet.2024.106949
    2. Zhen Liang, Wan-Wei Liu, Fu Song, et al. Qualitative and Quantitative Model Checking Against Recurrent Neural Networks. Journal of Computer Science and Technology, 2024, 39(6): 1292. DOI:10.1007/s11390-023-2703-2
    3. Zhe Zhao, Guangke Chen, Tong Liu, et al. Attack as Detection: Using Adversarial Attack Methods to Detect Abnormal Examples. ACM Transactions on Software Engineering and Methodology, 2024, 33(3): 1. DOI:10.1145/3631977
    4. Zhen Liang, Dejin Ren, Bai Xue, et al. Verifying safety of neural networks from topological perspectives. Science of Computer Programming, 2024, 236: 103121. DOI:10.1016/j.scico.2024.103121
    5. Yedi Zhang, Zhe Zhao, Guangke Chen, et al. Precise Quantitative Analysis of Binarized Neural Networks: A BDD-based Approach. ACM Transactions on Software Engineering and Methodology, 2023, 32(3): 1. DOI:10.1145/3563212
    6. Zhen Liang, Taoran Wu, Wanwei Liu, et al. Towards robust neural networks via a global and monotonically decreasing robustness training strategy. Frontiers of Information Technology & Electronic Engineering, 2023, 24(10): 1375. DOI:10.1631/FITEE.2300059
    7. Lei Bu, Zhe Zhao, Yuchao Duan, et al. Taking Care of the Discretization Problem: A Comprehensive Study of the Discretization Problem and a Black-Box Adversarial Attack in Discrete Integer Domain. IEEE Transactions on Dependable and Secure Computing, 2022, 19(5): 3200. DOI:10.1109/TDSC.2021.3088661
    8. Fu Song, Yusi Lei, Sen Chen, et al. Advanced evasion attacks and mitigations on practical ML‐based phishing website classifiers. International Journal of Intelligent Systems, 2021, 36(9): 5210. DOI:10.1002/int.22510
    9. Yedi Zhang, Zhe Zhao, Guangke Chen, et al. QVIP: An ILP-based Formal Verification Approach for Quantized Neural Networks. Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, DOI:10.1145/3551349.3556916
    10. Zhen Liang, Dejin Ren, Wanwei Liu, et al. Theoretical Aspects of Software Engineering. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-35257-7_15
    11. Xingwu Guo, Wenjie Wan, Zhaodi Zhang, et al. Eager Falsification for Accelerating Robustness Verification of Deep Neural Networks. 2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE), DOI:10.1109/ISSRE52982.2021.00044
    12. Xiyue Zhang, Xiaohong Chen, Meng Sun. Theoretical Aspects of Computing – ICTAC 2022. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-17715-6_28
    13. Yedi Zhang, Zhe Zhao, Guangke Chen, et al. Computer Aided Verification. Lecture Notes in Computer Science, DOI:10.1007/978-3-030-81685-8_8
    14. Ye Tao, Wanwei Liu, Fu Song, et al. Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-45329-8_18
    15. Emanuele De Angelis, Guglielmo De Angelis, Maurizio Proietti. A Classification Study on Testing and Verification of AI-based Systems. 2023 IEEE International Conference On Artificial Intelligence Testing (AITest), DOI:10.1109/AITest58265.2023.00010
    16. Yantao Bai, Wanwei Liu, Xinjun Mao, et al. Modeling Neural Networks Training Process with Markov Decision Process. 2021 2nd International Conference on Artificial Intelligence and Computer Engineering (ICAICE), DOI:10.1109/ICAICE54393.2021.00102
    17. Zhe Zhao, Guangke Chen, Jingyi Wang, et al. Attack as defense: characterizing adversarial examples using robustness. Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis, DOI:10.1145/3460319.3464822
    18. Yedi Zhang, Fu Song, Jun Sun. Computer Aided Verification. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-37703-7_20
    19. XinFeng Shu, YanLin Li, WeiRan Gao. Structured Object-Oriented Formal Language and Method. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-29476-1_3
    20. Zhe Zhao, Yedi Zhang, Guangke Chen, et al. Static Analysis. Lecture Notes in Computer Science, DOI:10.1007/978-3-031-22308-2_20
    21. Zhen Liang, Changyuan Zhao, Wanwei Liu, et al. A Geometrical Characterization on Feature Density of Image Datasets. 2023 IEEE International Conference on Multimedia and Expo (ICME), DOI:10.1109/ICME55011.2023.00313

    Other cited types(0)

Catalog

    Get Citation
    PDF
    XML
    Read Online
    Article views (236) PDF downloads (23) Cited by(21)
    Related

    Copyright ©2025 JCST, All Rights Reserved     京ICP备05002829号-1

    Institute of Computing Technology, Chinese Academy of Sciences
    P.O. Box 2704, Beijing 100190, P.R. China

    Tel.: 86-10-62610746 E-mail: jcst@ict.ac.cn

    /

    DownLoad:  Full-Size Img  PowerPoint
    Return
    Return