Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits

• URL: http://arxiv.org/abs/2210.01484v1
• Date: Tue, 4 Oct 2022 09:19:13 GMT
• Title: Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits
• Authors: Alexander Semenov, Konstantin Chukharev, Egor Tarasov, Daniil Chivilikhin and Viktor Kondratiev
• Abstract summary: We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
• Score: 58.83758257568434
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In this paper we investigate how to estimate the hardness of Boolean satisfiability (SAT) encodings for the Logical Equivalence Checking problem (LEC). Meaningful estimates of hardness are important in cases when a conventional SAT solver cannot solve a SAT instance in a reasonable time. We show that the hardness of SAT encodings for LEC instances can be estimated \textit{w.r.t.} some SAT partitioning. We also demonstrate the dependence of the accuracy of the resulting estimates on the probabilistic characteristics of a specially defined random variable associated with the considered partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy. In the experimental part we propose a class of scalable LEC tests that give extremely complex instances with a relatively small input size $n$ of the considered circuits. For example, for $n = 40$, none of the state-of-the-art SAT solvers can cope with the considered tests in a reasonable time. However, these tests can be solved in parallel using the proposed partitioning methods.

Related papers

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  We introduce hardware accelerated algorithms for fast SAT problem generation and a geometric SAT encoding. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models.
  arXiv  Detail & Related papers  (2024-10-18T22:25:54Z)
• ParaICL: Towards Robust Parallel In-Context Learning [74.38022919598443]
  Large language models (LLMs) have become the norm in natural language processing. Few-shot in-context learning (ICL) relies on the choice of few-shot demonstration examples. We propose a novel method named parallel in-context learning (ParaICL)
  arXiv  Detail & Related papers  (2024-03-31T05:56:15Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
  arXiv  Detail & Related papers  (2023-12-16T12:44:36Z)
• Using deep learning to construct stochastic local search SAT solvers with performance bounds [0.0]
  We train oracles using Graph Neural Networks and evaluate them on two SLS solvers on random SAT instances of varying difficulty. We find that access to GNN-based oracles significantly boosts the performance of both solvers.
  arXiv  Detail & Related papers  (2023-09-20T16:27:52Z)
• Machine Learning for SAT: Restricted Heuristics and New Graph Representations [0.8870188183999854]
  SAT is a fundamental NP-complete problem with many applications, including automated scheduling. To solve large instances, SAT solvers have to rely on Booleans, e.g., choosing a branching variable in DPLL and CDCL solvers. We suggest a strategy of making a few initial steps with a trained ML model and then releasing control to classical runtimes.
  arXiv  Detail & Related papers  (2023-07-18T10:46:28Z)
• Sequential Permutation Testing of Random Forest Variable Importance Measures [68.8204255655161]
  It is proposed here to use sequential permutation tests and sequential p-value estimation to reduce the high computational costs associated with conventional permutation tests. The results of simulation studies confirm that the theoretical properties of the sequential tests apply. The numerical stability of the methods is investigated in two additional application studies.
  arXiv  Detail & Related papers  (2022-06-02T20:16:50Z)
• DeepSAT: An EDA-Driven Learning Framework for SAT [9.111341161918375]
  We present DeepSAT, a novel end-to-end learning framework for the Boolean satisfiability (SAT) problem. DeepSAT achieves significant accuracy improvements over state-of-the-art learning-based SAT solutions.
  arXiv  Detail & Related papers  (2022-05-27T03:20:42Z)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
  arXiv  Detail & Related papers  (2022-03-02T05:14:12Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.