Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms

Evgeny Dantsin, Edward A. Hirsch, Alexander Wolpert

Research output

9 Citations (Scopus)

Abstract

We give a deterministic algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. Its upper bound on the worst-case running time matches the best known upper bound for randomized satisfiability-testing algorithms [6]. In comparison with the randomized algorithm in [6], our deterministic algorithm is simpler and more intuitive.

Original languageEnglish
Title of host publicationAlgorithms and Complexity - 6th Italian Conference, CIAC 2006, Proceedings
PublisherSpringer Nature
Pages60-68
Number of pages9
ISBN (Print)354034375X, 9783540343752
DOIs
Publication statusPublished - 1 Jan 2006
Event6th Italian Conference on Algorithms and Complexity, CIAC 2006 - Rome
Duration: 29 May 200631 May 2006

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume3998 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference6th Italian Conference on Algorithms and Complexity, CIAC 2006
CountryItaly
CityRome
Period29/05/0631/05/06

Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms'. Together they form a unique fingerprint.

  • Cite this

    Dantsin, E., Hirsch, E. A., & Wolpert, A. (2006). Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms. In Algorithms and Complexity - 6th Italian Conference, CIAC 2006, Proceedings (pp. 60-68). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3998 LNCS). Springer Nature. https://doi.org/10.1007/11758471_9