The symmetry rule in propositional logic

DOI10.1016/S0166-218X(99)00039-6zbMath0938.03023WikidataQ126297728 ScholiaQ126297728MaRDI QIDQ1961453

Alasdair Urquhart

Publication date: 14 February 2000

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

zbMATH Keywords

extension ruleexponential lower bound on the size of resolution refutationsrandom clausesymmetry rule

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Classical propositional logic (03B05) Complexity of proofs (03F20)

Related Items

On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ A Study of Symmetry Breaking Predicates and Model Counting ⋮ The state of SAT ⋮ Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas ⋮ Homomorphisms of conjunctive normal forms. ⋮ Testing satisfiability of CNF formulas by computing a stable set of points ⋮ The complexity of homomorphisms and renamings for minimal unsatisfiable formulas ⋮ Short proofs for some symmetric quantified Boolean formulas ⋮ \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver ⋮ Relative efficiency of propositional proof systems: Resolution vs. cut-free LK ⋮ A Logical Autobiography

Cites Work

• Unnamed Item
• Short proofs for tricky formulas
• Resolution proofs of generalized pigeonhole principles
• The intractability of resolution
• Explicit constructions of linear-sized superconcentrators
• On the complexity of regular resolution and the Davis-Putnam procedure
• The tail of the hypergeometric distribution
• Graphs on unlabelled nodes with a given number of edges
• Propositional proof systems, the consistency of first order theories and the complexity of computations
• Many hard examples for resolution
• Hard examples for resolution
• The relative efficiency of propositional proof systems
• The Complexity of Propositional Proofs

This page was built for publication: The symmetry rule in propositional logic