### 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 + n^{3}), 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 language | English (US) |
---|---|

Title of host publication | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |

Publisher | Springer Verlag |

Pages | 209-220 |

Number of pages | 12 |

Volume | 2054 |

ISBN (Print) | 3540420762, 9783540420767 |

DOIs | |

State | Published - 2001 |

Externally published | Yes |

Event | 6th International Workshop on DNA-Based Computers, DNA 2000 - Leiden, Netherlands Duration: Jun 13 2000 → Jun 17 2000 |

### Publication series

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

Volume | 2054 |

ISSN (Print) | 03029743 |

ISSN (Electronic) | 16113349 |

### Other

Other | 6th International Workshop on DNA-Based Computers, DNA 2000 |
---|---|

Country | Netherlands |

City | Leiden |

Period | 6/13/00 → 6/17/00 |

### Fingerprint

### ASJC Scopus subject areas

- Computer Science(all)
- Theoretical Computer Science

### Cite this

*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.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

*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

}

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

AN - SCOPUS:84958956223

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 -