Skip to main content

find_random_core

Function find_random_core 

Source
pub fn find_random_core(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    max_steps: usize,
) -> Option<Vec<Vec<Lit>>>
Expand description

Find the randomness. Strip every structural lever — a certified cut decides it (so there was no irreducible randomness), carve (unit/pure/subsumption) and bounded variable elimination peel structure away — and return what survives: the irreducible core. None means the instance was fully structured and got decided. Some(core) is the kernel where carving can do no more; check it with diagnose — if it also has no cut and ~zero symmetry-bits, that is the randomness, isolated.