Pith. sign in

REVIEW 2 major objections 8 minor 41 references

Miter-Aware LUT Mapping: Aligning Structure and Solvability for Efficient Logic Equivalence Checking

T0 review · 2 major / 8 minor · reviewed 2026-07-09 · glm-5.2

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Reformulating the miter before solving cuts SAT runtime by 92%

desk verdict Joint LUT mapping of both miter sides is a genuinely new idea for LEC, but the solver-oriented metric weights are tuned on an undisclosed set with no out-of-distribution test. read the letter →

arxiv 2607.07164 v1 pith:CAGK3PNC submitted 2026-07-08 cs.AR cs.LO

Jiaying Zhu , Zhengyuan Shi , Mengxia Tao , Kezhi Li , Min Li , Qiang Xu This is my paper
classification cs.ARcs.LO
keywords logicequivalencecheckingLUTmappingSATsolvingmitercircuitGaussianeliminationXORmodelingsolver-friendlyencodingCNFoptimization
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper argues that in Logic Equivalence Checking — the task of proving two circuit designs compute identical functions — the bottleneck is not the SAT solver but how the comparison circuit (the miter) is modeled before solving. The authors propose replacing the conventional flat netlist miter with a Look-up Table (LUT)-based miter built through three coordinated steps: equivalence-preserving mapping that aligns corresponding substructures across both designs so internal equivalences survive synthesis transformations, Gaussian-guided XOR modeling that detects XOR-dense regions, performs Gaussian elimination over GF(2) to extract affine relations, and materializes them as explicit XOR LUTs, and a solver-oriented LUT selection criterion that scores candidate LUTs on branching efficiency, propagation strength, conflict interpretability, and structural compactness. The combined framework reduces PAR2 scores by up to 92.1% across five solvers and engines, with an 83.3% average improvement, demonstrating that problem formulation — not solver improvement — can be the dominant lever for LEC performance.

What carries the argument

LUT-based miter — a reformulation of the equivalence-checking problem in which both circuits are mapped to Look-up Table abstractions before SAT encoding, preserving structural correspondence and exposing algebraic structure that a flat netlist would obscure.

What would settle it

Construct two circuit families with similar XOR density but different structural topology (e.g., tree-structured vs. chain-structured arithmetic) and show that the same Bayesian-optimized weights produce inconsistent PAR2 improvements across families, indicating the weights encode design-family priors rather than solver-invariant properties.

Watch

Extended reading notes

Core claim

The central discovery is that the representation of the miter, constructed before any SAT solving begins, determines solving difficulty more than solver choice. By jointly mapping both circuits to LUT abstractions with structural alignment, algebraic XOR simplification, and solver-aware selection, the framework converts a hard SAT instance into an easier one without changing the solver. The equivalence-preserving mapping alone reduces runtime by 62.5%, and the Gaussian-guided XOR modeling alone yields 36.8% on XOR-dense circuits, showing these are independently effective mechanisms targeting distinct failure modes of current LEC pipelines.

Load-bearing premise

The solver-friendliness cost function uses weights tuned on a small validation set, and the paper asserts without evidence that these weights generalize to design families outside the tuning data. If the optimal weights are design-dependent, the reported gains would not transfer to unseen benchmarks.

Editorial extensions

If this is right

  • If the modeling stage dominates LEC performance, then future verification tooling should invest in problem reformulation rather than solely pushing solver internals.
  • The joint mapping of two circuits — rather than optimizing each independently — suggests that cross-design structural correspondence is a first-class resource in equivalence checking, not just a byproduct of similar designs.
  • Gaussian elimination over GF(2) integrated into circuit-level abstraction hints that algebraic and logical reasoning can be interleaved at the representation level, not just inside the solver.
  • The solver-friendliness metrics (branch count, determinacy, monotonicity, conflict interpretability, compactness) could generalize to other SAT-encoded problems beyond LEC, such as model checking or constraint satisfaction over circuit-derived instances.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The claim that Bayesian-optimized weights are robust across all validation sets without out-of-distribution evidence suggests the metrics may capture genuinely solver-relevant properties that transfer, but this distinction between solver-intrinsic and design-family-specific patterns is untested.
  • The framework's compatibility with existing LEC engines like ABC's CEC suggests it could deploy as a pre-processing layer in industrial flows, but the under-10% formulation overhead claim needs validation on larger industrial designs where mapping cost may scale differently.
  • The restriction to 2/3/4-input LUTs is driven by CNF encoding complexity, but if solver-native XOR reasoning were used, larger LUTs or direct XOR-clause support might shift the cost-benefit tradeoff and change which metrics dominate.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 8 minor

