Solving optimal satisfiability problems through clause-directed A*
Thesis (M.Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2002.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2005
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/29242 |
| _version_ | 1811097368924258304 |
|---|---|
| author | Ragno, Robert J. (Robert John), 1977- |
| author2 | Brian C. Williams. |
| author_facet | Brian C. Williams. Ragno, Robert J. (Robert John), 1977- |
| author_sort | Ragno, Robert J. (Robert John), 1977- |
| collection | MIT |
| description | Thesis (M.Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2002. |
| first_indexed | 2024-09-23T16:58:26Z |
| format | Thesis |
| id | mit-1721.1/29242 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T16:58:26Z |
| publishDate | 2005 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/292422019-04-12T16:03:32Z Solving optimal satisfiability problems through clause-directed A* Solving optimal satisfiability problems through ClA* Ragno, Robert J. (Robert John), 1977- Brian C. Williams. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis (M.Eng.)--Massachusetts Institute of Technology, Dept. of Electrical Engineering and Computer Science, 2002. Includes bibliographical references (p. 37-38). Real-world applications, such as diagnosis and embedded control, are increasingly being framed as OpSAT problems - problems of finding the best solution that satisfies a formula in propositional state logic. Previous methods, such as Conflict-directed A*, solve OpSAT problems through a weak coupling of A* search, used to generate optimal candidates, and a DPLL-based SAT solver, used to test feasibility. This paper achieves a substantial performance improvement by introducing a tightly coupled approach, Clause-directed A * (CIA *). ClA* simultaneously directs the search towards assignments that are feasible and optimal. First, satisfiability is generalized to state logic by unifying the DPLL satisfiability procedure with forward checking. Second, optimal assignments are found by using A* to guide variable splitting within DPLL. Third, search is directed towards feasible regions of the state space by treating all clauses as conflicts, and by selecting only assignments that entail more clauses. Finally, ClA* climbs towards the optimum by using a variable ordering heuristic that emulates gradient search. Empirical experiments on real-world and randomly-generated instances demonstrate an order of magnitude increase in performance over Conflict-directed A*. by Robert J. Ragno. M.Eng. 2005-10-14T19:23:46Z 2005-10-14T19:23:46Z 2002 2002 Thesis http://hdl.handle.net/1721.1/29242 51589373 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 38 p. 1072047 bytes 1071855 bytes application/pdf application/pdf application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Ragno, Robert J. (Robert John), 1977- Solving optimal satisfiability problems through clause-directed A* |
| title | Solving optimal satisfiability problems through clause-directed A* |
| title_full | Solving optimal satisfiability problems through clause-directed A* |
| title_fullStr | Solving optimal satisfiability problems through clause-directed A* |
| title_full_unstemmed | Solving optimal satisfiability problems through clause-directed A* |
| title_short | Solving optimal satisfiability problems through clause-directed A* |
| title_sort | solving optimal satisfiability problems through clause directed a |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/29242 |
| work_keys_str_mv | AT ragnorobertjrobertjohn1977 solvingoptimalsatisfiabilityproblemsthroughclausedirecteda AT ragnorobertjrobertjohn1977 solvingoptimalsatisfiabilityproblemsthroughcla |