Pith. sign in

REVIEW 4 major objections 6 minor 28 references

Learned Clause Minimization in Parallel SAT Solvers

T0 review · 4 major / 6 minor · reviewed 2026-08-14 · deepseek-v4-flash

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

Pith's one-line read Most parallel SAT solvers slow down when learned-clause minimization is added, and only targeted variants help.

desk verdict Useful empirical study of clause minimization in parallel SAT solvers, but the positive conclusions are too strong for the small, unreplicated effect sizes. read the letter →

arxiv 1908.01624 v1 pith:7BYSWDW2 submitted 2019-08-05 cs.DS cs.LO

Marc Hartung , Florian Schintke This is my paper · ORCID
classification cs.DScs.LO
keywords learnedclauseminimizationvivificationparallelSATsolvingportfoliosolverssharingLBDunsatisfiableinstancesGlucose-Syrup
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

This paper tries to settle whether learned clause minimization (LCM), a technique that shortens learned clauses by vivification and clearly helps sequential SAT solvers, should be carried over to parallel portfolio solvers that exchange clauses between threads. Based on implementations in a Glucose-Syrup baseline and comparisons with two other vivification-based solvers, the authors argue that the transfer is not automatic: LCM improves the overall number of solved instances only when it is applied to clauses a solver learned itself (PCM), while vivifying exported clauses pays off mainly on unsatisfiable instances and only with a tight LBD cutoff. The headline result is negative for naive adoption: on most instances LCM decreases parallel solver performance, and the gains come from a minority of problems where the shortened clauses are actually reused. The paper matters because parallel SAT solvers are the practical route to hard industrial instances, and this work identifies which minimization choices preserve or reverse the sequential benefit.

What carries the argument

The load-bearing object is clause vivification: for a learned clause, negate each literal and propagate; a conflict yields a replacement clause, and literals propagated to false can be removed. What carries the argument is the placement of vivification in the shared-clause pipeline (private clauses only, linked private clauses, or delayed export) together with the literal block distance (LBD), the number of decision levels spanned by a clause's literals, which is used to select clauses worth vivifying. The paper's ECM approaches use LBD as the cutoff (below 4 works, below 5 over-minimizes), while PCM and LPCM sort by LBD and activity and vivify roughly the half with LBD at most 5. The supporting mechanism is that vivified clauses only pay off when they are used again: the paper cites statistics that most learned clauses participate in only one conflict and that only about 10% of imported clauses lead to conflicts in the importing solver, which explains why over-vivifying exported clauses is mostly wasted work.

What would settle it

Repeat the same 1,050-benchmark comparison on a different many-core system, or with several randomized repetitions on the same system, and check whether PCM still beats the baseline by 18 instances and whether ECM3 still gains 20 unsatisfiable instances; if the signs of those differences flip, the claimed generalization fails.

Watch

Extended reading notes

Core claim

The central discovery is that where and when clause vivification happens determines whether learned clause minimization helps a parallel portfolio solver. The authors define three homogeneous variants: PCM vivifies only clauses learned by the same thread and never re-shares the improvement; LPCM adds a link so strengthened clauses can be shared; ECM delays export until after vivification, using an LBD cutoff to limit which clauses are processed. Across 1,050 benchmarks from SAT Competitions 2016 to 2018 with a 15,000-second limit, PCM solves 698 instances versus 680 for the baseline, ECM with an LBD below 4 solves 693 and adds 20 unsatisfiable instances while losing 7 satisfiable ones, and ECM with an LBD below 5 solves only 623. The ECM variant of TopoSAT2 also lowers its performance when enabled. The authors conclude that LCM boosts parallel solvers only on a fraction of instances, that shortening a solver's own high-activity clauses is the reliable route, and that vivifying exported clauses helps mostly for unsatisfiable problems when kept to clauses with small LBD.

Load-bearing premise

The overall conclusions depend on the three SAT Competition benchmark families and the single 34-thread Xeon Phi configuration with a 15,000-second limit being representative; several decisive differences are only a handful of solved instances, so run-to-run or benchmark-selection variation could change them.

Editorial extensions

If this is right

  • Vivifying only a solver's own learned clauses (PCM) is the reliable default: it solves 18 more instances overall than the baseline without requiring linked-clause machinery.
  • ECM with an LBD cutoff below 4 is a targeted unsatisfiable-instance strategy: it solves 20 more unsatisfiable instances than the baseline while solving 7 fewer satisfiable ones.
  • Over-minimizing exported clauses is counterproductive: raising the ECM cutoff to LBD below 5 drops the total from 693 to 623, below the baseline.
  • The sharing mechanism itself changes the benefit: Sticky, which uses physical clause sharing, gains about 20 instances from LPCM and ECM3, while the linked-sharing variant in Syrup gains less.