Summary. This paper proposes a miter-aware LUT mapping framework for Logic Equivalence Checking (LEC) that reformulates the miter circuit before SAT solving. The framework integrates three components: (1) equivalence-preserving LUT mapping that aligns structurally corresponding regions across golden and implementation designs, (2) Gaussian-guided XOR modeling that detects XOR-dense regions and applies Gaussian elimination over GF(2) to extract explicit affine relations, and (3) solver-oriented LUT selection guided by five metrics (branch count, sensitivity, determinacy, monotonicity, conflict interpretability) aggregated with Bayesian-optimized weights. The method is evaluated on benchmarks from ITC99, EPFL, OpenCores, and industrial sources across five solvers (Kissat, CaDiCaL, X-SAT, CSAT, CEC), reporting up to 92.1% PAR2 reduction. The core idea—that miter modeling before solving is as important as solver performance—is well-motivated and the experimental gains are substantial. The equivalence-preserving mapping and Gaussian-guided XOR modeling components are well-grounded in ablation studies. However, the solver-oriented LUT selection component has a validation gap that undermines confidence in its generalization.

Significance. The paper addresses a practically important problem in hardware verification. The conceptual contribution of unifying LUT mapping with SAT reasoning for the miter-specific setting (rather than single-circuit SAT) is a genuine departure from prior work. The experimental methodology is commendable: five solvers spanning CNF-based, circuit-based, and dedicated LEC engines, comprehensive benchmarks from multiple public and industrial sources, PAR2 metrics with timeout penalties, and ablation studies isolating each component. The Gaussian-guided XOR modeling is a clean integration of algebraic techniques into circuit-level abstraction. The equivalence-preserving mapping idea of using XOR/XNOR gates near primary outputs as alignment anchors is elegant and practical. The reported 92.1% PAR2 reduction on CaDiCaL and consistent gains across all solvers are significant if they generalize.

major comments (2)
  1. §3.4, Cost aggregation and weight learning: The five solver-friendliness metrics are aggregated with Bayesian-optimized weights w_i tuned on a 'small validation set' whose size, composition, and relationship to the test benchmarks are undisclosed. The paper claims robustness 'across all validation sets' but provides no cross-validation results, no held-out family test, and no variance or confidence intervals. The text also states that 'higher f_det for SAT, higher f_branch for UNSAT' solvers, implying per-paradigm weight configurations. If weights are tuned separately for satisfaction-oriented vs. proof-oriented solvers, the effective parameter count doubles on a small tuning set, raising overfitting risk. The ablation in Figure 4 shows the tuned metric outperforms Comp.1 by 34.1%, but this gain is the portion most vulnerable to tuning-set memorization. Without at least one out-of-domain
  2. §3.2, Equivalence-preserving LUT mapping: The structural similarity heuristic combines 'topological depth, fan-in/fan-out counts, and the functional hash of the immediate logic cone,' but the relative weights or combination formula for these factors is not specified. Since this heuristic determines which node pairs are matched across designs—and matched nodes retain equivalence variables in the CNF while unmatched nodes are absorbed—the heuristic's design directly affects the quality of structural alignment. A reader cannot reproduce or assess this component without knowing how these three factors are combined. Please specify the formula or algorithm, and if applicable, report sensitivity to the heuristic parameters.
