Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning (Q3623009)

From MaRDI portal

!

This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:

scientific article; zbMATH DE number 5548985
Language Label Description Also known as
default for all languages
No label defined
    English
    Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
    scientific article; zbMATH DE number 5548985

      Statements

      Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning (English)
      0 references
      0 references
      0 references
      0 references
      29 April 2009
      0 references
      propositional proof complexity
      0 references
      resolution
      0 references
      satisfiability
      0 references
      SAT solving
      0 references
      weakening
      0 references
      proof search algorithms
      0 references
      0 references
      0 references

      Identifiers

      0 references
      0 references
      0 references
      0 references
      0 references
      0 references
      0 references