Versenden
Drucken
Rühmkorf, Jens (2010) Using Autarky to Evaluate Quantified Boolean Formulae. The Fourth International Conference on Advanced Engineering Computing and Applications in Sciences (ADVCOMP 2010), Florence, Italy.
![[img]](https://elib.dlr.de/style/images/fileicons/application_pdf.png) |
PDF
- Nur DLR-intern zugänglich
185kB |
Kurzfassung
In this paper, we discuss algorithmical implications for the extension of autarky from SAT to evaluate QBF formulas. First, we describe the Davis-Putnam procedure for SAT. Then we explain efficient known data structures as used for our SAT solver and known extensions to QBF. Finally, we introduce the concept of autarky in general and 2-autarkies in particular and discuss algorithmical implications for QBF. To the best of our knowledge we are the first to discuss described techniques for pruning the search tree of QBF solvers.
| elib-URL des Eintrags: | https://elib.dlr.de/65244/ | ||||||||
|---|---|---|---|---|---|---|---|---|---|
| Dokumentart: | Konferenzbeitrag (Vortrag, Paper) | ||||||||
| Zusätzliche Informationen: | Best Paper Award ADVCOMP 2010 | ||||||||
| Titel: | Using Autarky to Evaluate Quantified Boolean Formulae | ||||||||
| Autoren: |
| ||||||||
| Datum: | 2010 | ||||||||
| Referierte Publikation: | Ja | ||||||||
| Open Access: | Nein | ||||||||
| Gold Open Access: | Nein | ||||||||
| In SCOPUS: | Nein | ||||||||
| In ISI Web of Science: | Nein | ||||||||
| Status: | akzeptierter Beitrag | ||||||||
| Stichwörter: | Autarky; Davis-Putnam; SAT; QBF | ||||||||
| Veranstaltungstitel: | The Fourth International Conference on Advanced Engineering Computing and Applications in Sciences (ADVCOMP 2010) | ||||||||
| Veranstaltungsort: | Florence, Italy | ||||||||
| Veranstaltungsart: | internationale Konferenz | ||||||||
| HGF - Forschungsbereich: | Luftfahrt, Raumfahrt und Verkehr | ||||||||
| HGF - Programm: | keine Zuordnung | ||||||||
| HGF - Programmthema: | keine Zuordnung | ||||||||
| DLR - Schwerpunkt: | Luftfahrt | ||||||||
| DLR - Forschungsgebiet: | L - keine Zuordnung | ||||||||
| DLR - Teilgebiet (Projekt, Vorhaben): | L - keine Zuordnung (alt) | ||||||||
| Standort: | Köln-Porz | ||||||||
| Institute & Einrichtungen: | Institut für Simulations- und Softwaretechnik Institut für Simulations- und Softwaretechnik > Verteilte Systeme und Komponentensoftware | ||||||||
| Hinterlegt von: | Rühmkorf, Jens | ||||||||
| Hinterlegt am: | 23 Sep 2010 13:53 | ||||||||
| Letzte Änderung: | 12 Dez 2013 21:01 |
Nur für Mitarbeiter des Archivs: Kontrollseite des Eintrags
