Though the declarative semantics of both explicit and nonmonotonic negation in logic
programs has been studied extensively, relatively little work has been done on computation
and implementation of these semantics. In this paper, we study three different approaches
to computing stable models of logic programs based on mixed integer linear programming
methods for automated deduction introduced by R. Jeroslow. We subsequently discuss the
relative efficiency of these algorithms. The results of experiments with a prototype
compiler implemented by us tend to confirm our theoretical discussion. In contrast to
resolution, the mixed integer programming methodology is both fully declarative and handles
reuse of old computations gracefully. We also introduce, compare, implement, and experiment
with linear constraints corresponding to four semantics for "explicit" negation in logic
programs: the four-valued annotated semantics, the Gelfond-Lifschitz semantics, the
over-determined models, and the classical logic semantics. Gelfond and Lifschitz argue for
simultaneous use of two modes of negation in logic programs, "classical" and "nonmonotonic",
so we give algorithms for computing "answer sets" for such logic programs too.