Struct ProofComplexitySystem 

pub struct ProofComplexitySystem {
    pub name: String,
    pub has_p_simulations: bool,
    pub simulates_resolution: bool,
    pub super_polynomial_lower_bound: bool,
}

Represents a proof system and its complexity measures.

Fields

name: String

Name of the proof system.

has_p_simulations: bool

Whether the system has polynomial-size proofs for tautologies (p-simulation).

simulates_resolution: bool

Whether the system can simulate resolution.

super_polynomial_lower_bound: bool

The Cook-Reckhow conjectured lower bound on proof size.

Implementations

impl ProofComplexitySystem

pub fn new(name: &str) -> Self

Create a new proof complexity system descriptor.

pub fn resolution() -> Self

Resolution proof system.

pub fn extended_frege() -> Self

Extended Frege system.

pub fn frege() -> Self

Frege system (Hilbert-style).

pub fn cook_reckhow_separation(&self) -> bool

Cook-Reckhow theorem: if NP ≠ coNP, no proof system is polynomially bounded.

pub fn php_complexity(&self) -> String

Propositional pigeonhole principle: known to require exponential proofs in Resolution.

Trait Implementations

impl Clone for ProofComplexitySystem

fn clone(&self) -> ProofComplexitySystem

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ProofComplexitySystem

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

Formats the value using the given formatter.