ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

X
feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
  • 1
    Electronic Resource
    Electronic Resource
    New Worst-Case Upper Bounds for SAT (2000)
    Springer
    Journal of automated reasoning 24 (2000), S. 397-420 
    Details
    ISSN: 1573-0670
    Keywords: SAT ; worst-case upper bounds
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract In 1980 Monien and Speckenmeyer proved that satisfiability of a propositional formula consisting of K clauses (of arbitrary length) can be checked in time of the order 2 K / 3. Recently Kullmann and Luckhardt proved the worst-case upper bound 2 L / 9, where L is the length of the input formula. The algorithms leading to these bounds are based on the splitting method, which goes back to the Davis–Putnam procedure. Transformation rules (pure literal elimination, unit propagation, etc.) constitute a substantial part of this method. In this paper we present a new transformation rule and two algorithms using this rule. We prove that these algorithms have the worst-case upper bounds 20. 30897 K and 20. 10299 L , respectively.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1006340920104
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
  • 2
    Electronic Resource
    Electronic Resource
    SAT Local Search Algorithms: Worst-Case Study (2000)
    Springer
    Journal of automated reasoning 24 (2000), S. 127-143 
    Details
    ISSN: 1573-0670
    Keywords: SAT ; greedy local search ; worst-case time bounds
    Source: Springer Online Journal Archives 1860-2000
    Topics: Computer Science
    Notes: Abstract Recent experiments demonstrated that local search algorithms (e.g. GSAT) are able to find satisfying assignments for many “hard” Boolean formulas. A wide experimental study of these algorithms demonstrated their good performance on some inportant classes of formulas as well as poor performance on some other ones. In contrast, theoretical knowledge of their worst-case behavior is very limited. However, many worst-case upper and lower bounds of the form 2α n (α〈1 is a constant) are known for other SAT algorithms, for example, resolution-like algorithms. In the present paper we prove both upper and lower bounds of this form for local search algorithms. The class of linear-size formulas we consider for the upper bound covers most of the DIMACS benchmarks; the satisfiability problem for this class of formulas is NP-complete.
    Type of Medium: Electronic Resource
    URL: http://dx.doi.org/10.1023/A:1006318521185
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
    Paper (German National Licenses)
    Fulltext
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...