Core First Unit Propagation

Jingchao Chen

arxiv: 1907.01192 · v1 · pith:PTHU445Onew · submitted 2019-07-02 · 💻 cs.LO

Core First Unit Propagation

Jingchao Chen This is my paper

Pith reviewed 2026-05-25 11:01 UTC · model grok-4.3

classification 💻 cs.LO

keywords SAT solversunit propagationCDCLcore clausesliteral block distancelearnt clauses

0 comments

The pith

Core first unit propagation prefers low-LBD clauses during Boolean constraint propagation to produce shorter learnt clauses.

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

The paper introduces core first unit propagation, a change to how CDCL SAT solvers scan clauses when performing unit propagation. Instead of scanning the watch list in linear order, the method prioritizes clauses whose literal block distance is at most 7. The goal is to trigger conflicts that produce shorter clauses to learn. Tests on the 2018 SAT competition winner show measurable gains in solved instances.

Core claim

Core first unit propagation modifies the standard linear scan of the watch list by always trying core clauses first. A core clause is one whose literal block distance is seven or less. By generating conflicts from these clauses sooner, the solver derives shorter learnt clauses, which in turn improve the overall search.

What carries the argument

core first unit propagation: the rule that selects clauses with literal block distance at most 7 before non-core clauses when propagating units.

If this is right

Shorter learnt clauses reduce the size of the clause database and the cost of subsequent propagations.
The same preference rule can be added to any CDCL solver that already tracks literal block distance.
Empirical improvement appears on the specific benchmark set used in the 2018 competition.
The change requires only a reordering of the watch list traversal and no new data structures.

Where Pith is reading between the lines

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

If the preference consistently shortens clauses, solvers could adopt a dynamic threshold instead of the fixed value of seven.
The technique might interact with other heuristics such as clause deletion policies that also use literal block distance.
It remains open whether the same ordering helps on unsatisfiable instances or only on satisfiable ones.

Load-bearing premise

That giving priority to clauses with literal block distance seven or less will produce shorter learnt clauses rather than merely reordering propagation without any net gain.

What would settle it

Run the modified solver and the unmodified 2018 winner on the same SAT competition benchmark set and measure both the average length of learnt clauses and the total number of instances solved within the time limit.

read the original abstract

Unit propagation (which is called also Boolean Constraint Propagation) has been an important component of every modern CDCL SAT solver since the CDCL solver was developed. In general, unit propagation is implemented by scanning sequentially every clause over a linear watch-list. This paper presents a new unit propagation technique called core first unit propagation. The main idea is to prefer core clauses over non-core ones during unit propagation, trying to generate a shorter learnt clause. Here, the core clause is defined as one with literal block distance less than or equal to 7. Empirical results show that core first unit propagation improves the performance of the winner of the SAT Competition 2018, MapleLCMDistChronoBT.

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.

Desk Editor's Note private letter to a colleague

A narrow heuristic tweak to clause scanning order in unit propagation that claims a speed boost on one 2018 SAT winner but supplies almost no experimental backing.

read the letter

The core idea is to change the order in which a CDCL solver scans its watch list during unit propagation: check low-LBD clauses (called core, LBD <= 7) before the rest, on the hope that this produces shorter learnt clauses. The paper presents this as a new rule layered on top of existing LBD and CDCL machinery and says it improves MapleLCMDistChronoBT, the 2018 competition winner. That is the actual contribution—an incremental ordering preference rather than a new data structure or proof system. If the measured gain is real and reproducible, it could matter for people who run these solvers on verification or planning instances where every percent counts. The motivation is straightforward and stays inside the standard architecture, which keeps the change easy to implement and test. The main weakness is the evidence. The abstract asserts an improvement but gives no instance counts, no tables, no ablation runs, and no statistical checks. Without those, it is impossible to tell whether the reported gain comes from the new ordering or from other factors in the solver. The assumption that preferring LBD <= 7 clauses will reliably shorten learnt clauses is plausible but not automatic; reordering can easily produce no net benefit or even longer clauses on some problems. The paper also introduces one free parameter (the LBD threshold) without showing sensitivity analysis. This work is aimed at the small group of researchers who tune SAT solver heuristics for competitions or embedded use. It is not a broad theoretical result and does not change how we think about CDCL, but the change is concrete enough that a referee could check the experiments and decide whether the improvement is worth adopting. I would send it to peer review so the data can be examined; the idea is simple and the claim is falsifiable once the numbers are on the table.

Referee Report

2 major / 0 minor

Summary. The manuscript presents 'core first unit propagation', a modification to unit propagation in CDCL SAT solvers. It prioritizes 'core' clauses (LBD ≤ 7) during propagation to try to produce shorter learnt clauses. The paper claims this improves the performance of MapleLCMDistChronoBT from the SAT Competition 2018.

Significance. A simple change to the propagation order could have practical impact on SAT solving if the improvement is real and reproducible. However, without experimental details, the significance cannot be properly assessed. The paper does not provide machine-checked proofs or parameter-free derivations.

major comments (2)

[Abstract] The abstract asserts that empirical results show improvement but supplies no experimental details, instance counts, statistical tests, or ablation data. This is load-bearing for the central empirical claim.
[Abstract] The LBD threshold of 7 for defining core clauses is presented without justification or analysis of its sensitivity, and it is a free parameter.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the comments. We address the major comments point by point below, indicating planned revisions where appropriate.

read point-by-point responses

Referee: [Abstract] The abstract asserts that empirical results show improvement but supplies no experimental details, instance counts, statistical tests, or ablation data. This is load-bearing for the central empirical claim.

Authors: The body of the manuscript describes the evaluation on the SAT Competition 2018 benchmark instances used to assess MapleLCMDistChronoBT. We agree the abstract should be self-contained and will revise it to include the number of instances, the observed improvement in solved instances, and a note on the comparison setup. revision: yes
Referee: [Abstract] The LBD threshold of 7 for defining core clauses is presented without justification or analysis of its sensitivity, and it is a free parameter.

Authors: The threshold follows the definition of core clauses already employed inside MapleLCMDistChronoBT. We acknowledge it is a tunable parameter and will add a short justification together with a sensitivity experiment in the revised manuscript. revision: yes

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper presents a heuristic modification to unit propagation in CDCL SAT solvers (preferring clauses with LBD <= 7) and reports empirical performance gains on an existing competition solver. No derivation chain, equations, fitted parameters renamed as predictions, or self-citation load-bearing steps are present in the provided text. The LBD threshold is a fixed definition used to motivate the heuristic, not derived from or equivalent to the experimental outcomes. The central claim rests on external benchmarking rather than internal reduction to inputs.

Axiom & Free-Parameter Ledger

1 free parameters · 1 axioms · 0 invented entities

The LBD threshold of 7 is a chosen cutoff used to label core clauses; the paper relies on the standard CDCL assumption that unit propagation occurs via sequential watch-list scans.

free parameters (1)

LBD threshold for core clauses = 7
The value 7 is used to decide which clauses are core and therefore preferred; this cutoff is stated without derivation from first principles.

axioms (1)

domain assumption Unit propagation is implemented by scanning sequentially every clause over a linear watch-list.
This is the baseline implementation the new technique modifies.

pith-pipeline@v0.9.0 · 5626 in / 1110 out tokens · 30050 ms · 2026-05-25T11:01:14.753715+00:00 · methodology

Core First Unit Propagation

Core claim

What carries the argument

If this is right

Where Pith is reading between the lines

Load-bearing premise

What would settle it

discussion (0)