Multi-step partitioning combined with SOM neural network-based clustering technique effectively improves SAT solver performance

As the core engine of electronic design automation (EDA) tools, the efficiency of Boolean Satisfiability Problem (SAT) solver largely determines the cycle of integrated circuit research and development. The effectiveness of SAT solvers has steadily turned into the key bottleneck of circuit design cy...

Full description

Saved in:
Bibliographic Details
Main Authors: Siyu Yun, Xinsheng Wang
Format: Article
Language:English
Published: PeerJ Inc. 2025-08-01
Series:PeerJ Computer Science
Subjects:
Online Access:https://peerj.com/articles/cs-3076.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1849235384097046528
author Siyu Yun
Xinsheng Wang
author_facet Siyu Yun
Xinsheng Wang
author_sort Siyu Yun
collection DOAJ
description As the core engine of electronic design automation (EDA) tools, the efficiency of Boolean Satisfiability Problem (SAT) solver largely determines the cycle of integrated circuit research and development. The effectiveness of SAT solvers has steadily turned into the key bottleneck of circuit design cycle due to the dramatically increased integrated circuit scale. The primary issue of SAT solver now is the divergence between SAT used in industry and research on pure solution algorithms. We propose a strategy for partitioning the SAT problem based on the structural information then solving it. By effectively extracting the structure information from the original SAT problem, the self-organizing map (SOM) neural network deployed in the division section can speed up the sub-thread solver’s processing while avoiding cumbersome parameter adjustments. The experimental results demonstrate the stability and scalability of our technique, which can drastically shorten the time required to solve industrial benchmarks from various sources.
format Article
id doaj-art-77981343dc224ec589bf2d5b7b8359a8
institution Kabale University
issn 2376-5992
language English
publishDate 2025-08-01
publisher PeerJ Inc.
record_format Article
series PeerJ Computer Science
spelling doaj-art-77981343dc224ec589bf2d5b7b8359a82025-08-20T04:02:49ZengPeerJ Inc.PeerJ Computer Science2376-59922025-08-0111e307610.7717/peerj-cs.3076Multi-step partitioning combined with SOM neural network-based clustering technique effectively improves SAT solver performanceSiyu YunXinsheng WangAs the core engine of electronic design automation (EDA) tools, the efficiency of Boolean Satisfiability Problem (SAT) solver largely determines the cycle of integrated circuit research and development. The effectiveness of SAT solvers has steadily turned into the key bottleneck of circuit design cycle due to the dramatically increased integrated circuit scale. The primary issue of SAT solver now is the divergence between SAT used in industry and research on pure solution algorithms. We propose a strategy for partitioning the SAT problem based on the structural information then solving it. By effectively extracting the structure information from the original SAT problem, the self-organizing map (SOM) neural network deployed in the division section can speed up the sub-thread solver’s processing while avoiding cumbersome parameter adjustments. The experimental results demonstrate the stability and scalability of our technique, which can drastically shorten the time required to solve industrial benchmarks from various sources.https://peerj.com/articles/cs-3076.pdfSATSOM neural networkClusterDivideStructural information
spellingShingle Siyu Yun
Xinsheng Wang
Multi-step partitioning combined with SOM neural network-based clustering technique effectively improves SAT solver performance
PeerJ Computer Science
SAT
SOM neural network
Cluster
Divide
Structural information
title Multi-step partitioning combined with SOM neural network-based clustering technique effectively improves SAT solver performance
title_full Multi-step partitioning combined with SOM neural network-based clustering technique effectively improves SAT solver performance
title_fullStr Multi-step partitioning combined with SOM neural network-based clustering technique effectively improves SAT solver performance
title_full_unstemmed Multi-step partitioning combined with SOM neural network-based clustering technique effectively improves SAT solver performance
title_short Multi-step partitioning combined with SOM neural network-based clustering technique effectively improves SAT solver performance
title_sort multi step partitioning combined with som neural network based clustering technique effectively improves sat solver performance
topic SAT
SOM neural network
Cluster
Divide
Structural information
url https://peerj.com/articles/cs-3076.pdf
work_keys_str_mv AT siyuyun multisteppartitioningcombinedwithsomneuralnetworkbasedclusteringtechniqueeffectivelyimprovessatsolverperformance
AT xinshengwang multisteppartitioningcombinedwithsomneuralnetworkbasedclusteringtechniqueeffectivelyimprovessatsolverperformance