[sat] Clause layout: SmallVec<[Lit;4]> spills 5–8 lit clauses; main fits 8 inline in 64B cache line #43

Summary

Both trees mark Clause with #[repr(align(64))], but inline literal capacity and field order diverge. v0.3.2 still uses SmallVec<[Lit; 4]> with metadata-first layout; main reorders fields and uses SmallVec<[Lit; 8]> so typical learned clauses stay in one cache line with no heap spill.

Layout comparison

v0.3.2 (oxiz-sat/src/clause.rs)

#[repr(align(64))]
pub struct Clause {
    pub activity: f64,       // metadata first
    pub learned: bool,
    pub lbd: u32,
    pub deleted: bool,
    pub lits: SmallVec<[Lit; 4]>,  // spills at ≥5 lits
    pub tier: ClauseTier,
    pub usage_count: u32,
}

Comment says metadata is kept hot at the front so propagation touches one line before reading literals — but any clause with 5+ lits pays a heap indirection on every watch/BCP touch of lits.

main (00bd400d, 5d2ae229)

#[repr(align(64))]
pub struct Clause {
    /// SmallVec FIRST: 8×u32 lits + len/cap + metadata ≤ 64B
    pub lits: SmallVec<[Lit; 8]>,
    pub lbd: u32,
    pub usage_count: u32,
    pub activity: f64,
    pub learned: bool,
    pub deleted: bool,
    pub tier: ClauseTier,
}

Layout probe (type layout is compile-time; same at all opt levels):

[Lit;7] and [Lit;8] are the same SmallVec footprint (padding); main takes the free 8th slot.

Main also has assert!(size_of::<Clause>() <= 64) so the invariant can’t regress silently.

Why it matters

Structured instances learn longer clauses than random-3-SAT. With [Lit;4], most 5–8 lit clauses heap-allocate → ~2 cache misses per clause touch vs 1 when inline.

Main measurements (00bd400d):

Correct on 75 cadical/test/cnf instances; sat lib tests green.

This is pure layout — no API change — and is independent of lucky / lazy-HBR / opt-level gaps (#35, #38, #37).

Commits on main

• 00bd400d perf(sat): SmallVec<[Lit;7]> + field reorder — eliminates heap spills
• 5d2ae229 perf(sat): use SmallVec<[Lit;8]> — free over [Lit;7] (same 64B struct)

Suggested direction

1. Put lits: SmallVec<[Lit; 8]> first in Clause
2. Keep #[repr(align(64))] and add size_of::<Clause>() <= 64 test
3. Re-bench Urquhart / longmult / industrial CNF (and anything from [perf] sat #35)

No semantic change expected — only cache behaviour.