Fast incremental unit propagation by unifying watched-literals and local repair
Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Aeronautics and Astronautics, 2006.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2007
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/37691 |
| _version_ | 1826201911973380096 |
|---|---|
| author | Qu, Shen, S.M. Massachusetts Institute of Technology |
| author2 | Brian C. Williams. |
| author_facet | Brian C. Williams. Qu, Shen, S.M. Massachusetts Institute of Technology |
| author_sort | Qu, Shen, S.M. Massachusetts Institute of Technology |
| collection | MIT |
| description | Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Aeronautics and Astronautics, 2006. |
| first_indexed | 2024-09-23T11:58:48Z |
| format | Thesis |
| id | mit-1721.1/37691 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T11:58:48Z |
| publishDate | 2007 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/376912019-04-11T11:24:03Z Fast incremental unit propagation by unifying watched-literals and local repair Qu, Shen, S.M. Massachusetts Institute of Technology Brian C. Williams. Massachusetts Institute of Technology. Dept. of Aeronautics and Astronautics. Massachusetts Institute of Technology. Dept. of Aeronautics and Astronautics. Aeronautics and Astronautics. Thesis (S.M.)--Massachusetts Institute of Technology, Dept. of Aeronautics and Astronautics, 2006. Includes bibliographical references (p. 100-102). The propositional satisfiability problem has been studied extensively due to its theoretical significance and applicability to a variety of fields including diagnosis, autonomous control, circuit testing, and software verification. In these applications, satisfiability problem solvers are often used to solve a large number of problems that are essentially the same and only differ from each other by incremental alterations. Furthermore, unit propagation is a common component of satisfiability problem solvers that accounts for a considerable amount of the solvers' computation time. Given this knowledge, it is desirable to develop incremental unit propagation algorithms that can efficiently perform changes between similar theories. This thesis introduces two new incremental unit propagation algorithms, called Logic-based Truth Maintenance System with Watched-literals and Incremental Truth Maintenance System with Watched-literals. These algorithms combine the strengths of the Logic-based and Incremental Truth Maintenance Systems designed for generic problem solvers with a state-of-the-art satisfiability solver data structure called watched literals. (cont.) Empirical results show that the use of the watched-literals data structure significantly decreases workload of the LTMS and the ITMS without adversely affecting the incremental performance of these truth maintenance systems. by Shen Qu. S.M. 2007-06-28T12:24:13Z 2007-06-28T12:24:13Z 2006 2006 Thesis http://hdl.handle.net/1721.1/37691 129947026 eng M.I.T. theses are protected by copyright. They may be viewed from this source for any purpose, but reproduction or distribution in any format is prohibited without written permission. See provided URL for inquiries about permission. http://dspace.mit.edu/handle/1721.1/7582 102 p. application/pdf Massachusetts Institute of Technology |
| spellingShingle | Aeronautics and Astronautics. Qu, Shen, S.M. Massachusetts Institute of Technology Fast incremental unit propagation by unifying watched-literals and local repair |
| title | Fast incremental unit propagation by unifying watched-literals and local repair |
| title_full | Fast incremental unit propagation by unifying watched-literals and local repair |
| title_fullStr | Fast incremental unit propagation by unifying watched-literals and local repair |
| title_full_unstemmed | Fast incremental unit propagation by unifying watched-literals and local repair |
| title_short | Fast incremental unit propagation by unifying watched-literals and local repair |
| title_sort | fast incremental unit propagation by unifying watched literals and local repair |
| topic | Aeronautics and Astronautics. |
| url | http://hdl.handle.net/1721.1/37691 |
| work_keys_str_mv | AT qushensmmassachusettsinstituteoftechnology fastincrementalunitpropagationbyunifyingwatchedliteralsandlocalrepair |