DEMOTIC：一种用于多级数字电路的可微分采样器
DEMOTIC: A Differentiable Sampler for Multi-Level Digital Circuits
AI总结：
针对数字电路可满足性采样的可扩展性问题，提出可微分采样器DEMOTIC，将CircuitSAT重构为监督回归任务，通过GPU并行加速，在ISCAS-85基准上较现有启发式方法提速超两个数量级。
摘要：
电路可满足性（CircuitSAT）是著名的NP完全问题，其可满足公式的高效采样对现代前端应用中数字电路的全面测试和验证至关重要。由于数字电路的固有复杂性、搜索空间大小以及过程中涉及的资源限制，生成此类样本是一个困难的计算问题。应对这些挑战促使了严重依赖启发式的专用算法的发展。然而，这些基于启发式的方法在需要从大量解中采样时经常遇到可扩展性问题，主要是由于其顺序性质。与这类启发式算法不同，我们提出了一种用于多级数字电路的新型可微分采样器DEMOTIC，它利用梯度下降（GD）解决CircuitSAT问题并获得广泛的有效且不同的解。DEMOTIC利用问题实例的电路结构，通过将CircuitSAT问题重构为监督多输出回归任务，使用GD学习有效解。这种可微分方法允许对张量的每个元素独立执行按位操作，实现学习操作的并行执行，因此与最先进的启发式采样器相比，GPU加速采样具有显著的运行时改进。我们在ISCAS-85基准套件的各种CircuitSAT实例上证明了DEMOTIC在采样任务中的优越运行时性能。具体而言，在大多数情况下，DEMOTIC的性能优于最先进的采样器两个数量级以上。
英文摘要：
Efficient sampling of satisfying formulas for circuit satisfiability (CircuitSAT), a well-known NP-complete problem, is essential in modern front-end applications for thorough testing and verification of digital circuits. Generating such samples is a hard computational problem due to the inherent complexity of digital circuits, size of the search space, and resource constraints involved in the process. Addressing these challenges has prompted the development of specialized algorithms that heavily rely on heuristics. However, these heuristic-based approaches frequently encounter scalability issues when tasked with sampling from a larger number of solutions, primarily due to their sequential nature. Different from such heuristic algorithms, we propose a novel differentiable sampler for multi-level digital circuits, called {\sc Demotic}, that utilizes gradient descent (GD) to solve the CircuitSAT problem and obtain a wide range of valid and distinct solutions. {\sc Demotic} leverages the circuit structure of the problem instance to learn valid solutions using GD by re-framing the CircuitSAT problem as a supervised multi-output regression task. This differentiable approach allows bit-wise operations to be performed independently on each element of a tensor, enabling parallel execution of learning operations, and accordingly, GPU-accelerated sampling with significant runtime improvements compared to state-of-the-art heuristic samplers. We demonstrate the superior runtime performance of {\sc Demotic} in the sampling task across various CircuitSAT instances from the ISCAS-85 benchmark suite. Specifically, {\sc Demotic} outperforms the state-of-the-art sampler by more than two orders of magnitude in most cases.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
