Short proofs for tricky formulas
From MaRDI portal
Publication:800909
DOI10.1007/BF00265682zbMath0552.03009OpenAlexW1999522767MaRDI QIDQ800909
Publication date: 1985
Published in: Acta Informatica (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/bf00265682
symmetryRamsey numbersextensionresolutionformal proofspropositional calculusacyclic digraphcheckerboard puzzleinductive argumentspropositional tautologies
Related Items
On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers, Tractability through symmetries in propositional calculus, Mutilated chessboard problem is exponentially hard for resolution, The state of SAT, Local and global symmetry breaking in itemset mining, Short resolution proofs for a sequence of tricky formulas, Regular and General Resolution: An Improved Separation, The limits of tractability in resolution-based propositional proof systems, Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas, Symmetric blocking, Homomorphisms of conjunctive normal forms., Local Symmetry Breaking During Search in CSPs, The symmetry rule in propositional logic, Propositional proof systems based on maximum satisfiability, Ground resolution with group computations on semantic symmetries, Testing satisfiability of CNF formulas by computing a stable set of points, The complexity of homomorphisms and renamings for minimal unsatisfiable formulas, Exploiting Symmetry in SMT Problems, Short proofs for some symmetric quantified Boolean formulas, An Exponential Lower Bound for Width-Restricted Clause Learning, Sum of squares bounds for the ordering principle, Resolution and the binary encoding of combinatorial principles, \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver, Relative efficiency of propositional proof systems: Resolution vs. cut-free LK, Separation results for the size of constant-depth propositional proofs, Symmetries, almost symmetries, and lazy clause generation, On Linear Resolution, Formula simplification via invariance detection by algebraically indexed types
