Answer Set Programming with Clause Learning

1. Babovich, Y., Erdem, E., Lifschitz, V.: Fage’s Theorem and Answer Set Programming. In: Proc. Int’l. Workshop on Non-Monotonic Reasoning (2000)

   Google Scholar 

2. Babovich, Y., Maratea, M.: Cmodels-2: SAT-based Answer Set Solver Enhanced to Non-tight Programs, Available from http://www.cs.utexas.edu/users/tag/cmodels.html

3. Bayardo, R., Schrag, R.: Using CSP look-back techniques to solve real-world SAT instances. In: Proc. of the Int’l. Conf. on Automate Deduction (1997)

   Google Scholar 

4. Clark, K.: Negation as failure. In: Gallaire, H., Minker, J. (eds.) Logic and Data Bases, pp. 293–322. Plenum Press, New York (1978)

   Google Scholar 

5. Davis, M., Logemann, G., Loveland, D.: A Machine Program for Theorem Proving. Communications of the Association of Computing Machinery 5, 394–397 (1962)

   MATH  MathSciNet  Google Scholar 

6. Eiter, T., Faber, W., Leone, N., Pfeifer, G.: Declarative Problem-Solving Using the DLV System. In: Minker, J. (ed.) Logic-Based Artificial Intelligence, pp. 79–103 (2000)

   Google Scholar 

7. Fages, F.: Consistency of Clark’s completion and existence of stable models. J. Methods of Logic in Computer Science 1, 51–60 (1994)

   Google Scholar 

8. Giunchiglia, E., Maratea, M., Tacchella, A.: Look-Ahead vs. Look-Back techniques in a modern SAT solver. In: SAT 2003, Portofino, Italy, May 5-8 (2003)

   Google Scholar 

9. Goldberg, E., Novikov, Y.: BerkMin: a Fast and Robust Sat–Solver. Design Automation and Test in Europe (DATE), 142–149 (2002)

   Google Scholar 

10. Lin, F., Jicheng, Z.: On Tight Logic Programs and Yet Another Translation from Normal Logic Programs to Propositional Logic. In: Proc. of IJCAI 2003 (2003) (to appear)

    Google Scholar 

11. Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. In: Proc. of the 18th Nat’l. Conf. on Artificial Intelligence, AAAI 2002 (2002)

    Google Scholar 

12. Marques-Silva, J.P., Sakallah, K.A.: GRASP: A Search Algorithm for Propositional Satisfiability. IEEE Trans. on Computers 48(5), 506–521 (1999)

    Google Scholar 

13. Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: Proc. of the 38th Design Automation Conf., DAC 2001 (2001)

    Google Scholar 

14. Niemela, I., Simons, P., Syrjanen, T.: Smodels: a system for answer set programming. In: Proc. of the 8th Int’l. Workshop on Non-Monotonic Reasoning (2000)

    Google Scholar 

15. Niemela, I.: Logic programming with stable model semantics as a constraint programming paradigm. Annals of Mathematics and Artificial Intelligence 25(3-4), 241–273 (1999)

    Article  MathSciNet  Google Scholar 

16. Simons, P.: Extending and Implementing the Stable Model Semantics. PhD dissertation, Helsinki University of Technology (2000)

    Google Scholar 

17. Velev, M., Bryant, R.: Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 37–53. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

18. Zhang, H.: SATO: An Efficient Propositional Prover. In: Proc. of Int’l. Conf. on Automated Deduction (1997)

    Google Scholar 

19. Zhang, L., Madigan, C., Moskewicz, M., Malik, S.: Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. In: Proc. of ICCAD 2001 (2001)

    Google Scholar 

20. ASSAT code, available from http://assat.cs.ust.hk/

21. Cmodels code, available from http://www.cs.utexas.edu/users/tag/cmodels.html

22. Chaff2 code, available from http://www.ee.princeton.edu/chaff/index1.html

23. Simo code is included in the Cmodels-2 distribution, See also http://www.mrg.dist.unige.it/sim/simo/

Download references