Effective Partitioning Method With Predictable Hardness for CircuitSAT
Many industrial verification problems are solved via reduction to CircuitSAT (curcuit satisfibiliaty). It is often the case that the resulting SAT instances are very hard and require the use of parallel computing to be solved in reasonable time. The particularly relevant problem in this context is h...
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2025-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/10820338/ |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1841550870616997888 |
|---|---|
| author | Konstantin Chukharev Irina Gribanova Dmitry Ivanov Stepan Kochemazov Victor Kondratiev Alexander Semenov |
| author_facet | Konstantin Chukharev Irina Gribanova Dmitry Ivanov Stepan Kochemazov Victor Kondratiev Alexander Semenov |
| author_sort | Konstantin Chukharev |
| collection | DOAJ |
| description | Many industrial verification problems are solved via reduction to CircuitSAT (curcuit satisfibiliaty). It is often the case that the resulting SAT instances are very hard and require the use of parallel computing to be solved in reasonable time. The particularly relevant problem in this context is how to best plan the use of the computing resources, because SAT solvers’ runtime is well known to be hard to predict. In the present paper we propose two methods that employ the knowledge about a circuit’s structure to partition a CircuitSAT instance into a specific number of simpler subproblems. A distinctive feature of the proposed partitioning methods is that they make it possible to estimate the hardness (e.g. the total runtime of a SAT solver on all subproblems) of a partitioning via the Monte Carlo method. In the experimental evaluation we apply these methods to hard CircuitSAT instances and compare their performance with the well known Cube and Conquer approach. The proposed partitioning methods not only often outperform Cube and Conquer, but also show remarkably small variance in the runtime of a SAT solver on subproblems from a partitioning, thus making it possible to construct accurate estimations of time required to process all subproblems, using random samples of small size. As a consequence, we have the efficient stochastic estimation procedure which provides an additional opportunity to employ hyperparameter tuning methods to further increase the SAT solver performance on (partitioned) hard SAT instances. We demonstrate the effectiveness of the proposed constructions by applying them to some problems associated with CircuitSAT, in particular, Logical Equivalence Checking benchmarks, Automated Test Pattern Generation benchmarks and the inversion problems of some cryptographic functions. |
| format | Article |
| id | doaj-art-bac4249d186e48ce955e229199ea8988 |
| institution | Kabale University |
| issn | 2169-3536 |
| language | English |
| publishDate | 2025-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj-art-bac4249d186e48ce955e229199ea89882025-01-10T00:00:45ZengIEEEIEEE Access2169-35362025-01-01134218423410.1109/ACCESS.2024.352512210820338Effective Partitioning Method With Predictable Hardness for CircuitSATKonstantin Chukharev0https://orcid.org/0000-0002-4636-2379Irina Gribanova1Dmitry Ivanov2Stepan Kochemazov3https://orcid.org/0000-0003-2848-5786Victor Kondratiev4https://orcid.org/0000-0003-0356-5149Alexander Semenov5https://orcid.org/0000-0001-6172-4801Faculty of Information Technologies and Programming, ITMO University, Saint Petersburg, RussiaISDCT SB RAS, Irkutsk, RussiaIndependent Researcher, Saint-Petersburg, RussiaFaculty of Information Technologies and Programming, ITMO University, Saint Petersburg, RussiaISDCT SB RAS, Irkutsk, RussiaFaculty of Information Technologies and Programming, ITMO University, Saint Petersburg, RussiaMany industrial verification problems are solved via reduction to CircuitSAT (curcuit satisfibiliaty). It is often the case that the resulting SAT instances are very hard and require the use of parallel computing to be solved in reasonable time. The particularly relevant problem in this context is how to best plan the use of the computing resources, because SAT solvers’ runtime is well known to be hard to predict. In the present paper we propose two methods that employ the knowledge about a circuit’s structure to partition a CircuitSAT instance into a specific number of simpler subproblems. A distinctive feature of the proposed partitioning methods is that they make it possible to estimate the hardness (e.g. the total runtime of a SAT solver on all subproblems) of a partitioning via the Monte Carlo method. In the experimental evaluation we apply these methods to hard CircuitSAT instances and compare their performance with the well known Cube and Conquer approach. The proposed partitioning methods not only often outperform Cube and Conquer, but also show remarkably small variance in the runtime of a SAT solver on subproblems from a partitioning, thus making it possible to construct accurate estimations of time required to process all subproblems, using random samples of small size. As a consequence, we have the efficient stochastic estimation procedure which provides an additional opportunity to employ hyperparameter tuning methods to further increase the SAT solver performance on (partitioned) hard SAT instances. We demonstrate the effectiveness of the proposed constructions by applying them to some problems associated with CircuitSAT, in particular, Logical Equivalence Checking benchmarks, Automated Test Pattern Generation benchmarks and the inversion problems of some cryptographic functions.https://ieeexplore.ieee.org/document/10820338/SATCircuitSATpartitioninghardness estimationlogical equivalence checkingautomated test pattern generation |
| spellingShingle | Konstantin Chukharev Irina Gribanova Dmitry Ivanov Stepan Kochemazov Victor Kondratiev Alexander Semenov Effective Partitioning Method With Predictable Hardness for CircuitSAT IEEE Access SAT CircuitSAT partitioning hardness estimation logical equivalence checking automated test pattern generation |
| title | Effective Partitioning Method With Predictable Hardness for CircuitSAT |
| title_full | Effective Partitioning Method With Predictable Hardness for CircuitSAT |
| title_fullStr | Effective Partitioning Method With Predictable Hardness for CircuitSAT |
| title_full_unstemmed | Effective Partitioning Method With Predictable Hardness for CircuitSAT |
| title_short | Effective Partitioning Method With Predictable Hardness for CircuitSAT |
| title_sort | effective partitioning method with predictable hardness for circuitsat |
| topic | SAT CircuitSAT partitioning hardness estimation logical equivalence checking automated test pattern generation |
| url | https://ieeexplore.ieee.org/document/10820338/ |
| work_keys_str_mv | AT konstantinchukharev effectivepartitioningmethodwithpredictablehardnessforcircuitsat AT irinagribanova effectivepartitioningmethodwithpredictablehardnessforcircuitsat AT dmitryivanov effectivepartitioningmethodwithpredictablehardnessforcircuitsat AT stepankochemazov effectivepartitioningmethodwithpredictablehardnessforcircuitsat AT victorkondratiev effectivepartitioningmethodwithpredictablehardnessforcircuitsat AT alexandersemenov effectivepartitioningmethodwithpredictablehardnessforcircuitsat |