Reading between the lines

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

  • Not a paper claim: because PCM (no sharing of improvements) solves more SAT instances than LPCM (linked sharing), the overhead of publishing clause updates may cancel the benefit; a batched or lazy update scheme is a natural next test.
  • Not a paper claim: if only about 10% of imported clauses ever participate in conflicts, an import-time filter that predicts which clauses will be reused could let ECM spend its vivification budget only on high-yield exports.
  • Not a paper claim: all comparisons ran on one shared-memory 34-thread node, so on distributed-memory clusters where clause exchange is far more expensive, the balance between ECM's delayed export and PCM's local minimization could shift and change the ranking.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 6 minor

Summary. The paper studies whether learned clause minimization (LCM) via clause vivification helps parallel portfolio SAT solvers. It defines three homogeneous LCM approaches: private clause minimization (PCM) on locally learned clauses, linked PCM (LPCM) that shares improved clauses through references, and export clause minimization (ECM) that vivifies clauses before export. The approaches are implemented in Glucose-Syrup 4.0 and compared with the vivification-based solvers TopoSAT2 and Sticky on 1,050 SAT Competition benchmarks from 2016, 2017, and 2018, using 34 threads on a Xeon Phi with a 15,000-second time limit. The main empirical conclusions are that PCM increases the number of solved instances overall, that ECM with a low LBD threshold improves performance on unsatisfiable instances, and that applying LCM more broadly often decreases performance.

Significance. If the empirical claims withstand scrutiny, the paper makes a useful contribution: it fills a gap in the evaluation of homogeneous LCM in parallel SAT solvers, provides open-source implementations (the Syrup extensions and Sticky), and offers plausible explanations for the observed differences, such as vivification propagation overhead and the low reuse of imported clauses. The robust negative result for Syrup-ECM4 and the inconsistent cross-solver effects are also informative. However, the positive effects are small, are based on unreplicated runs, and are partly contradicted across solvers, so the significance of the paper depends on additional statistical validation or a clearly more cautious framing.

major comments (4)
  1. [Section 4.2, Table 1] The central positive conclusions rest on small, unreplicated differences. Syrup-PCM solves 698 vs. 680 instances (+18 of 1,050), with the gain concentrated in SAT'18 (+15) and no gain in SAT'17; Syrup-ECM3 solves 13 more overall but 7 fewer SAT and 20 more UNSAT, while the UNSAT effect reverses for TopoSAT2-ECM3 (−18 UNSAT vs. TopoSAT2) and Sticky-ECM3 (+26 UNSAT vs. Sticky). No confidence intervals, repeated runs, or paired tests are reported. On a 34-thread portfolio with dynamic restarts and lazy clause sharing, differences of a few instances can easily be run-to-run noise. The conclusion that "PCM leads to more solved instances in general" therefore needs statistical support or a clear statement that the direction is observed but not statistically confirmed; otherwise only the negative ECM4 result (623 vs. 680) is robust.
  2. [Sections 4.1 and 4.2, threshold choices] The evaluation is not protected against threshold selection. The paper evaluates multiple LBD thresholds (ECM3: LBD < 4; ECM4: LBD < 5; PCM: at most LBD 5 among the half with lowest LBD/activity; TopoSAT2: cap reduced to 3 "for better results on the used system") and reports the best-performing variants. No training/validation split, tuning protocol, or multiplicity correction is described. Since the main positive conclusion depends on the specific threshold, the manuscript should either validate the chosen thresholds on held-out benchmarks or report the sensitivity of Table 1 to the threshold, for example via a small parameter sweep.
  3. [Section 4.2, cross-solver comparison] The cross-solver inference is confounded. TopoSAT2 differs from Syrup not only in using ECM but also in branching, restart, database heuristics, preprocessing, and lazy export policy, and Sticky differs again in clause representation. The paper attributes the contradictory ECM results to lazy export policy and the visibility of vivification, but without ablating these factors the attribution is only a hypothesis. This matters because the conclusion that ECM "significantly increases performance on unsatisfiable SAT problems" is meant to be supported by the cross-solver data, yet TopoSAT2-ECM3 shows the opposite sign.
  4. [Section 4, experimental setup] The generalization to "parallel SAT solvers" rests on a single hardware/software configuration: 34 threads on one Xeon Phi socket, a 15,000-second time limit, and three SAT Competition benchmark sets. The paper itself acknowledges the compute-time restriction, but the abstract and conclusion are phrased more generally. Adding a scope statement in the conclusion, such as "on this benchmark suite and configuration," would align the claims with the evidence.
