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

The paper presents a neuro-symbolic framework for accelerating SAT encoding of Single Constant Multiplication (SCM), an NP-hard hardware optimization problem using additions, subtractions, and shifts. A graph neural network predicts promising operator types from constant decompositions, and confidence scores guide symbolic pruning of unfavorable choices. On unseen 17–32-bit constants, the authors report one- to two-order-of-magnitude reductions in encoding time, over 97% lower memory usage, and an order-of-magnitude reduction in branching, while preserving near-optimal addition counts. Code and data are available in the SCM_MLDP repository.