pith. sign in

arxiv: 2406.14190 · v5 · pith:OLRKQI3Snew · submitted 2024-06-20 · 💻 cs.LO

Extended Resolution Clause Learning via Dual Implication Points

Sam Buss , Jonathan Chung , Vijay Ganesh , Albert Oliveras This is my paper

Pith reviewed 2026-05-25 08:56 UTC · model grok-4.3

classification 💻 cs.LO
keywords SAT solvingextended resolutionclause learningdual implication pointsimplication graphCDCLTseitin formulasXOR formulas
0
0 comments X

The pith

A CDCL SAT solver learns stronger clauses by introducing variables for dual implication points in the implication graph.

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

The paper presents a new extended resolution clause learning algorithm for CDCL SAT solvers that dynamically adds variables as definitions for dual implication points detected in the implication graph at runtime. DIPs generalize unique implication points and are viewed as pairs of dominator nodes from the highest-level decision variable to the conflict. The method is implemented in xMapleLCM, which is compared experimentally to the baseline MapleLCM plus Kissat, CryptoMiniSat, SBVA+CaDiCaL, and GlucoseER. The authors report that xMapleLCM solves more instances on Tseitin and XORified formulas. A sympathetic reader cares because these formula classes remain difficult for standard clause-learning methods, and the DIP mechanism offers a concrete way to derive more powerful lemmas during search.

Core claim

Dual implication points allow a solver to introduce fresh variables that serve as definitions for pairs of dominators in the implication graph, thereby enabling extended resolution inferences that standard unit-propagation-based learning cannot produce; when this mechanism is added to MapleLCM the resulting solver outperforms the unmodified version and several other leading CDCL solvers on Tseitin and XORified formulas.

What carries the argument

Dual Implication Points (DIPs), a pair of dominator nodes from the decision variable at the highest decision level to the conflict node in the implication graph.

If this is right

  • xMapleLCM solves more Tseitin and XORified instances than MapleLCM, Kissat 3.1.1, CryptoMiniSat 5.11, and SBVA+CaDiCaL.
  • The DIP-based approach produces different clauses than the extended-resolution method used in GlucoseER.
  • The performance edge appears on formulas whose structure creates repeated dominator pairs in the implication graph.
  • New variables introduced for DIPs can be used both for clause learning and for subsequent propagation.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same DIP construction could be added to other base CDCL solvers besides MapleLCM.
  • Formulas with similar implication-graph structure outside the Tseitin and XORified classes might also benefit.
  • Combining DIP learning with other preprocessing or inprocessing techniques remains unexplored in the paper.

Load-bearing premise

The observed performance gains are produced by the DIP-based variable introduction rather than by other implementation differences, benchmark selection, or solver parameters.

What would settle it

Running xMapleLCM on the same Tseitin and XORified instances after the DIP variable-introduction code is disabled and finding that the modified solver solves no more instances than the original MapleLCM would falsify the claim.

read the original abstract

We present a new extended resolution clause learning (ERCL) algorithm, implemented as part of a conflict-driven clause-learning (CDCL) SAT solver, wherein new variables are dynamically introduced as definitions for {\it Dual Implication Points} (DIPs) in the implication graph constructed by the solver at runtime. DIPs are generalizations of unique implication points and can be informally viewed as a pair of dominator nodes, from the decision variable at the highest decision level to the conflict node, in an implication graph. We perform extensive experimental evaluation to establish the efficacy of our ERCL method, implemented as part of the MapleLCM SAT solver and dubbed xMapleLCM, against several leading solvers including the baseline MapleLCM, as well as CDCL solvers such as Kissat 3.1.1, CryptoMiniSat 5.11, and SBVA+CaDiCaL, the winner of SAT Competition 2023. We show that xMapleLCM outperforms these solvers on Tseitin and XORified formulas. We further compare xMapleLCM with GlucoseER, a system that implements extended resolution in a different way, and provide a detailed comparative analysis of their performance.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper proposes Dual Implication Points (DIPs) as a generalization of unique implication points in the implication graph of a CDCL SAT solver, enabling a new extended resolution clause learning (ERCL) scheme. The method is implemented in xMapleLCM (a modification of MapleLCM) and is claimed to outperform the baseline MapleLCM as well as Kissat 3.1.1, CryptoMiniSat 5.11, and SBVA+CaDiCaL on Tseitin and XORified formulas; a comparative analysis with GlucoseER is also provided.

