Journal of Computer Science and Technology


A Semi-Tensor Product Based All Solutions Boolean Satisfiability Solver

Hong-Yang Pan(潘鸿洋), Student Member, CCF and Zhu-Fei Chu*(储著飞), Senior Member, CCF, Member, IEEE   

  1. Faculty of Electrical Engineering and Computer Science, Ningbo University, Ningbo 315211, China
  • Received:2021-11-01 Revised:2022-10-23 Accepted:2022-12-07
  • Contact: Zhu-Fei Chu
  • About author: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 an associate professor at Ningbo University, Ningbo. His current research interests include the 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 (

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 both in 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.


我们的研究目标是,设计一种基于半张量积的数理计算SAT求解器。约束问题的求解可以将SAT问题分为两种情况,SAT及其变种,即全解SAT (AllSAT)。SAT是基于启发式算法的求解,能在最快的时间内得到一个满足约束的解;相比AllSAT基于精确算法,可以得到所有满足约束的解,但很难在大规模实例中得到应用。在EDA逻辑综合中组合电路优化时,不需要功能强大的单实例SAT求解器,开发一个更灵活、鲁棒性好、轻量级的SAT求解器可以更好地处理逻辑综合中产生的一系列小规模电路问题。

Key words: All solutions Boolean satisfiability(AllSAT); semi-tensor product of matrices; conjunctive normal form(CNF) satisfiability; circuit satisfiability;

No related articles found!
Full text



No Suggested Reading articles found!

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
  Copyright ©2015 JCST, All Rights Reserved