pith. sign in

arxiv: 1906.10357 · v2 · pith:D7FOHQE3new · submitted 2019-06-25 · 💻 cs.LO

Partial Quantifier Elimination With Learning

Eugene Goldberg This is my paper

Pith reviewed 2026-05-25 16:34 UTC · model grok-4.3

classification 💻 cs.LO
keywords partial quantifier eliminationD-sequentsquantified CNFredundancy proofsverificationSAT solversclause learning
0
0 comments X

The pith

A new partial quantifier elimination algorithm learns and reuses D-sequents while proving clauses redundant one by one.

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

The paper addresses partial quantifier elimination, where only a small portion of a formula is removed from quantifier scope, as many verification tasks reduce to this easier subproblem. It builds on prior work using D-sequents, which record that a clause is redundant in a quantified CNF formula inside a given subspace. The new algorithm incorporates learning and safe reuse of these D-sequents and processes target clauses individually, backtracking immediately once redundancy is established for the current one. This design mirrors SAT-solver behavior of early termination on a single falsified clause. Experiments demonstrate that the updated method runs faster than the version without reuse or early backtracking.

Core claim

The paper presents a PQE algorithm based on a revised definition of D-sequents that supports learning and reuse without losing correctness of redundancy proofs; the algorithm proves clauses redundant individually and backtracks as soon as the current target clause is shown redundant in the current subspace, and this version outperforms its predecessor in experiments.

What carries the argument

D-sequents, records stating that a clause is redundant in a quantified CNF formula in a specified subspace, now defined to permit safe reuse across steps.

If this is right

  • The algorithm can learn D-sequents on the fly and reuse them in later steps.
  • It proves target clauses redundant one at a time and backtracks immediately upon success.
  • This produces behavior similar to a SAT-solver that terminates upon falsifying any single clause.
  • The resulting procedure outperforms the earlier PQE algorithm without reuse on experimental instances.

Where Pith is reading between the lines

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

  • The early-backtracking design could be ported to other structural-reasoning tasks that currently process all clauses before pruning.
  • Safe reuse of redundancy records might extend to quantified Boolean formula solvers that face similar structural rather than purely semantic constraints.

Load-bearing premise

The modified definition of D-sequents enables their safe reusing in the new algorithm without compromising correctness of the redundancy proofs.

What would settle it

A benchmark instance from equivalence checking or model checking where the new algorithm returns an incorrect result traceable to reuse of a D-sequent would falsify the central claim.

Figures

Figures reproduced from arXiv: 1906.10357 by Eugene Goldberg.

