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.