minor comments (8)
  1. §1: The abstract and introduction state '92.1% reduction across state-of-the-art SAT solvers,' but Table 2 shows 92.1% only for CaDiCaL; other solvers show 91.44%, 87.35%, 79.17%, 66.49%. The phrasing 'up to 92.1% across solvers' is technically correct but could be misread as 92.1% for all solvers. Consider clarifying that this is the maximum single-solver reduction.
  2. §3.3: The Gaussian elimination example is clear, but the paper does not specify how XOR-dense regions are detected (threshold? density metric?) before GE is applied. A brief description of the detection criterion would improve reproducibility.
  3. §3.4: The metrics f_branch, f_sensitivity, f_det, f_interp, f_compact are defined for individual LUTs, but the paper does not clarify whether the cost function Cost(L) is evaluated per-LUT during mapping or aggregated over the entire network. The mapping algorithm's selection procedure (greedy? dynamic programming?) is not specified.
  4. §4.1: The paper states LUTs are restricted to 2-, 3-, and 4-input because larger LUTs produce 'exponentially more complex CNF encodings (2^n clauses).' This is correct for naive encodings, but Tseitin encoding produces linear clauses. The justification should be stated more precisely.
  5. Table 2: The 'Impv.' column shows percentage of additional instances solved, while 'PAR2 Red.' shows percentage reduction in PAR2 score. These are different metrics and could confuse readers. A footnote or clearer column header would help.
  6. §4.2: The paper states the formulation overhead accounts for '<10%' of PAR2, but it would be useful to report the absolute mapping runtime separately, especially for large instances, to verify that the overhead does not scale superlinearly with circuit size.
  7. Figure 1: The diagram is dense and some labels (e.g., 'weight*', 'Conflict interpretability') are difficult to read. Consider enlarging or simplifying.
  8. References [33] and [37] are cited as prior work applying LUT mapping to single-circuit SAT. The distinction between these works and the current paper is clear, but the novelty boundary (what is genuinely new vs. incremental over [37]) could be stated more precisely.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found; derivation is self-contained against external benchmarks

full rationale

The paper's three components are independently grounded. (1) Equivalence-preserving LUT mapping uses structural heuristics (topological depth, fan-in/fan-out, functional hash) to align golden and implementation circuits—no output quantity is defined in terms of the result it claims to produce. (2) Gaussian-guided XOR modeling applies standard Gaussian elimination over GF(2) (citing external works [17, 22]) to extract affine relations; this is a well-known algebraic technique, not a self-defined construct. (3) The solver-oriented LUT selection metrics (branch count, sensitivity, determinacy, monotonicity, conflict interpretability, structural compactness) are each defined from truth-table properties of the LUT function, independent of the solving results they aim to predict. The Bayesian-optimized weights w_i are tuned on a validation set, which raises generalization/overfitting concerns (a correctness risk), but this is not circularity: the weights do not make the cost function tautologically equal to the solving time, and the final evaluation uses external benchmarks (ITC99, EPFL, OpenCores, ForgeEDA) with independent solvers (Kissat, CaDiCaL, X-SAT, CSAT, CEC). Self-citations ([33], [37], [36], [42]) are for tools and benchmarks used in evaluation, not for load-bearing theoretical premises. No step in the derivation chain reduces to its own inputs by construction.

Assumptions & free parameters 2 free parameters · 4 assumptions · 0 invented entities

The paper introduces no new physical or mathematical entities. The solver-friendliness metrics are reformulations of known SAT-solving concepts (branching, propagation, conflict analysis) into LUT-level cost functions. The free parameters (w_i) are fitted weights, and the axioms are domain assumptions standard to the EDA/SAT literature, with two ad-hoc heuristics whose effectiveness is validated empirically but not proven.

free parameters (2)
  • w_i (metric weights) = Bayesian-optimized, exact values not reported
    The cost function Cost(L) = sum_i w_i * f_i(L) uses weights tuned on a validation set to minimize solving time (Sec 3.4). These are free parameters fitted to data.
  • LUT size k = 2, 3, or 4
    Restricted to 2/3/4-input LUTs (Sec 4.1) because larger LUTs produce exponentially complex CNF. This is a design choice justified empirically but not derived.
assumptions (4)
  • domain assumption CDCL-based SAT solvers poorly handle XOR-dense constraints
    Invoked in Sec 1 and Sec 3.3 to motivate Gaussian-guided XOR modeling. This is a well-established observation in the SAT community [10,39,40].
  • ad hoc to paper Structural similarity heuristic (topological depth + fan-in/fan-out + functional hash) identifies corresponding nodes across synthesized designs
    Sec 3.2 states this heuristic is used to match LUT candidates across designs. No formal guarantee or empirical success rate is provided.
  • ad hoc to paper The five solver-friendliness metrics (branch count, sensitivity, determinacy, monotonicity, conflict interpretability) are sufficient to predict SAT solving difficulty
    Sec 3.4 defines these metrics and aggregates them. The paper states propagation and branching metrics 'dominate' but does not prove these five are necessary or sufficient.
  • standard math Gaussian elimination over GF(2) correctly captures all relevant affine relations in XOR-dense regions
    Standard linear algebra over finite fields (Sec 3.3). The mathematical correctness is not in question; the assumption is that the detected XOR relations are the ones that matter for solver performance.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Miter-Aware LUT Mapping: Aligning Structure and Solvability for Efficient Logic Equivalence Checking." pith.science (2026). https://pith.science/paper/CAGK3PNC