Significance. If the performance advantage can be rigorously attributed to the DIP-based ERCL mechanism rather than ancillary implementation differences, the work would offer a concrete algorithmic advance for handling structured formulas with XOR or Tseitin structure, extending the practical reach of extended resolution within CDCL solvers.

major comments (2)
  1. [Experimental Evaluation] Experimental section: the central claim that xMapleLCM outperforms the listed solvers on Tseitin and XORified formulas is unsupported by any reported benchmark counts, instance selection criteria, runtime cutoffs, or statistical tests; without these, the empirical superiority cannot be verified or reproduced.
  2. [Implementation and Evaluation] Implementation and evaluation: xMapleLCM is presented as a modified MapleLCM incorporating DIP-ERCL, yet no ablation controls, parameter-matching details, or isolation of the DIP component from other solver changes are described; this leaves open whether observed gains are caused by the new mechanism.
minor comments (1)
  1. [DIP Definition] The informal definition of DIPs as 'a pair of dominator nodes' in the implication graph would benefit from a precise graph-theoretic formulation or pseudocode in the section introducing the concept.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the detailed review and the recommendation for major revision. The comments correctly identify areas where additional experimental details and controls would strengthen the presentation. We address each point below and will incorporate the requested information in the revised manuscript.

read point-by-point responses

  1. Referee: [Experimental Evaluation] Experimental section: the central claim that xMapleLCM outperforms the listed solvers on Tseitin and XORified formulas is unsupported by any reported benchmark counts, instance selection criteria, runtime cutoffs, or statistical tests; without these, the empirical superiority cannot be verified or reproduced.

    Authors: We agree that the experimental section requires explicit reporting of benchmark counts, instance selection criteria, runtime cutoffs, and statistical tests to allow verification. The current manuscript describes the benchmark families (Tseitin and XORified formulas) and compares against the listed solvers, but does not tabulate the precise instance counts or cutoff values used. In the revision we will add a new subsection in the experimental evaluation that lists the number of instances per family, their sources, the uniform runtime cutoff applied, and any statistical tests (e.g., Wilcoxon signed-rank) performed on the runtime distributions. revision: yes

  2. Referee: [Implementation and Evaluation] Implementation and evaluation: xMapleLCM is presented as a modified MapleLCM incorporating DIP-ERCL, yet no ablation controls, parameter-matching details, or isolation of the DIP component from other solver changes are described; this leaves open whether observed gains are caused by the new mechanism.

    Authors: The manuscript states that xMapleLCM is obtained by integrating the DIP-ERCL procedure into MapleLCM while retaining the solver's default parameter settings. However, we acknowledge that an explicit ablation isolating the DIP component and a clear statement of parameter equivalence are absent. In the revised version we will add an ablation table comparing MapleLCM with and without the DIP-ERCL module on the same benchmark set, and we will include a paragraph confirming that all other solver parameters were left at their MapleLCM defaults. revision: yes

Circularity Check

0 steps flagged

No circularity: algorithmic proposal evaluated against independent external solvers

full rationale

The paper introduces an ERCL algorithm based on DIPs in the implication graph and implements it in xMapleLCM, then reports direct runtime comparisons to unmodified MapleLCM plus unrelated solvers (Kissat, CryptoMiniSat, SBVA+CaDiCaL, GlucoseER) on Tseitin/XORified instances. No equations, fitted parameters, or self-referential definitions appear; the central efficacy claim rests on external benchmark outcomes rather than any reduction of results to the method's own inputs by construction. Self-citations, if present, are not load-bearing for the performance attribution.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The approach rests on standard CDCL implication graph properties and introduces DIPs as a new definitional device without fitted parameters or external evidence for the new entity.

axioms (2)
  • domain assumption CDCL solvers maintain implication graphs with decision levels and conflict nodes
    Invoked as the foundation for identifying DIPs during conflict analysis.
  • standard math Unique implication points are well-defined dominators in implication graphs
    Used as the baseline that DIPs generalize.
invented entities (1)
  • Dual Implication Points (DIPs) no independent evidence
    purpose: To identify pairs of dominators for introducing new variables as definitions in extended resolution clause learning
    New concept defined in the paper to enable the ERCL algorithm.

pith-pipeline@v0.9.0 · 5742 in / 1237 out tokens · 43574 ms · 2026-05-25T08:56:50.724417+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

