Struct GpuCdclConfig 

#[non_exhaustive]
pub struct GpuCdclConfig {
    pub max_learned_clauses: u32,
    pub max_learned_lits: u32,
    pub max_proof_u32: u32,
    pub restart_base: u32,
    pub reduce_interval: u32,
    pub max_conflicts: u32,
}

Configuration for the GPU CDCL (Conflict-Driven Clause Learning) solver.

Controls arena sizes for learned clauses, proof traces, and the deterministic restart/reduce schedule. The defaults are tuned for equivalence verification of circuits with up to ~10 000 variables; larger problems may need proportionally larger arenas.

Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

max_learned_clauses: u32

Maximum number of learned clauses retained in the arena.

max_learned_lits: u32

Maximum total literals across all learned clauses.

max_proof_u32: u32

Maximum size (in u32 words) of the resolution proof trace.

restart_base: u32

Base conflict count between deterministic restarts.

reduce_interval: u32

Conflict count between clause-database reductions.

max_conflicts: u32

Conflict budget: 0 = unlimited (default; no behavior change). When nonzero, the solver bails with status BUDGET_EXHAUSTED after this many conflicts without terminating, bounding wall-clock so a treewidth-hard instance returns gracefully instead of running to a CUDA launch timeout that poisons the primary context.

Trait Implementations

impl Clone for GpuCdclConfig

fn clone(&self) -> GpuCdclConfig

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for GpuCdclConfig

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for GpuCdclConfig

fn default() -> Self

Returns the “default value” for a type.

impl Copy for GpuCdclConfig