@misc{pith2026260707164,
  author       = {Pith},
  title        = {Pith review of: Miter-Aware LUT Mapping: Aligning Structure and Solvability for Efficient Logic Equivalence Checking},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/CAGK3PNC}},
  note         = {Machine review of arXiv:2607.07164}
}
read the original abstract

Logic Equivalence Checking (LEC), a fundamental hardware verification task, is often bottlenecked by synthesis-induced structural perturbations and XOR-dense regions that degrade SAT solver performance. We contend that the modeling of the miter is as critical as the SAT solver itself. To this end, we introduce a miter-aware mapping framework that strategically formulates the problem before solving. By constructing a LUT-based miter -- instead of a traditional, flat netlist -- our approach preserves critical structural correspondence between the two designs while making high-level logic relations explicit. Our framework uniquely integrates three techniques: equivalence-preserving mapping to structurally align the two circuits, Gaussian-guided XOR modeling to algebraically simplify dense arithmetic, and solver-oriented LUT selection to generate a representation optimized for efficient SAT reasoning. Evaluated on comprehensive datasets, our method achieves up to a \textbf{92.1\%} reduction across state-of-the-art SAT solvers. This demonstrates that a solver-aware modeling paradigm, which unifies structural mapping with SAT reasoning, can fundamentally enhance LEC efficiency.

Figures

Figures reproduced from arXiv: 2607.07164 by the authors.

