Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning

• URL: http://arxiv.org/abs/2607.21188v1
• Date: Thu, 23 Jul 2026 11:15:55 GMT
• Title: Identifying Good Rules for Efficient SAT Encodings of Single-Constant Multiplication Using Machine Learning
• Abstract summary: We propose a neuro-symbolic framework that accelerates SCM SAT encoding by identifying good rules for guiding operator selection during decomposition.<n> Experimental results on unseen 17-32 bit constants demonstrate one to two orders of magnitude reductions in encoding time, over 97% reduction in memory usage, and an order-of-magnitude decrease in branching.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The Single Constant Multiplication problem is a fundamental NP-hard optimization task in hardware design, which seeks to decompose a fixed constant using only additions, subtractions, and bit-shifts. Although dynamic programming methods can produce near-optimal SAT encodings for SCM, their encoding cost remains high for large constants. We propose a neuro-symbolic framework that accelerates SCM SAT encoding by identifying good rules for guiding operator selection during decomposition. Our approach employs a graph neural network model to predict promising operator types from constant decompositions, and exploits the resulting confidence scores to prune no-good choices in the symbolic search. Experimental results on unseen 17-32 bit constants demonstrate one to two orders of magnitude reductions in encoding time, over 97% reduction in memory usage, and an order-of-magnitude decrease in branching, while preserving near-optimal encoding quality in terms of additions. These results show that learning-guided symbolic strategies can significantly improve the scalability and efficiency of SCM encoding. Our code and data are publicly available at: https://github.com/Chufeng-Jiang/SCM_MLDP

Related papers

• Coset Ensemble Decoder for Quantum Error Correction with Algorithm-Hardware Co-Design [16.143601808851162]
  quantum error correction (QEC) continuously extracts and decodes error syndromes in real time.<n>A critical component in QEC is the decoder, a classical subsystem that must simultaneously deliver high logical accuracy and ultra-low latency.<n>This paper presents a novel algorithm-hardware co-design that improves the accuracy-latency trade-off over existing approaches.
  arXiv  Detail & Related papers  (2026-06-09T16:37:13Z)
• Effectiveness of Binary Autoencoders for QUBO-Based Optimization Problems [0.669087470775851]
  In black-box optimization, objective evaluations are often expensive, so high quality solutions must be found under a limited budget.<n>Recent work combines FMQA with a binary autoencoder that learns a compact binary latent code from feasible solutions.<n>We show that the bAE reconstructs feasible tours accurately and, compared with manually designed encodings at similar compression, better aligns tour distances with latent Hamming distances.
  arXiv  Detail & Related papers  (2026-02-10T17:59:29Z)
• Fast correlated decoding of transversal logical algorithms [67.01652927671279]
  Quantum error correction (QEC) is required for large-scale computation, but incurs a significant resource overhead.<n>Recent advances have shown that by jointly decoding logical qubits in algorithms composed of logical gates, the number of syndrome extraction rounds can be reduced.<n>Here, we reform the problem of decoding circuits by directly decoding relevant logical operator products as they propagate through the circuit.
  arXiv  Detail & Related papers  (2025-05-19T18:00:00Z)
• A PyTorch-Compatible Spike Encoding Framework for Energy-Efficient Neuromorphic Applications [36.52207669429316]
  Spiking Neural Networks (SNNs) offer promising energy efficiency advantages, particularly when processing sparse spike trains.<n>This paper introduces a novel, open-source PyTorch-compatible Python framework for spike encoding.
  arXiv  Detail & Related papers  (2025-04-15T09:50:03Z)
• Accelerating Error Correction Code Transformers [56.75773430667148]
  We introduce a novel acceleration method for transformer-based decoders. We achieve a 90% compression ratio and reduce arithmetic operation energy consumption by at least 224 times on modern hardware.
  arXiv  Detail & Related papers  (2024-10-08T11:07:55Z)
• Low-Weight High-Distance Error Correcting Fermionic Encodings [0.0]
  We search for practical fermion-to-qubit encodings with error correcting properties. We report multiple promising high-distance encodings which significantly improve the weights of stabilizers and logical operators.
  arXiv  Detail & Related papers  (2024-02-23T15:32:57Z)
• GEC-DePenD: Non-Autoregressive Grammatical Error Correction with Decoupled Permutation and Decoding [52.14832976759585]
  Grammatical error correction (GEC) is an important NLP task that is usually solved with autoregressive sequence-to-sequence models. We propose a novel non-autoregressive approach to GEC that decouples the architecture into a permutation network. We show that the resulting network improves over previously known non-autoregressive methods for GEC.
  arXiv  Detail & Related papers  (2023-11-14T14:24:36Z)
• Factorizers for Distributed Sparse Block Codes [45.29870215671697]
  We propose a fast and highly accurate method for factorizing distributed block codes (SBCs) Our iterative factorizer introduces a threshold-based nonlinear activation, conditional random sampling, and an $ell_infty$-based similarity metric. We demonstrate the feasibility of our method on four deep CNN architectures over CIFAR-100, ImageNet-1K, and RAVEN datasets.
  arXiv  Detail & Related papers  (2023-03-24T12:31:48Z)
• Rapid Person Re-Identification via Sub-space Consistency Regularization [51.76876061721556]
  Person Re-Identification (ReID) matches pedestrians across disjoint cameras. Existing ReID methods adopting real-value feature descriptors have achieved high accuracy, but they are low in efficiency due to the slow Euclidean distance computation. We propose a novel Sub-space Consistency Regularization (SCR) algorithm that can speed up the ReID procedure by 0.25$ times.
  arXiv  Detail & Related papers  (2022-07-13T02:44:05Z)
• Quantized Neural Networks via {-1, +1} Encoding Decomposition and Acceleration [83.84684675841167]
  We propose a novel encoding scheme using -1, +1 to decompose quantized neural networks (QNNs) into multi-branch binary networks. We validate the effectiveness of our method on large-scale image classification, object detection, and semantic segmentation tasks.
  arXiv  Detail & Related papers  (2021-06-18T03:11:15Z)
• Less is More: Pre-training a Strong Siamese Encoder Using a Weak Decoder [75.84152924972462]
  Many real-world applications use Siamese networks to efficiently match text sequences at scale. This paper pre-trains language models dedicated to sequence matching in Siamese architectures.
  arXiv  Detail & Related papers  (2021-02-18T08:08:17Z)
• Consistent Multiple Sequence Decoding [36.46573114422263]
  We introduce a consistent multiple sequence decoding architecture. This architecture allows for consistent and simultaneous decoding of an arbitrary number of sequences. We show the efficacy of our consistent multiple sequence decoder on the task of dense relational image captioning.
  arXiv  Detail & Related papers  (2020-04-02T00:43:54Z)

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.