minor comments (6)
  1. [Abstract and Introduction] The abstract contains typos: "LCM let to performance improvements" should be "LCM led to performance improvements," and "Learned clauses minimization" should be "Learned clause minimization."
  2. [Section 3] The sentence "Our experiments show that ECM should be restricted to clauses with an LBD lower than 4" states a conclusion before the experiments are presented; it should be moved to the results or phrased as a hypothesis.
  3. [Section 4.1] The percentages cited from Audemard et al. [4] ("91% appear one time, 34% two times, 22% three times, 17% four times") are mutually inconsistent if read as exact frequencies; clarify whether these are cumulative percentages of clauses appearing at least that many times.
  4. [References] Reference [11] lists the author as "Thorst Ehlers"; this should be "Thorsten Ehlers."
  5. [Figure 3] The inset legend "smaller is better" is confusing because the x-axis is the number of solved instances; clarify which quantity is meant to be smaller.
  6. [Section 4.1] The statement "ECM3 is always faster than ECM4" is too strong for a cactus-plot comparison over solved instances; a paired runtime scatter plot or a phrase such as "ECM3 has a better cumulative runtime profile on the solved instances" would be more precise.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper is an empirical comparison whose reported gains are measured outcomes, not quantities defined in terms of the conclusions or derived from fitted constants.

full rationale

The paper makes no formal derivation claim. Its central results, that PCM leads to more solved instances overall and that an ECM variant with LBD below 4 improves UNSAT performance, are read directly from Table 1 and runtime cactus plots. The minimization approaches are implemented and then measured on SAT Competition benchmarks against upstream baselines (Syrup, TopoSAT2, Sticky), so the reported quantities are not defined in terms of the conclusions. The LBD threshold of 4 is presented as an experimental finding ('Our experiments show that ECM should be restricted to clauses with an LBD lower than 4'), and the paper also reports the worse-performing ECM4 configuration; the positive claim is therefore a selected empirical outcome rather than a parameter fit disguised as a prediction. Citations to prior work on vivification and on TopoSAT2's ECM are not self-citations and are not load-bearing in a circular sense. Any concern about small, unreplicated differences in Table 1 is a question of statistical robustness, not of circularity, and does not change the verdict.

Assumptions & free parameters 5 free parameters · 3 assumptions · 0 invented entities

The paper's central claims are empirical. They depend on benchmark representativeness, the chosen thresholds, and the hardware configuration. No free parameters are fitted to produce the claim; thresholds are hand-selected. The LPCM mechanism introduces an invented bookkeeping structure but no new physical or mathematical entity.

free parameters (5)
  • PCM vivification LBD threshold = 5
    Clauses with LBD <= 5 are candidates for vivification; chosen by hand and affects overhead.
  • ECM vivification LBD threshold for ECM3 = 3 (clauses with LBD < 4)
    The paper sets ECM to vivify clauses with LBD lower than 4; this threshold drives the main comparison.
  • ECM vivification LBD threshold for ECM4 = 4 (clauses with LBD < 5)
    The paper sets ECM to vivify clauses with LBD lower than 5; this increases overhead and reduces solved instances.
  • TopoSAT2 ECM LBD cap = 3
    They reduced TopoSAT2's maximum LBD for vivifying clauses to 3 for better results on the used system.
  • Number of parallel solver instances = 34
    34 instances on a 68-core Xeon Phi due to memory restrictions; affects parallelism and throughput.
assumptions (3)
  • domain assumption SAT Competition benchmark tracks (2016 application, 2017 and 2018 main) are representative of hard SAT instances for parallel solving.
    The paper draws general conclusions about LCM in parallel solvers from these three benchmark sets (Section 4).
  • domain assumption The 34-thread Xeon Phi configuration and 15,000 second limit model practical parallel SAT solving.
    All experiments use one Xeon Phi socket with 34 instances; conclusions may not transfer to different hardware or time limits (Section 4).
  • standard math Clause vivification applied at decision level zero preserves solver soundness and completeness.
    Section 2 states vivification is independent of search space when applied at decision level zero; the implementations delay vivification until restarts (Section 4.1).

how reviews work

0 comments
Cite this review

Pith. "Pith review of Learned Clause Minimization in Parallel SAT Solvers." pith.science (2026). https://pith.science/paper/7BYSWDW2

@misc{pith2026190801624,
  author       = {Pith},
  title        = {Pith review of: Learned Clause Minimization in Parallel SAT Solvers},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/7BYSWDW2}},
  note         = {Machine review of arXiv:1908.01624}
}
read the original abstract

