{"id":"250ff445-8744-43c7-b9df-880d7d29e772","arxiv_id":"1908.01624","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"Parallel SAT solvers mostly lose performance when learned clauses are vivified, but a private-minimization scheme yields modest overall gains.","lead":"The paper tests whether learned clause minimization, which speeds up sequential SAT solvers, transfers to parallel SAT solvers. It finds that most variants slow solving, while a private-clause variant gives small overall gains and an export-time variant helps unsatisfiable instances.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Positive claims in Section 5 rest on small, unreplicated solved-instance differences that may be within run-to-run noise.","rationale":"The paper is a careful empirical study, and the availability of the implementations is real support for reproducibility. However, the main contribution is an empirical claim about which LCM variants help, and the evidence for the positive claims is a handful of instances out of 1050. The paper reports no error bars or statistical tests, and the effect sizes are comparable to typical SAT solver variance. This is the same weak spot the reader identified; I agree with the CONDITIONAL verdict. The concern is not that the implementations are wrong, but that the broad conclusions in Section 5 generalize beyond what the data can establish. A concrete repeated-seed study would settle whether the effect is real or noise.","tokens_in":9251,"tokens_out":3796,"duration_ms":40373,"concrete_test":"Re-run Syrup, Syrup-PCM, and Syrup-ECM3 on the SAT'18 and SAT'17 benchmark sets with 10 independent random seeds (or, if seeds are fixed, randomized restart offsets), and for each configuration pair apply McNemar's test to the paired per-instance solved/unsolved outcomes and report the median and interquartile range of solved counts. If the PCM advantage over Syrup does not replicate in sign across most seeds or yields p ≥ 0.05 on the paired test, the Section 5 statement 'PCM leads to more solved instances in general' should be weakened to 'a modest, not statistically significant improvement was observed on this benchmark set.'","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central positive claims in Section 5 are supported by small, unreplicated absolute differences in Table 1. Syrup-PCM solves 698 instances vs 680 for Syrup, a gain of 18 of 1050 (~1.7%) that is concentrated in SAT'18 (+15) with +3 on SAT'16A and 0 on SAT'17. Syrup-LPCM is +6 overall; Syrup-ECM3 is +13 overall but with -7 SAT and +20 UNSAT, so the 'significant increase on UNSAT' is a net effect driven by one solver and one partition. Across solvers the pattern is inconsistent: TopoSAT2-ECM3 solves 18 fewer UNSAT instances than TopoSAT2, while Sticky-ECM3 solves 26 more. No confidence intervals, repeated runs, or paired significance tests are reported, so the observed effects are within the range that could be produced by run-to-run variance in a 34-thread portfolio with dynamic restarts and lazy clause sharing. The claim 'PCM leads to more solved instances in general' therefore rests on an untested assumption that the Table 1 differences are not noise; the negative result (ECM4 vs Syrup, 623 vs 680) is large enough to be robust, but the positive claims are not.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":9538,"tokens_out":7170,"duration_ms":68554,"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":[{"comment":"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.","section":"Section 4.2, Table 1"},{"comment":"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.","section":"Sections 4.1 and 4.2, threshold choices"},{"comment":"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.","section":"Section 4.2, cross-solver comparison"},{"comment":"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.","section":"Section 4, experimental setup"}],"minor_comments":[{"comment":"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.\"","section":"Abstract and Introduction"},{"comment":"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.","section":"Section 3"},{"comment":"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.","section":"Section 4.1"},{"comment":"Reference [11] lists the author as \"Thorst Ehlers\"; this should be \"Thorsten Ehlers.\"","section":"References"},{"comment":"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.","section":"Figure 3"},{"comment":"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.","section":"Section 4.1"}],"recommendation":"major_revision","confidential_remarks":"This is an honest and clearly written empirical study with released code, but the central positive claims are currently at the level of observed differences without variance analysis. If the authors add paired significance tests, repeated runs, or a clear reframing as preliminary observations, the paper is publishable. The negative result for ECM4 is robust and valuable. No citation concerns."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a well-executed empirical study with a useful negative result and a partially supported positive one. The paper deserves peer review, but the conclusion that ECM 'significantly increases' UNSAT performance is too strong given the evidence.\n\nWhat's new: the paper gives the first systematic comparison of three homogeneous LCM strategies (PCM, LPCM, ECM) in parallel portfolio solvers, implements them in Glucose-Syrup, and adds the LPCM pointer-sharing scheme. The artifacts are public. That is real.\n\nThe work does well: the benchmark set is standard (SAT Competition 2016-18, 1050 instances), the implementations are grounded in existing solvers, and the paper reports both solved-instance counts and runtime distributions. The negative result—ECM4 with an LBD cutoff of 5 clearly hurts (623 vs 680 solved)—is solid and matches the authors' own overhead analysis.\n\nSoft spots: the positive effects are small and unreplicated. Syrup-PCM gains 18 instances over 1050; the gain is concentrated in SAT'18. ECM3 gains 20 UNSAT instances, and this is consistent across the three benchmark sets for Syrup, but the other two solvers do not confirm it: TopoSAT2-ECM3 solves 18 fewer UNSAT instances than plain TopoSAT2, while Sticky-ECM3 solves 26 more. So the 'significant' claim in the conclusion is really solver-specific. There are no confidence intervals or repeated runs, and with 34 threads and dynamic restarts, run-to-run variance is a real risk. That said, the consistency of Syrup-ECM3's UNSAT gain across all three years makes it more than a single-instance fluke; I would not call the effect fabricated, but it is unproven. The causal explanations in Section 5 are plausible, not tested.\n\nBottom line: this is for SAT solver builders. It gives them practical guidance—use targeted LCM or none; broad vivification of imported clauses is usually harmful. The paper is honest about many of its own limitations. I would send it to peer review and ask the authors either to run repeated trials or to scope the conclusions to the specific solvers and configurations. The central claims are worth testing, not dismissing.","headline":"Useful empirical study of clause minimization in parallel SAT solvers, but the positive conclusions are too strong for the small, unreplicated effect sizes.","tokens_in":10040,"tokens_out":3547,"would_cite":true,"duration_ms":34875,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Most parallel SAT solvers slow down when learned-clause minimization is added, and only targeted variants help.","keywords":["learned clause minimization","clause vivification","parallel SAT solving","portfolio solvers","clause sharing","LBD","unsatisfiable instances","Glucose-Syrup"],"falsifier":"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.","tokens_in":9072,"feed_emoji":"⚙️","tokens_out":9255,"duration_ms":89715,"temperature":0.7,"pith_summary":"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.","feed_headline":"Most parallel SAT solvers slow down when clause minimization is added","feed_subtitle":"A 1,050-benchmark comparison: private-clause minimization wins, while export minimization helps mainly unsatisfiable instances.","key_machinery":"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.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the sequential learned clause minimization procedure that the paper ports to parallel solvers.","marker":"[19]"},{"why":"Defines clause vivification, the core shortening operation used by all proposed approaches.","marker":"[23]"},{"why":"Provides the lazy clause exchange policy and the statistics on how rarely imported clauses are reused.","marker":"[4]"},{"why":"Describes the TopoSAT2 ECM implementation that the paper compares against its own ECM variants.","marker":"[11]"},{"why":"Defines the LBD measure used to select clauses for vivification in the ECM approaches.","marker":"[2]"},{"why":"Introduces concurrent clause strengthening and physical clause sharing used by the Sticky solver comparison.","marker":"[27]"},{"why":"Documents the Glucose/Syrup solver baseline that all proposed implementations extend.","marker":"[5]"}],"fun_headline_variants":["Private clause vivification alone boosts parallel SAT solvers","Sharing minimized clauses usually slows parallel SAT solvers","LCM in parallel: only small-LBD exports help unsatisfiable","Vivification timing decides if parallel SAT solvers profit","Where you vivify changes parallel SAT solver speed"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Private clause vivification alone boosts parallel SAT solvers","Sharing minimized clauses usually slows parallel SAT solvers","LCM in parallel: only small-LBD exports help unsatisfiable","Vivification timing decides if parallel SAT solvers profit","Where you vivify changes parallel SAT solver speed"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000211,"raw_usage":{"total_tokens":1375,"prompt_tokens":866,"completion_tokens":509,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":482,"completion_tokens_details":{"reasoning_tokens":431}},"tokens_in":482,"tokens_out":509,"duration_ms":5093,"temperature":1.0,"reasoning_tokens":431,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T15:06:34.409007+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"An effective learnt clause mini- mization approach for CDCL SAT solvers","cited_arxiv_id":null,"evidence_quote":"Supplies the sequential learned clause minimization procedure that the paper ports to parallel solvers."},{"cited_title":"Vivifying propositional clausal formulae","cited_arxiv_id":null,"evidence_quote":"Defines clause vivification, the core shortening operation used by all proposed approaches."},{"cited_title":"Lazy clause exchange policy for parallel SAT solvers","cited_arxiv_id":null,"evidence_quote":"Provides the lazy clause exchange policy and the statistics on how rarely imported clauses are reused."},{"cited_title":"Glucose hacks and TOPOSAT2 description","cited_arxiv_id":null,"evidence_quote":"Describes the TopoSAT2 ECM implementation that the paper compares against its own ECM variants."},{"cited_title":"Glucose 2.1, aggressive – but reactive – clause database management, dynamic restarts","cited_arxiv_id":null,"evidence_quote":"Defines the LBD measure used to select clauses for vivification in the ECM approaches."},{"cited_title":"Concurrent clause strengthening","cited_arxiv_id":null,"evidence_quote":"Introduces concurrent clause strengthening and physical clause sharing used by the Sticky solver comparison."},{"cited_title":"Glucose and Syrup: Nine years in the SAT competitions","cited_arxiv_id":null,"evidence_quote":"Documents the Glucose/Syrup solver baseline that all proposed implementations extend."}],"review_version":1}