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

arXiv: https://arxiv.org/abs/2607.21188 · HTML: https://mlsanity.com/paper/2607.21188/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 21 references that are in the map.
- First posted on arXiv 23 Jul 2026.

## Builds on (most cited first, 4 of 4)

- [Universal Invariant and Equivariant Graph Neural Networks](https://mlsanity.com/paper/1905.04943/) (2019)
- [Using Logic Programming and Kernel-Grouping for Improving Interpretability of Convolutional Neural Networks](https://mlsanity.com/paper/2310.13073/) (2023)
- [CON-FOLD -- Explainable Machine Learning with Confidence](https://mlsanity.com/paper/2408.07854/) (2024)
- [Boolean Equi-propagation for Concise and Efficient SAT Encodings of Combinatorial Problems](https://mlsanity.com/paper/1402.0568/) (2014)

## Abstract (arXiv)

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