⚡ 本页包含 AI 生成的分析内容，仅供参考
该论文提出了一种名为VIP-Sat的布尔可满足性（SAT）求解器，采用5×12可变内存处理（In-Memory Processing）单元，实现了98%的可解性。该求解器针对SAT这一NP完全问题，适用于人工智能、机器学习、电子设计自动化等领域。
Boolean satisfiability (SAT), a non-deterministic polynomial (NP)-complete problem, has gained increasing attention with applications in artificial intelligence, machine learning, electronic design automation, and VLSI tests with practical examples, such as AI planning and ML model verification, fault diagnosis, combinational equivalence checking and automatic test pattern generation. The SAT problem is based on testing if a Boolean formula in conjunctive normal form (CNF) can be solved by finding a set of Boolean variables that satisfy the formula (i.e., makes the formula TRUE). Conventionally, software-based SAT-solving algorithms, such as WalkSAT, have been widely used. However, they have limitations in solving large-scale SAT problems with an increasing number of variables due to limited parallelism and a significant latency and energy overhead arising from frequent memory access. Alternatively, dedicated ASIC hardware
Chaeyun Shim, Jooyoung Bae, Bongjin Kim
University of California, Santa Barbara, CA