|
|
|
|
| Bachelorprojekt - Softwareteknologi | Project No. 0100: SAT Algorithms in Prolog |
| Aktuelle | Tidligere |
The SAT problem - determining if a formula in proposition logic is satisfiable - is decidable: at worst, construct a truth table by evaluating the formula for every possible assignment of truth values (T or F) to the atomic propositions. If there are n atomic propositions, there are 2n assignments, so this is an inefficient algorithm. If there is an efficient algorithm that can decide the satisfiability of all formulas, this would solve the P=NP? problem in the affirmative, which is unlikely.
However, research has discovered many interesting algorithms that have proved to be very efficient in practice. The algorithms are generally based on the DPLL (David, Putnam, Logemann, Loveland) algorithm and add sophisticated search methods and heuristics. The project is to implement some of these algorithms in Prolog; the implementation should enable the user to understand the algorithms by tracing their progress.
The project may be co-supervised by associate professor Moti Ben-Ari, Weizmann Institute of Science, Israel.
| Prerequisites: | 02156 Logical Systems and Logic Programming |
Supervisor(s) Jørgen Villadsen
| Sidst opdateret: Nov 18, 2011 af Hans Henrik Løvengreen |