Figure 1
Figure 1. Overview of the proposed mapping-based framework. Given a miter of two circuits under verification, our framework [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Illustration of equivalence-preserving mapping. [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 4
Figure 4. Solving performance under the solver-oriented LUT [PITH_FULL_IMAGE:figures/full_fig_p006_4.png] view at source ↗
Figures from the paper (1 more)
Figure 3
Figure 3. Figure 3: Solving performance on 20 multipliers under the [PITH_FULL_IMAGE:figures/full_fig_p006_3.png]

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

41 extracted references · 41 canonical work pages

  1. [1]

    Shuja Abbasi, Zulhelmi Zulhelmi, and Abdulrahman Alamoud. 2015. FPGA Design, Simulation and Prototyping of a High Speed 32-bit Pipeline Multiplier Based on Vedic Mathematics.IEICE Electronics Express12 (07 2015). doi:10.1587/ elex.12.20150450

    work page 2015

  2. [3]

    Biere Armin, Faller Tobias, Fazekas Katalin, Fleury Mathias, Froleyks Nils, and Pollitt Florian. 2024. CaDiCaL, Gimsatul, IsaSAT and Kissat entering the SAT Competition 2024.Proc. of SAT Competition(2024), 8–10

    work page 2024

  3. [4]

    Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks, and Florian Pollitt. 2024. CaDiCaL 2.0. Springer-Verlag, Berlin, Heidelberg, 133–152. doi:10.1007/978-3-031-65627-9_7

    work page doi:10.1007/978-3-031-65627-9_7 2024

  4. [5]

    Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks. 2024. Clausal congruence closure. In27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Schloss Dagstuhl–Leibniz-Zentrum für Infor- matik, 6–1

    work page 2024

  5. [6]

    Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh. 2021.Hand- book of Satisfiability. Frontiers in Artificial Intelligence and Applications, Vol. 336. IOS Press

    work page 2021

  6. [7]

    Robert K Brayton, Gary D Hachtel, and Alberto L Sangiovanni-Vincentelli. 2002. Multilevel logic synthesis.Proc. IEEE78, 2 (2002), 264–300

    work page 2002

  7. [8]

    Brayton and Alan Mishchenko

    Robert K. Brayton and Alan Mishchenko. 2010. ABC: A System for Sequential Synthesis and Verification. InProceedings of the 22nd International Conference on Computer Aided Verification (CA V). 24–40

    work page 2010

  8. [9]

    Serap Cekli and Ali Akman. 2024. A high speed pipelined radix-16 Booth multi- plier architecture for FPGA implementation.AEU - International Journal of Elec- tronics and Communications185 (2024), 155435. doi:10.1016/j.aeue.2024.155435

    work page doi:10.1016/j.aeue.2024.155435 2024

Show all 41 references
  1. [10]

    Jingchao Chen. 2009. Building a hybrid SAT solver via conflict-driven, look- ahead and XOR reasoning techniques. InInternational Conference on Theory and Applications of Satisfiability Testing. Springer, 298–311

    2009

  2. [11]

    Davidson

    S. Davidson. 1999. ITC’99 Benchmark Circuits - Preliminary Results. InInter- national Test Conference 1999. Proceedings (IEEE Cat. No.99CH37034). 1125–1125. doi:10.1109/TEST.1999.805857

    1999 doi

  3. [12]

    Niklas Eén and Armin Biere. 2005. Effective preprocessing in SAT through vari- able and clause elimination. InInternational conference on theory and applications of satisfiability testing. Springer, 61–75

    2005

  4. [13]

    Niklas Een and Alan Mishchenko. 2007. Incremental SAT sweeping. InProceedings of the IEEE/ACM International Conference on Computer-Aided Design (ICCAD). IEEE, 223–230

    2007

  5. [14]

    Niklas Eén, Alan Mishchenko, and Niklas Sörensson. 2007. Applying logic syn- thesis for speeding up SAT. InInternational Conference on Theory and Applications of Satisfiability Testing. Springer, 272–286

    2007

  6. [15]

    Hu, Sam Bayless, Syed M

    Nick Feng, Alan J. Hu, Sam Bayless, Syed M. Iqbal, Patrick Trentin, Michael W. Whalen, Lee Pike, and John Backes. 2024. DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories.ArXivabs/2401.10703 (2024). https://api. semanticscholar.org/CorpusID:267061064

    2024 arXiv

  7. [16]

    Youssef Hamadi, Said Jabbour, and Jabbour Sais. 2012. Control-based clause sharing in parallel SAT solving. InAutonomous Search. Springer, 245–267

    2012

  8. [17]

    Cheng-Shen Han and Jie-Hong Roland Jiang. 2012. When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way. InInternational Conference on Computer Aided Verification. https://api.semanticscholar.org/CorpusID:18689957

    2012

  9. [18]

    2012.Formal equivalence checking and design debugging

    Shi-Yu Huang and Kwang-Ting Tim Cheng. 2012.Formal equivalence checking and design debugging. Vol. 12. Springer Science & Business Media

    2012

  10. [19]

    Daniela Kaufmann and Armin Biere. 2023. Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra.International Journal on Software Tools for Technology Transfer25 (01 2023), 1–12. doi:10.1007/s10009- 022-00688-6

    2023 doi

  11. [20]

    Andreas Kuehlmann and Florian Krohm. 2000. Combinational and sequential equivalence checking: Theory and practice.IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems19, 12 (2000), 1428–1449

    2000

  12. [21]

    Jia Hui Liang, Vijay Ganesh, Ed Zulkoski, Atulan Zaman, and Krzysztof Czar- necki. 2015. Understanding VSIDS branching heuristics in conflict-driven clause- learning SAT solvers. InHaifa Verification Conference. Springer, 225–241

    2015

  13. [22]

    Ole Lübke. 2024. IGMaxHS–An Incremental MaxSAT Solver with Support for XOR Clauses.arXiv preprint arXiv:2410.15897(2024)

    2024 arXiv

  14. [23]

    Lucas Machado and Jordi Cortadella. 2017. Boolean decomposition for aig opti- mization. InProceedings of the Great Lakes Symposium on VLSI 2017. 143–148

    2017

  15. [24]

    Joao Marques-Silva, Inês Lynce, and Sharad Malik. 2009. Conflict-driven clause learning SAT solvers.Handbook of satisfiability(2009), 131–153

    2009

  16. [25]

    McCluskey

    Edward J. McCluskey. 1956. Minimization of Boolean functions.Bell System Technical Journal35, 6 (1956), 1417–1444

    1956

  17. [26]

    Alan Mishchenko and Robert K. Brayton. 2006. Scalable logic synthesis using a simple circuit structure. InProc. IWLS, Vol. 6. 15–22

    2006

  18. [27]

    Alan Mishchenko, Satrajit Chatterjee, and Robert Brayton. 2006. DAG-aware AIG rewriting a fresh look at combinational logic synthesis. InProceedings of the 43rd annual Design Automation Conference. 532–535

    2006

  19. [28]

    Alan Mishchenko, Satrajit Chatterjee, and Robert Brayton. 2006. Simulation- based boolean equivalence checking using AIGs. InProceedings of the International Workshop on Logic and Synthesis (IWLS). 7–12

    2006

  20. [29]

    2006.Bayesian Approach to Global Optimization

    Jonas Mockus. 2006.Bayesian Approach to Global Optimization. Vol. 37. 473–481. doi:10.1007/BFb0006170

    2006 doi

  21. [30]

    In-Ho Moon and Carl Pixley. 2004. Non-miter-based combinational equivalence checking by comparing BDDs with different variable orders. InInternational Conference on Formal Methods in Computer-Aided Design. Springer, 144–158

    2004

  22. [31]

    Naomi Nishimura, Prabhakar Ragde, and Stefan Szeider. 2004. Detecting Backdoor Sets with Respect to Horn and Binary Clauses. InInternational Conference on Theory and Applications of Satisfiability Testing. https://api.semanticscholar.org/ CorpusID:15232413

    2004

  23. [32]

    Team OpenCore. 1999. OpenCore.https://opencores.org/(1999)

    1999

  24. [33]

    Yuhang Qian, Zhihan Chen, Xindi Zhang, and Shaowei Cai. 2025. X-SAT: An Efficient Circuit-Based SAT Solver. In2025 62nd ACM/IEEE Design Automation Conference (DAC). IEEE, 1–7

    2025

  25. [34]

    Willard V. Quine. 1952. The problem of simplifying truth functions.The American Mathematical Monthly59, 8 (1952), 521–531

    1952

  26. [35]

    Zhengyuan Shi, Wentao Jiang, Xindi Zhang, Jin Luo, Yun Liang, Zhufei Chu, and Qiang Xu. 2025. Dynamicsat: Dynamic configuration tuning for sat solving. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Schloss Dagstuhl–Leibniz-Zen...

    2025

  27. [36]

    Zhengyuan Shi, Zeju Li, Chengyu Ma, Yunhao Zhou, Ziyang Zheng, Jiawei Liu, Hongyang Pan, Lingfeng Zhou, Kezhi Li, Jiaying Zhu, Lingwei Yan, Zhiqiang He, Chenhao Xue, Wentao Jiang, Fan Yang, Guangyu Sun, Xiaoyan Yang, Gang Chen, Chuan Shi, Zhufei Chu, Jun Yang, and Qiang Xu. 20...

    2025 arXiv

  28. [37]

    Zhengyuan Shi, Tiebing Tang, Jiaying Zhu, Sadaf Khan, Hui-Ling Zhen, Minjie Yuan, Zhufei Chu, and Qiang Xu. 2025. Logic Optimization Meets SAT: A Novel Framework for Circuit-SAT Solving. InProceedings of the 62nd ACM/IEEE Design Automation Conference (DAC). 1–6

    2025

  29. [38]

    Mathias Soeken, Heinz Riener, Winston Haaswijk, Eleonora Testa, Bruno Schmitt, Giulia Meuli, Fereshte Mozafari, Siang-Yun Lee, Alessandro Tempia Calvino, Dewmini Sudara Marakkalage, et al. 2018. The EPFL logic synthesis libraries. arXiv preprint arXiv:1805.05121(2018)

    2018 arXiv

  30. [39]

    Mate Soos and Kuldeep S Meel. 2019. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. InProceedings of the AAAI Conference on Artificial Intelligence, Vol. 33. 1592–1599

    2019

  31. [40]

    Mate Soos, Karsten Nohl, and Claude Castelluccia. 2009. Extending SAT solvers to cryptographic problems. InInternational Conference on Theory and Applications of Satisfiability Testing. Springer, 244–257

    2009

  32. [41]

    He-Teng Zhang, Jie-Hong R Jiang, Luca Amarú, Alan Mishchenko, and Robert Brayton. 2021. Deep integration of circuit simulator and SAT solver. In2021 58th ACM/IEEE Design Automation Conference (DAC). IEEE, 877–882

    2021

  33. [42]

    He-Teng Zhang, Jie-Hong R Jiang, and Alan Mishchenko. 2021. A circuit-based SAT solver for logic synthesis. In2021 IEEE/ACM International Conference On Computer Aided Design (ICCAD). IEEE, 1–6

    2021

Pith tools

Reviewed July 9, 2026 · model on record in the stance chip above.