Skip to main content

refute_ordering

logicaffeine_proof::ordering

Function refute_ordering 

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

Refute a formula that contains a complete ordering-principle core. true iff a certificate is recovered — see ordering_certificate. Never a false refutation.