The following pages link to Hard examples for resolution (Q3780485):
Displaying 50 items.
- Tractable approximate deduction for OWL (Q274420) (← links)
- Towards NP-P via proof complexity and search (Q408544) (← links)
- A finite state intersection approach to propositional satisfiability (Q442157) (← links)
- Meta-resolution: An algorithmic formalisation (Q671650) (← links)
- Tractability of cut-free Gentzen type propositional calculus with permutation inference (Q672046) (← links)
- Exponential lower bounds for the pigeonhole principle (Q687506) (← links)
- Highly symmetric expanders (Q700158) (← links)
- Group cancellation and resolution (Q817703) (← links)
- Smaller superconcentrators of density 28 (Q844173) (← links)
- A feasibly constructive lower bound for resolution proofs (Q915457) (← links)
- Resolution proofs of generalized pigeonhole principles (Q920967) (← links)
- Formula dissection: A parallel algorithm for constraint satisfaction (Q931750) (← links)
- A simplified way of proving trade-off results for resolution (Q989569) (← links)
- A combinatorial characterization of treelike resolution space (Q1014444) (← links)
- On threshold BDDs and the optimal variable ordering problem (Q1016038) (← links)
- Resolution for Max-SAT (Q1028942) (← links)
- Resolution vs. cutting plane solution of inference problems: Some computational experience (Q1100093) (← links)
- Seventy-five problems for testing automatic theorem provers (Q1101242) (← links)
- Optimizing propositional calculus formulas with regard to questions of deducibility (Q1117918) (← links)
- Unrestricted resolution versus N-resolution (Q1185013) (← links)
- Tseitin's formulas revisited (Q1193906) (← links)
- Complexity of resolution proofs and function introduction (Q1194246) (← links)
- On the modelling of search in theorem proving -- towards a theory of strategy analysis (Q1281504) (← links)
- An exponential lower bound for the size of monotone real circuits (Q1288204) (← links)
- A lower bound for tree resolution (Q1336637) (← links)
- The complexity of the pigeonhole principle (Q1343166) (← links)
- The relative complexity of resolution and cut-free Gentzen systems (Q1353988) (← links)
- Davis-Putnam resolution versus unrestricted resolution (Q1353991) (← links)
- An average case analysis of a resolution principle algorithm in mechanical theorem proving. (Q1353997) (← links)
- Simplified lower bounds for propositional proofs (Q1374208) (← links)
- Proof complexity in algebraic systems and bounded depth Frege systems with modular counting (Q1377580) (← links)
- Resolution lower bounds for the weak functional pigeonhole principle. (Q1401365) (← links)
- Resolution and binary decision diagrams cannot simulate each other polynomially (Q1408378) (← links)
- On the structure of some classes of minimal unsatisfiable formulas (Q1408380) (← links)
- Equivalent literal propagation in the DLL procedure (Q1408382) (← links)
- Binary decision diagrams for first-order predicate logic. (Q1426055) (← links)
- On hard instances (Q1575555) (← links)
- Proving unsatisfiability of CNFs locally (Q1610678) (← links)
- Lower bound on average-case complexity of inversion of Goldreich's function by drunken backtracking algorithms (Q1678752) (← links)
- Approximate counting in SMT and value estimation for probabilistic programs (Q1683928) (← links)
- On subclasses of minimal unsatisfiable formulas (Q1841884) (← links)
- Space bounds for resolution (Q1854472) (← links)
- Resolution proofs of matching principles (Q1861903) (← links)
- Resolution lower bounds for perfect matching principles (Q1881260) (← links)
- On the complexity of resolution with bounded conjunctions (Q1885907) (← links)
- A new algorithm for the propositional satisfiability problem (Q1894360) (← links)
- Cutting planes, connectivity, and threshold logic (Q1908818) (← links)
- An exponential separation between the parity principle and the pigeonhole principle (Q1923563) (← links)
- Short resolution proofs for a sequence of tricky formulas (Q1924995) (← links)
- The complexity of inverting explicit Goldreich's function by DPLL algorithms (Q1946844) (← links)
