A DNA-based random walk method for solving k-SAT

Sergio Díaz, Juan Luis Esteban, Mitsunori Ogihara

Research output: Chapter in Book/Report/Conference proceedingConference contribution

10 Citations (Scopus)

Abstract

This paper presents an implementation of a concurrent version of Schöning’s algorithm for k-SAT in [Sch99]. It is shown that the algorithm can be implemented with space complexity (Formula Presented) and time complexity O(kmn + n3), where n is the number of variables and m the number of clauses. Besides, borrowing ideas from the above mentioned implementation, it is presented an implementation of resolution, a widely studied and used proof system, mainly in the fields of Proof Complexity and Automated Theorem Proving.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages209-220
Number of pages12
Volume2054
ISBN (Print)3540420762, 9783540420767
DOIs
StatePublished - 2001
Externally publishedYes
Event6th International Workshop on DNA-Based Computers, DNA 2000 - Leiden, Netherlands
Duration: Jun 13 2000Jun 17 2000

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2054
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other6th International Workshop on DNA-Based Computers, DNA 2000
CountryNetherlands
CityLeiden
Period6/13/006/17/00

Fingerprint

Random walk
DNA
Theorem proving
Proof Complexity
Automated Theorem Proving
Proof System
Space Complexity
Time Complexity
Concurrent

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Díaz, S., Esteban, J. L., & Ogihara, M. (2001). A DNA-based random walk method for solving k-SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2054, pp. 209-220). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2054). Springer Verlag. https://doi.org/10.1007/3-540-44992-2_14

A DNA-based random walk method for solving k-SAT. / Díaz, Sergio; Esteban, Juan Luis; Ogihara, Mitsunori.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 2054 Springer Verlag, 2001. p. 209-220 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2054).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Díaz, S, Esteban, JL & Ogihara, M 2001, A DNA-based random walk method for solving k-SAT. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 2054, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2054, Springer Verlag, pp. 209-220, 6th International Workshop on DNA-Based Computers, DNA 2000, Leiden, Netherlands, 6/13/00. https://doi.org/10.1007/3-540-44992-2_14
Díaz S, Esteban JL, Ogihara M. A DNA-based random walk method for solving k-SAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 2054. Springer Verlag. 2001. p. 209-220. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-44992-2_14
Díaz, Sergio ; Esteban, Juan Luis ; Ogihara, Mitsunori. / A DNA-based random walk method for solving k-SAT. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 2054 Springer Verlag, 2001. pp. 209-220 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{aaa4a8c3afb44c46b715fae18b9837b9,
title = "A DNA-based random walk method for solving k-SAT",
abstract = "This paper presents an implementation of a concurrent version of Sch{\"o}ning’s algorithm for k-SAT in [Sch99]. It is shown that the algorithm can be implemented with space complexity (Formula Presented) and time complexity O(kmn + n3), where n is the number of variables and m the number of clauses. Besides, borrowing ideas from the above mentioned implementation, it is presented an implementation of resolution, a widely studied and used proof system, mainly in the fields of Proof Complexity and Automated Theorem Proving.",
author = "Sergio D{\'i}az and Esteban, {Juan Luis} and Mitsunori Ogihara",
year = "2001",
doi = "10.1007/3-540-44992-2_14",
language = "English (US)",
isbn = "3540420762",
volume = "2054",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "209--220",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

T1 - A DNA-based random walk method for solving k-SAT

AU - Díaz, Sergio

AU - Esteban, Juan Luis

AU - Ogihara, Mitsunori

PY - 2001

Y1 - 2001

N2 - This paper presents an implementation of a concurrent version of Schöning’s algorithm for k-SAT in [Sch99]. It is shown that the algorithm can be implemented with space complexity (Formula Presented) and time complexity O(kmn + n3), where n is the number of variables and m the number of clauses. Besides, borrowing ideas from the above mentioned implementation, it is presented an implementation of resolution, a widely studied and used proof system, mainly in the fields of Proof Complexity and Automated Theorem Proving.

AB - This paper presents an implementation of a concurrent version of Schöning’s algorithm for k-SAT in [Sch99]. It is shown that the algorithm can be implemented with space complexity (Formula Presented) and time complexity O(kmn + n3), where n is the number of variables and m the number of clauses. Besides, borrowing ideas from the above mentioned implementation, it is presented an implementation of resolution, a widely studied and used proof system, mainly in the fields of Proof Complexity and Automated Theorem Proving.

UR - http://www.scopus.com/inward/record.url?scp=84958956223&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84958956223&partnerID=8YFLogxK

U2 - 10.1007/3-540-44992-2_14

DO - 10.1007/3-540-44992-2_14

M3 - Conference contribution

SN - 3540420762

SN - 9783540420767

VL - 2054

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 209

EP - 220

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

ER -