Logic programming with the stable model (answer set) semantics has been put forward as a novel constraint programming paradigm. It is well-known that constraint satisfaction problems (CSPs), the Hamiltonian circuit (HC) problern, and planning problems in STRIPS format can be encoded in domain restricted logic programs such that stable models of these programs correspond to solutions to the problems. In this thesis, we shall show that these problems can be encoded in such a way that the encoded programs are tight on every model of their Clark completions. According to a result in [3], this implies that stable models of these logic programs can be found by using propositional satisfiability (SAT) solvers on their Clark completions....[ Read more ]

Logic programming with the stable model (answer set) semantics has been put forward as a novel constraint programming paradigm. It is well-known that constraint satisfaction problems (CSPs), the Hamiltonian circuit (HC) problern, and planning problems in STRIPS format can be encoded in domain restricted logic programs such that stable models of these programs correspond to solutions to the problems. In this thesis, we shall show that these problems can be encoded in such a way that the encoded programs are tight on every model of their Clark completions. According to a result in [3], this implies that stable models of these logic programs can be found by using propositional satisfiability (SAT) solvers on their Clark completions.

We also study some other encodings of the HC problem, and show that they are all equivalent with respect to extensional predicates. Some of the encodings are compared experinitmtally using SMODLES, SAT solvers, and ASSAT.

Next, loops in a logic program are considered. One of the main theoretical results of this thesis is that a stable model of a logic program can be found in polynomial time if the logic program has neither odd negative loops nor constraints. Such a program is also known as a call-consistent program. This result, is interesting comparing with the general case which is NP-hard. We also show that a logic program has at most one stable model if there is no even negative loop in the program.

Finally, we introduce a new splitting method that extracting a maximal order-consistent subset of a program. Such a splitting is useful in finding stable models of a normal logic program.