Learned clauses minimization (LCM) let to performance improvements of modern SAT solvers especially in solving hard SAT instances. Despite the success of LCM approaches in sequential solvers, they are not widely incorporated in parallel SAT solvers. In this paper we explore the potential of LCM for parallel SAT solvers by defining multiple LCM approaches based on clause vivification, comparing their runtime in different SAT solvers and discussing reasons for performance gains and losses. Results show that LCM only boosts performance of parallel SAT solvers on a fraction of SAT instances. More commonly applying LCM decreases performance. Only certain LCM approaches are able to improve the overall performance of parallel SAT solvers.

Figures

Figures reproduced from arXiv: 1908.01624 by the authors.

Figure 1
Figure 1. The flowcharts show the workflow of each proposed LCM approach. The standard [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Percentage of propagations used for clause vivification by each approach. [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Runtime cactus plot of solved instances by every Syrup implementation. [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Runtime comparison plots of Syrup to Syrup-PCM (a, b) and Syrup to Syrup-ECM3 [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

28 extracted references · 27 canonical work pages

  1. [1]

    An effective distributed D&C approach for the satisfiability problem

    Gilles Audemard. An effective distributed D&C approach for the satisfiability problem. In In 22nd Euromicro International Conference on Parallel, Distributed and network-based Processing (PDP14), 2014

    work page 2014

  2. [2]

    Glucose 2.1, aggressive – but reactive – clause database management, dynamic restarts

    Gilles Audemard and Laurent Simon. Glucose 2.1, aggressive – but reactive – clause database management, dynamic restarts. Pragmatics of SAT (Workshop of SAT’12), 2012. 9 Learned Clause Minimization in Parallel SAT Solvers M. Hartung and F. Schintke

    work page 2012

  3. [3]

    Refining restarts strategies for SAT and UNSAT

    Gilles Audemard and Laurent Simon. Refining restarts strategies for SAT and UNSAT. In Prin- ciples and Practice of Constraint Programming - 18th International Conference, CP 2012, Qu´ ebec City, QC, Canada, October 8-12, 2012. Proceedings , pages 118–126, 2012

    work page 2012

  4. [4]

    Lazy clause exchange policy for parallel SAT solvers

    Gilles Audemard and Laurent Simon. Lazy clause exchange policy for parallel SAT solvers. In Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, pages 197–205, 2014

    work page 2014

  5. [5]

    Glucose and Syrup: Nine years in the SAT competitions

    Gilles Audemard and Laurent Simon. Glucose and Syrup: Nine years in the SAT competitions. In Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions , pages 24–25, 2018

    work page 2018

  6. [6]

    PicoSAT essentials

    Armin Biere. PicoSAT essentials. JSAT, 4(2-4):75–97, 2008

    work page 2008

  7. [7]

    Preprocessing and inprocessing techniques in SAT

    Armin Biere. Preprocessing and inprocessing techniques in SAT. In Kerstin Eder, Jo˜ ao Louren¸ co, and Onn Shehory, editors, Hardware and Software: Verification and Testing — 7th International Haifa Verification Conference, HVC 2011, Haifa, Israel, December 6-8, 2011, Revised Selected Papers, page 1, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg

    work page 2011

  8. [8]

    AbcdSAT and Glucose hack: Various simplifications and optimizations for CDCL SAT solvers

    Jingchao Chen. AbcdSAT and Glucose hack: Various simplifications and optimizations for CDCL SAT solvers. In Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions , pages 24–25, 2018

    work page 2018

Show all 28 references
  1. [9]

    Effective preprocessing in SAT through variable and clause elim- ination

    Niklas E´ en and Armin Biere. Effective preprocessing in SAT through variable and clause elim- ination. In Fahiem Bacchus and Toby Walsh, editors, Theory and Applications of Satisfiability Testing, pages 61–75, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg

    2005

  2. [10]

    An extensible SAT-solver

    Niklas E´ en and Niklas S¨ orensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing , pages 502–518, Berlin, Hei- delberg, 2004. Springer Berlin Heidelberg

    2004

  3. [11]

    Glucose hacks and TOPOSAT2 description

    Thorst Ehlers and Dirk Nowotka. Glucose hacks and TOPOSAT2 description. In Proceedings of SAT Competition 2018: Solver and Benchmark Descriptions , pages 47–48, 2018

    2018

  4. [12]

    Tuning parallel SAT solvers

    Thorsten Ehlers and Dirk Nowotka. Tuning parallel SAT solvers. EasyChair Preprint no. 195, EasyChair, 2018

    2018

  5. [13]

    Alembic: An efficient algorithm for CNF preprocessing

    Hyojung Han and Fabio Somenzi. Alembic: An efficient algorithm for CNF preprocessing. In In: Proceedings of the 44th Design Automation Conference (DAC 2007) , pages 582–587, 2007

    2007

  6. [14]

    Marijn J. H. Heule, Oliver Kullmann, and Armin Biere. Cube-and-Conquer for Satisfiability, pages 31–59. Springer International Publishing, Cham, 2018

    2018

  7. [15]

    Antti E. J. Hyv¨ arinen, Tommi Junttila, and Ilkka Niemel¨ a. Partitioning SAT instances for dis- tributed solving. In Christian G. Ferm¨ uller and Andrei Voronkov, editors,Logic for Programming, Artificial Intelligence, and Reasoning , pages 372–386, Berlin, Heidelberg, 2010. ...

    2010

  8. [16]

    An incremental algorithm to check satisfiability for bounded model checking

    HoonSang Jin and Fabio Somenzi. An incremental algorithm to check satisfiability for bounded model checking. Electronic Notes in Theoretical Computer Science , 119(2):51–65, 2005. Proceed- ings of the 2nd International Workshop on Bounded Model Checking (BMC 2004)

    2005

  9. [17]

    SArTagnan - a parallel portfolio SAT solver with lockless physical clause sharing

    Michael Kaufmann, Stephan Kottler, Michael Kaufmann, and Stephan Kottler. SArTagnan - a parallel portfolio SAT solver with lockless physical clause sharing. In In Pragmatics of SAT, 2011

    2011

  10. [18]

    Learning rate based branching heuristic for SAT solvers

    Jia Hui Liang, Vijay Ganesh, Pascal Poupart, and Krzysztof Czarnecki. Learning rate based branching heuristic for SAT solvers. In Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings , pages ...

    2016

  11. [19]

    An effective learnt clause mini- mization approach for CDCL SAT solvers

    Mao Luo, Chu-Min Li, Fan Xiao, Felip Many, and Zhipeng L. An effective learnt clause mini- mization approach for CDCL SAT solvers. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17 , pages 703–711, 2017

    2017

  12. [20]

    Moskewicz, Conor F

    Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001 , pages 530–535, 2001. 10 Learned Clause Minimiza...

    2001

  13. [21]

    A propagation rate based splitting heuristic for divide-and-conquer solvers

    Saeed Nejati, Zack Newsham, Joseph Scott, Jia Hui Liang, Catherine Gebotys, Pascal Poupart, and Vijay Ganesh. A propagation rate based splitting heuristic for divide-and-conquer solvers. In Serge Gaspers and Toby Walsh, editors, Theory and Applications of Satisfiability Testing...

    2017

  14. [22]

    Between SAT and UNSAT: the fundamental difference in CDCL SAT

    Chanseok Oh. Between SAT and UNSAT: the fundamental difference in CDCL SAT. In Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings, pages 307–323, 2015

    2015

  15. [23]

    Vivifying propositional clausal formulae

    Cdric Piette, Youssef Hamadi, and Lakhdar Sais. Vivifying propositional clausal formulae. In ECAI 2008 Proceedings, ECAI ’08, pages 525–529, 01 2008

    2008

  16. [24]

    Extending SAT solvers to cryptographic problems

    Mate Soos, Karsten Nohl, and Claude Castelluccia. Extending SAT solvers to cryptographic problems. In Theory and Applications of Satisfiability Testing - SAT 2009, 12th International Conference, SAT 2009, Swansea, UK, June 30 - July 3, 2009. Proceedings , pages 244–257, 2009

    2009

  17. [25]

    Minimizing learned clauses

    Niklas S¨ orensson and Armin Biere. Minimizing learned clauses. In Oliver Kullmann, editor, Theory and Applications of Satisfiability Testing - SAT 2009 , pages 237–243, Berlin, Heidelberg,

    2009

  18. [26]

    Sathiamoorthy Subbarayan and Dhiraj K. Pradhan. NiVER: Non-increasing variable elimination resolution for preprocessing SAT instances. In Holger H. Hoos and David G. Mitchell, editors, Theory and Applications of Satisfiability Testing, pages 276–291, Berlin, Heidelberg, 2005. S...

    2005

  19. [27]

    Concurrent clause strengthening

    Siert Wieringa and Keijo Heljanko. Concurrent clause strengthening. In Matti J¨ arvisalo and Allen Van Gelder, editors, Theory and Applications of Satisfiability Testing – SAT 2013 , pages 116–132, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. 11

    2013

  20. [2009]

    Springer Berlin Heidelberg

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.