40 extracted references · 40 canonical work pages

  1. [1]

    Clause-learning algorithms with many restarts and bounded-width resolution

    Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. Journal of Artificial Intelligence Research , 40:353 --373, January 2011. Preliminary version in SAT '09

    work page 2011

  2. [2]

    Clause-learning algorithms with many restarts and bounded-width resolution

    Albert Atserias, Johannes Klaus Fichte, and Marc Thurley. Clause-learning algorithms with many restarts and bounded-width resolution. J. Artif. Intell. Res. , 40:353--373, 2011. https://doi.org/10.1613/jair.3152 doi:10.1613/jair.3152

    work page doi:10.1613/jair.3152 2011

  3. [3]

    A restriction of extended resolution for clause learning sat solvers

    Gilles Audemard, George Katsirelos, and Laurent Simon. A restriction of extended resolution for clause learning sat solvers. In AAAI , 2010

    work page 2010

  4. [4]

    Predicting learnt clauses quality in modern SAT solvers

    Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Craig Boutilier, editor, IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11-17, 2009 , pages 399--404, 2009. URL: http://ijcai.org/Proceedings/09/Papers/074.pdf

    work page 2009

  5. [5]

    Enhancing D avis P utnam with extended binary clause learning

    Fahiem Bacchus. Enhancing D avis P utnam with extended binary clause learning. In Proc. 18th Annual Conference on Artificial Intelligence and 15th Conference on Innovative Applications of Artificial Intelligence , pages 613--619. AAAI Press and MIT Press, 2002

    work page 2002

  6. [6]

    Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions

    Tomas Balyo, Marijn Heule, Markus Iser, Matti J \"a rvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions . Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2023

    work page 2023

  7. [7]

    Size space tradeoffs for resolution

    Eli Ben-Sasson. Size space tradeoffs for resolution. SIAM Journal on Computing , 38(6):2511--2525, 2009

    work page 2009

  8. [8]

    CaDiCaL , Kissat , Paracooba , Plingeling and Treengeling entering the SAT Competition 2020

    Armin Biere, Katalin Fazekas, Mathias Fleury, and Maximillian Heisinger. CaDiCaL , Kissat , Paracooba , Plingeling and Treengeling entering the SAT Competition 2020 . In Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti J \"a rvisalo, and Martin Suda, editors, Proc. of SAT Competition 2020 -- Solver and Benchmark Descriptions , volume B-2020-1 ...

    work page 2020

  9. [9]

    CadiBack : Extracting backbones with CaDiCal

    Armin Biere, Nils Froleyks, and Wenzi Wang. CadiBack : Extracting backbones with CaDiCal . In Proc. 26th Intl. Conf. on Theory and Applications of Satisfiability Testing SAT , pages 3:1--12. Leibniz-Zentrum f \" u r Informatik, 2023

    work page 2023

  10. [10]

    Bryant and Marijn J

    Randal E. Bryant and Marijn J. H. Heule. Generating extended resolution proofs with a bdd-based SAT solver. ACM Trans. Comput. Log. , 24(4):31:1--31:28, 2023. https://doi.org/10.1145/3595295 doi:10.1145/3595295

    work page doi:10.1145/3595295 2023

  11. [11]

    A linear time algorithm for two-vertex bottlenecks

    Sam Buss, Vijay Ganesh, and Albert Oliveras. A linear time algorithm for two-vertex bottlenecks. In preparation. Preliminary version available at https://math.ucsd.edu/ sbuss/ResearchWeb/TwoVertBottlenecks, March 2024

    work page 2024

  12. [12]

    Dual depth first search for binary clause reasoning

    Sam Buss, Oliver Kullmann, and Virginia Vassilevska Williams. Dual depth first search for binary clause reasoning. Preliminary version, March 2024

    work page 2024

  13. [13]

    Stephen A. Cook. A short proof of the pigeon hole principle using extended resolution. SIGACT News , 8(4):28--32, 1976. https://doi.org/10.1145/1008335.1008338 doi:10.1145/1008335.1008338

    work page doi:10.1145/1008335.1008338 1976

  14. [14]

    Andrew Haberlandt, Harrison Green, and Marijn J. H. Heule. Effective auxiliary variables via structured reencoding. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy , volume 271 of LIPIcs , pages 11:1--11:19. Schloss Dagstuhl - Le...

    work page doi:10.4230/lipics.sat.2023.11 2023

  15. [15]

    The intractability of resolution

    Armin Haken. The intractability of resolution. Theoretical computer science , 39:297--308, 1985

    work page 1985

  16. [16]

    Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Short proofs without new variables. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings , volume 10395 of Lecture Notes in Computer Science , pages 130--147. Springer, 2017. https://doi.org...

    work page doi:10.1007/978-3-319-63046-5 2017

  17. [17]

    Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Encoding redundancy for satisfaction-driven clause learning. In Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference (TACAS 2019), Part I , Lecture Notes in Computer Science 11427, pages 41--58. Springer Verlag, 2019

    work page 2019

  18. [18]

    Marijn J. H. Heule, Benjamin Kiesl, and Armin Biere. Strong extension-free proof systems. J. Autom. Reason. , 64(3):533--554, 2020. https://doi.org/10.1007/s10817-019-09516-0 doi:10.1007/s10817-019-09516-0

    work page doi:10.1007/s10817-019-09516-0 2020

  19. [19]

    Marijn J. H. Heule, Benjamin Kiesl, Martina Seidl, and Armin Biere. Pruning through satisfaction. In Ofer Strichman and Rachel Tzoref - Brill, editors, Hardware and Software: Verification and Testing - 13th International Haifa Verification Conference, HVC 2017, Haifa, Israel, November 13-15, 2017, Proceedings , volume 10629 of Lecture Notes in Computer Sc...

    work page doi:10.1007/978-3-319-70389-3 2017

  20. [20]

    A problem meta-data library for research in sat

    Markus Iser and Carsten Sinz. A problem meta-data library for research in sat. In Daniel Le Berre and Matti J "arvisalo, editors, Proceedings of Pragmatics of SAT 2015 and 2018 , volume 59 of EPiC Series in Computing , pages 144--152. EasyChair, 2019. URL: https://easychair.org/publications/paper/jQXv, https://doi.org/10.29007/gdbb doi:10.29007/gdbb

    work page doi:10.29007/gdbb 2015

  21. [21]

    Henry A. Kautz. Deconstructing planning as satisfiability. In Proceedings, The Twenty-First National Conference on Artificial Intelligence and the Eighteenth Innovative Applications of Artificial Intelligence Conference, July 16-20, 2006, Boston, Massachusetts, USA , pages 1524--1526. AAAI Press, 2006. URL: http://www.aaai.org/Library/AAAI/2006/aaai06-241.php

    work page 2006

  22. [22]

    Kautz and Bart Selman

    Henry A. Kautz and Bart Selman. Planning as satisfiability. In Bernd Neumann, editor, 10th European Conference on Artificial Intelligence, ECAI 92, Vienna, Austria, August 3-7, 1992. Proceedings , pages 359--363. John Wiley and Sons, 1992

    work page 1992

  23. [23]

    Software verification

    Daniel Kroening. Software verification. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications , pages 791--818. IOS Press, 2021. https://doi.org/10.3233/FAIA201004 doi:10.3233/FAIA201004

    work page doi:10.3233/faia201004 2021

  24. [24]

    Cnfgen: A generator of crafted benchmarks

    Massimo Lauria, Jan Elffers, Jakob Nordstr \" o m, and Marc Vinyals. Cnfgen: A generator of crafted benchmarks. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing - SAT 2017 - 20th International Conference, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings , volume 10491 of Lecture Notes in Comp...

    work page doi:10.1007/978-3-319-66263-3 2017

  25. [25]

    An effective learnt clause minimization approach for CDCL SAT solvers

    Mao Luo, Chu - Min Li, Fan Xiao, Felip Many \` a , and Zhipeng L \" u . An effective learnt clause minimization approach for CDCL SAT solvers. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, Melbourne, Australia, August 19-25, 2017 , pages 703--711. ijcai.org, 2017. URL: http...

    work page doi:10.24963/ijcai.2017/98 2017

  26. [26]

    Automated reencoding of boolean formulas

    Norbert Manthey, Marijn Heule, and Armin Biere. Automated reencoding of boolean formulas. In Armin Biere, Amir Nahir, and Tanja E. J. Vos, editors, Hardware and Software: Verification and Testing - 8th International Haifa Verification Conference, HVC 2012, Haifa, Israel, November 6-8, 2012. Revised Selected Papers , volume 7857 of Lecture Notes in Compute...

    work page doi:10.1007/978-3-642-39611-3 2012

  27. [27]

    Conflict-driven clause learning SAT solvers

    Jo \ a o Marques - Silva, In \^ e s Lynce, and Sharad Malik. Conflict-driven clause learning SAT solvers. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications , pages 133--182. IOS Press, 2021. https://doi.org/10.3233/FAIA20...

    work page doi:10.3233/faia200987 2021

  28. [28]

    Zur algemeinen K urventheorie

    Karl Menger. Zur algemeinen K urventheorie. Fundamenta Mathematicae , 10:96--115, 1927

    work page 1927

  29. [29]

    Backing backtracking

    Sibyle M \"o hle and Armin Biere. Backing backtracking. In 22nd Intl Conf. on Theory and Applications of Satisfiability Testing (SAT) , Lecture Notes in Computer Science 11628, pages 250--266. Springer, 2019

    work page 2019

  30. [30]

    Chronological backtracking

    Alexander Nadel and Vadim Ryvchin. Chronological backtracking. In 21nd Intl Conf. on Theory and Applications of Satisfiability Testing (SAT) , Lecture Notes in Computer Science 10929, pages 111--121. Springer, 2018

    work page 2018

  31. [31]

    Learning shorter redundant clauses in SDCL using maxsat

    Albert Oliveras, Chunxiao Li, Darryl Wu, Jonathan Chung, and Vijay Ganesh. Learning shorter redundant clauses in SDCL using maxsat. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing, SAT 2023, July 4-8, 2023, Alghero, Italy , volume 271 of LIPIcs , pages 18:1--18:17. Schlo...

    work page doi:10.4230/lipics.sat.2023.18 2023

  32. [32]

    On modern clause-learning satisfiability solvers

    Knot Pipatsrisawat and Adnan Darwiche. On modern clause-learning satisfiability solvers. Journal of Automated Reasoning , 44(3):277--301, 2010

    work page 2010

  33. [33]

    On the power of clause-learning SAT solvers as resolution engines

    Knot Pipatsrisawat and Adnan Darwiche. On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. , 175(2):512--525, 2011. https://doi.org/10.1016/j.artint.2010.10.002 doi:10.1016/j.artint.2010.10.002

    work page doi:10.1016/j.artint.2010.10.002 2011

  34. [34]

    Reeves, Marijn J

    Joseph E. Reeves, Marijn J. H. Heule, and Randal E. Bryant. Preprocessing of propagation redundant clauses. In Jasmin Blanchette, Laura Kov \' a cs, and Dirk Pattinson, editors, Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings , volume 13385 of Lecture Notes in Computer Science , pages 10...

    work page doi:10.1007/978-3-031-10769-6 2022

  35. [35]

    Sakallah

    Karem A. Sakallah. Symmetry and satisfiability. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition , volume 336 of Frontiers in Artificial Intelligence and Applications , pages 509--570. IOS Press, 2021. https://doi.org/10.3233/FAIA200996 doi:10.3233/FAIA200996

    work page doi:10.3233/faia200996 2021

  36. [36]

    Extending SAT solvers to cryptographic problems

    Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings , volume 5584 of Lecture Notes in Computer Science , pages 244--257. Springer,...

    work page doi:10.1007/978-3-642-02777-2 2009

  37. [37]

    On the complexity of derivation in propositional calculus

    Grigori S Tseitin. On the complexity of derivation in propositional calculus. Automation of reasoning: 2: Classical papers on computational logic 1967--1970 , pages 466--483, 1983

    work page 1967

  38. [38]

    Hard examples for resolution

    Alasdair Urquhart. Hard examples for resolution. J. ACM , 34(1):209--219, 1987. https://doi.org/10.1145/7531.8928 doi:10.1145/7531.8928

    work page doi:10.1145/7531.8928 1987

  39. [39]

    Saturn: A SAT-Based Tool for Bug Detection

    Yichen Xie and Alexander Aiken. Saturn: A SAT-Based Tool for Bug Detection . In Proceedings of the 17th International Conference on Computer Aided Verification, CAV 2005 , pages 139--143, 2005. https://doi.org/10.1007/11513988\_13 doi:10.1007/11513988\_13

    work page doi:10.1007/11513988 2005

  40. [40]

    Madigan, Matthew W

    Lintao Zhang, Conor F. Madigan, Matthew W. Moskewicz, and Sharad Malik. Efficient conflict driven learning in boolean satisfiability solver. In Rolf Ernst, editor, Proceedings of the 2001 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2001, San Jose, CA, USA, November 4-8, 2001 , pages 279--285. IEEE Computer Society, 2001. https://doi....

    work page doi:10.1109/iccad.2001.968634 2001