Figure 1
Figure 1. Figure 1: Main loop The main loop of DS-PQE + is shown in [PITH_FULL_IMAGE:figures/full_fig_p006_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The PrvRed procedure The operation of PrvRed in the while loop can be par￾titioned into three parts iden￾tified by dotted lines. The first part (lines 5-10) starts with checking if the assign￾ment queue Q is empty. If so, a new assignment v = b is picked (line 6) where v ∈ (X ∪ Y ) and b ∈ {0, 1} and added to Q. PrvRed first assigns7 the variables of Y . So v ∈ X, only if all variables of Y are as￾signed. … view at source ↗
Figure 2
Figure 2. Figure 2: ) In the first part (lines 2-9), BCP extracts an assignment w = b from the assignment queue Q (line 2). It can be a decision assignment or one derived from a clause C or D￾sequent S. Then, BCP updates the current assignment ~a (line 9). Lines 3-8 are explained in Subsection XII-B. BCP(η k ξ) { 1 while (Q 6= ∅) { 2 (w, b, C, S) := Pop(Q k ) 3* if (C = Ctrg ) { 4* C ′ := BCP∗ (η k ξ, w, b) 5* Ctrg := NewTrg(… view at source ↗
Figure 3
Figure 3. Figure 3: The BCP procedure In the second part (lines 10-17), BCP first checks if the current target clause Ctrg is satisfied by w = b. If so, BCP terminates return￾ing the backtracking condi￾tion SatTrg (line 11). Then BCP identifies the clauses of F1∧F2 satisfied or con￾strained by w = b (line 12). If a clause becomes unit, BCP stores the assignment derived from this clause in Q. If a falsified clause C ′ is found… view at source ↗
read the original abstract

We consider a modification of the Quantifier Elimination (QE) problem called Partial QE (PQE). In PQE, only a small part of the formula is taken out of the scope of quantifiers. The appeal of PQE is that many verification problems, e.g. equivalence checking and model checking, reduce to PQE and the latter is much easier than complete QE. Earlier, we introduced a PQE algorithm based on the machinery of D-sequents. A D-sequent is a record stating that a clause is redundant in a quantified CNF formula in a specified subspace. To make this algorithm efficient, it is important to reuse learned D-sequents. However, reusing D-sequents is not as easy as conflict clauses in SAT-solvers because redundancy is a structural rather than a semantic property. Earlier, we modified the definition of D-sequents to enable their safe reusing. In this paper, we present a PQE algorithm based on new D-sequents. It is different from its predecessor in two aspects. First, the new algorithm can learn and reuse D-sequents. Second, it proves clauses redundant one by one and thus backtracks as soon as the current target clause is proved redundant in the current subspace. This makes the new PQE algorithm similar to a SAT-solver that backtracks as soon as just one clause is falsified. We show experimentally that the new PQE algorithm outperforms its predecessor.

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 presents a new algorithm for Partial Quantifier Elimination (PQE) that modifies the definition of D-sequents to support safe learning and reuse, alters the backtracking strategy to prove redundancy of one clause at a time (similar to SAT-solver conflict handling), and reports experimental results showing outperformance over the predecessor algorithm based on earlier D-sequent machinery.

Significance. If the correctness of the modified D-sequents and the experimental outperformance hold, the work strengthens the applicability of PQE to verification tasks such as equivalence and model checking by adding learning capabilities without compromising redundancy proofs.

major comments (2)
  1. [Experimental evaluation section] The central experimental claim of outperformance (abstract) is load-bearing but the manuscript provides no details on experimental setup, baselines, benchmarks, or statistical handling; this prevents assessment of whether the result supports the algorithmic changes.
  2. [Section on new D-sequents and algorithm] The claim that the modified D-sequent definition enables safe reuse without compromising correctness (abstract and introduction) is a key assumption for the new algorithm; no explicit proof or argument is referenced for why the structural redundancy property is preserved under the new backtracking.
minor comments (1)
  1. The abstract could more clearly distinguish the two algorithmic changes (learning vs. one-by-one backtracking) and their individual contributions to performance.

Simulated Author's Rebuttal

2 responses · 0 unresolved

Thank you for reviewing our manuscript. We address each major comment below and will revise the manuscript accordingly.

read point-by-point responses

  1. Referee: [Experimental evaluation section] The central experimental claim of outperformance (abstract) is load-bearing but the manuscript provides no details on experimental setup, baselines, benchmarks, or statistical handling; this prevents assessment of whether the result supports the algorithmic changes.

    Authors: We agree that the experimental section requires additional details to support the outperformance claim. In the revised manuscript we will expand this section with a full description of the experimental setup, the benchmarks employed, the baseline algorithms, and any statistical handling used. revision: yes

  2. Referee: [Section on new D-sequents and algorithm] The claim that the modified D-sequent definition enables safe reuse without compromising correctness (abstract and introduction) is a key assumption for the new algorithm; no explicit proof or argument is referenced for why the structural redundancy property is preserved under the new backtracking.

    Authors: The modified D-sequent definition that enables safe reuse was introduced in our prior work. The new backtracking strategy (proving one clause redundant at a time) preserves the structural redundancy property because learned D-sequents remain valid in their associated subspaces; the change affects only the order of redundancy proofs and does not invalidate subspace-specific sequents. We will add an explicit clarifying argument in the revised algorithm section, with a reference to the prior work. revision: yes

Circularity Check

0 steps flagged

Minor self-citation of prior D-sequent work; central experimental claim remains independent

full rationale

The paper describes an algorithmic modification to prior D-sequent machinery (by the same author) to enable learning/reuse and altered backtracking, then reports experimental outperformance. No derivation step reduces a claimed result to a fitted parameter, self-defined quantity, or unverified self-citation chain; the experimental comparison is presented as an independent evaluation of the new procedure against its predecessor. This matches the expected non-circular case for an algorithmic paper whose core contribution is empirical.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Based on the abstract, the work relies on standard assumptions from logic and prior D-sequent definitions with modifications; no free parameters, new axioms, or invented entities are introduced.

axioms (1)
  • domain assumption D-sequents can be redefined to support safe reuse across subspaces
    The abstract states that the definition was modified to enable safe reusing.

pith-pipeline@v0.9.0 · 5776 in / 1055 out tokens · 37681 ms · 2026-05-25T16:34:02.520584+00:00 · methodology

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

37 extracted references · 37 canonical work pages · 3 internal anchors

  1. [1]

    Abramovici, M

    M. Abramovici, M. Breuer, and A. Friedman. Digital Systems Testing and Testable Design . John Wiley & Sons, 1994

    work page 1994

  2. [2]

    Aloul, K

    F. Aloul, K. Sakallah, and I. Markov. Efficient symmetry b reaking for boolean satisfiability. IEEE Transactions on Computers , 55(5):549–558, May 2006

    work page 2006

  3. [3]

    Biere, A

    A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y . Zhu. Sym bolic model checking using sat procedures instead of bdds. In DAC, pages 317–320, 1999

    work page 1999

  4. [4]

    Biere, F

    A. Biere, F. Lonsing, and M. Seidl. Blocked clause elimin ation for qbf. CADE-11, pages 101–115, 2011

    work page 2011

  5. [5]

    Bjorner and M

    N. Bjorner and M. Janota. Playing with quantified satisfa ction. In LPAR, 2015

    work page 2015

  6. [6]

    Bjorner, M

    N. Bjorner, M. Janota, and W. Klieber. On conflicts and str ategies in qbf. In LPAR, 2015

    work page 2015

  7. [7]

    A. R. Bradley. Sat-based model checking without unrolli ng. In VMCAI, pages 70–87, 2011

    work page 2011

  8. [8]

    Brauer, A

    J. Brauer, A. King, and J. Kriener. Existential quantific ation as incremental sat. CA V -11, pages 191–207, 2011

    work page 2011

  9. [9]

    R. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers , C-35(8):677–691, August 1986

    work page 1986

  10. [10]

    Chauhan, E

    P . Chauhan, E. Clarke, S. Jha, J.H. Kukula, H. V eith, and D. Wang. Using combinatorial optimization methods for quantificati on scheduling. CHARME-01, pages 293–309, 2001

    work page 2001

  11. [11]

    Chockler, A

    H. Chockler, A. Ivrii, A. Matsliah, S. Moran, and Z. Nevo . Incremental formal verification of hardware. In FMCAD-11, pages 135–143, 2011

    work page 2011

  12. [12]

    Crawford, M

    J. Crawford, M. Ginsberg, E. Luks, and A. Roy. Symmetry- breaking predicates for search problems. In Int. Conf. on Principles of Knowledge Representation and Reasoning , pages 148–159, 1996

    work page 1996

  13. [13]

    Davis, G

    M. Davis, G. Logemann, and D. Loveland. A machine progra m for theorem proving. Communications of the ACM , 5(7):394–397, July 1962

    work page 1962

  14. [14]

    Devriendt, B

    J. Devriendt, B. Bogaerts, M. Bruynooghe, and M. Deneck er. Improved static symmetry breaking for sat. In SAT, 2016

    work page 2016

  15. [15]

    E´ en and A

    N. E´ en and A. Biere. Effective preprocessing in sat thr ough variable and clause elimination. In SAT, pages 61–75, 2005

    work page 2005

  16. [16]

    E´ en and N

    N. E´ en and N. S¨ orensson. An extensible sat-solver. In SAT, pages 502–518, Santa Margherita Ligure, Italy, 2003

    work page 2003

  17. [17]

    Ganai, A.Gupta, and P .Ashar

    M. Ganai, A.Gupta, and P .Ashar. Efficient sat-based unb ounded sym- bolic model checking using circuit cofactoring. ICCAD-04, pages 510– 517, 2004

    work page 2004

  18. [18]

    Equivalence Checking By Logic Relaxation

    E. Goldberg. Equivalence checking by logic relaxation . Technical Report arXiv:1511.01368 [cs.LO], 2015

    work page internal anchor Pith review Pith/arXiv arXiv 2015

  19. [19]

    Goldberg

    E. Goldberg. Equivalence checking by logic relaxation . In FMCAD-16, pages 49–56, 2016

    work page 2016

  20. [20]

    Goldberg

    E. Goldberg. Property checking without invariant gene ration. Technical Report arXiv:1602.05829 [cs.LO], 2016

    work page arXiv 2016

  21. [21]

    Quantifier Elimination With Structural Learning

    E. Goldberg. Quantifier elimination with structural le arning. Technical Report arXiv: 1810.00160 [cs.LO], 2018

    work page internal anchor Pith review Pith/arXiv arXiv 2018

  22. [22]

    Goldberg and P

    E. Goldberg and P . Manolios. Quantifier elimination by d ependency sequents. In FMCAD-12, pages 34–44, 2012

    work page 2012

  23. [23]

    Removal of Quantifiers by Elimination of Boundary Points

    E. Goldberg and P . Manolios. Removal of quantifiers by el imination of boundary points. Technical Report arXiv:1204.1746 [cs.LO ], 2012

    work page internal anchor Pith review Pith/arXiv arXiv 2012

  24. [24]

    Goldberg and P

    E. Goldberg and P . Manolios. Quantifier elimination via clause redun- dancy. In FMCAD-13, pages 85–92, 2013

    work page 2013

  25. [25]

    Goldberg and P

    E. Goldberg and P . Manolios. Partial quantifier elimina tion. In Proc. of HVC-14, pages 148–164. Springer-V erlag, 2014

    work page 2014

  26. [26]

    Goldberg and P

    E. Goldberg and P . Manolios. Software for quantifier eli mination in propositional logic. In ICMS-2014,Seoul, South Korea, August 5-9, pages 291–294, 2014

    work page 2014

  27. [27]

    J¨ arvisalo, M

    M. J¨ arvisalo, M. Heule, and A. Biere. Inprocessing rul es. IJCAR-12, pages 355–370, 2012

    work page 2012

  28. [28]

    J. Jiang. Quantifier elimination via functional compos ition. In Pro- ceedings of the 21st International Conference on Computer A ided V erification, CA V -09, pages 383–397, 2009

    work page 2009

  29. [29]

    Jin and F.Somenzi

    H. Jin and F.Somenzi. Prime clauses for fast enumeratio n of satisfying assignments to boolean circuits. DAC-05, pages 750–753, 20 05

    work page

  30. [30]

    Klieber, M

    W. Klieber, M. Janota, J.Marques-Silva, and E. Clarke. Solving qbf with free variables. In CP, pages 415–431, 2013

    work page 2013

  31. [31]

    Kullmann

    O. Kullmann. New methods for 3-sat decision and worst-c ase analysis. Theor . Comput. Sci., 223(1-2):1–72, 1999

    work page 1999

  32. [32]

    Larrabee

    T. Larrabee. Test pattern generation using boolean sat isfiability. IEEE Trans. on Comp.-Aided Design of Integr . Circuits and System s, 11(1):4– 15, Jan 1992

    work page 1992

  33. [33]

    Marques-Silva and K

    J. Marques-Silva and K. Sakallah. Grasp – a new search al gorithm for satisfiability. In ICCAD-96, pages 220–227, 1996

    work page 1996

  34. [34]

    McMillan

    K. McMillan. Applying sat methods in unbounded symboli c model checking. In Proc. of CA V-02, pages 250–264. Springer-V erlag, 2002

    work page 2002

  35. [35]

    McMillan

    K. McMillan. Interpolation and sat-based model checki ng. In CA V-03, pages 1–13. Springer, 2003

    work page 2003

  36. [36]

    Moskewicz, C

    M. Moskewicz, C. Madigan, Y . Zhao, L. Zhang, and S. Malik . Chaff: engineering an efficient sat solver. In DAC-01, pages 530–535, New Y ork, NY , USA, 2001

    work page 2001

  37. [37]

    starting clause

    E. Niklas, A. Mishchenko, and R. Brayton. Efficient impl ementation of property directed reachability. In FMCAD-11, pages 125–134, 2011. APPENDIX I REDUNDANCY OF A CLAUSE IN A SUBSPACE In this appendix, we discuss the following problem. Let ∃X[F ] be an ∃CNF formula. Let C be an X-clause of F redundant in ∃X[F ] in subspace ⃗ q. Let ⃗ rbe an assignment to ...

    work page 2011