Short Proofs May Be Spacious : Understanding Space in Resolution
Om man ser på de bästa nu kända algoritmerna för att avgöra satisfierbarhet hos logiska formler så är de allra flesta baserade på den så kallade DPLL-metoden utökad med klausulinlärning. De två viktigaste gränssättande faktorerna för sådana algoritmer är hur mycket tid och minne de använder, och att...
| Main Author: | |
|---|---|
| Format: | Doctoral Thesis |
| Language: | English |
| Published: |
KTH, Teoretisk datalogi, TCS
2008
|
| Subjects: | |
| Online Access: | http://urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-4704 http://nbn-resolving.de/urn:isbn:978-91-7178-936-5 |