Answer Set Programming Based on Propositional Satisfiability

Armando, A., Castellini, C., Giunchiglia, E.: SAT-based procedures for temporal reasoning. In: Lecture Notes in Computer Science, vol. 1809, pp. 97–108 (1999)

Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: The SAT-based approach to separation logic. J. Autom. Reason. To appear (2005)

Babovich, Y., Erdem, E., Lifschitz, V.: ‘Fages’ theorem and answer set programming. In: Proc. NMR, (2000)

Baral, C., Gelfond, M., Scherl, R.: ‘Using answer set programming to answer complex queries. In: Workshop on Pragmatics of Question Answering at HLT-NAAC2004, (2004)

Barrett, C.W., Dill, D.L., Stump, A.: Checking satisfiability of first-order formulas by incremental Translation to SAT. In: Brinksma, E., Larsen, K.G. (eds.), 14th International Conference on Computer Aided Verification (CAV), vol. 2404 of Lecture Notes in Computer Science, pp. 236–249. Springer, Berlin Heidelberg New York (2002)

Bayardo, R.J. Jr, Schrag, R.C.: Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conference (AAAI-97/IAAI-97). Menlo Park, California, pp. 203–208. AAAI (1997)

Ben-Eliyahu, R., Dechter, R.: Propositional semantics for disjunctive logic programs. Ann. Math. Artif. Intell. 12, 53–87 (1996)

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

Ştefănescu, A., Esparza, J., Muscholl, A.: Synthesis of distributed algorithms using asynchronous automata. In: Proc. CONCUR'03, vol. 2761, pp. 27–41. Springer (2003)

Davis, M., Logemann, G., Loveland, D.W.: A machine program for theorem proving. Commun. ACM 5(7), 394–397 (1962)

de Moura, L., Rueß, H., Sorea, S.: Lazy theorem proving for bounded model checking over infinite domains. In: Voronkov, A. (ed.), Automated Deduction – CADE-18, vol. 2392 of Lecture Notes in Computer Science, pp. 438–455. Springer (2002)

Dixon, H.E., Ginsberg, M.L., Luks, E.M., Parkes, A.J.: Generalizing Boolean satisfiability II: Theory. J. Artif. Intell. Res. (JAIR) 22, 481–534 (2004)

Dowling, W., Gallier, J.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 3, 267–284 (1984)

Eén, N., Sörensson, N.: An extensible SAT-solver'. In: Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5–8, 2003 Selected Revised Papers, pp. 502–518, (2003)

Erdem, E.: Theory and applications of answer set programming. Ph.D. thesis, University of Texas at Austin (2002)

Erdem, E., Lifschitz, V.: ‘Fages’ theorem for programs with nested expressions. In: Proc. International Conference on Logic Programming, pp. 242–254, (2001)

Faber, W., Leone, N., Pfeifer, G.: Experimenting with heuristics for answer set programming. In: IJCAI, pp. 635–640 (2001)

Fages, F.: Consistency of Clark's completion and existence of stable models. J. Methods Logic Comput. Sci. 1, 51–60 (1994)

Ferraris, P., Lifschitz, V.: Weight constraints as nested expressions. Theory and Practice of Logic Programming 5, 45–74 (2005)

Gebser, M., Schaub, T.: Loops: Relevant or redundant?. In: Proceedings of 8th International Conference on Logic Programming and Nonmonotonic Reasoning, pp. 53–65. Springer (2005)

Gelfond, M., Lifschitz, V.: The stable model semantics for logic programming. In: Kowalski, R., Bowen, K. (eds.) Logic Programming: Proceedings of the Fifth Int'l Conf. and Symp., pp. 1070–1080, (1988)

Gelfond, M., Lifschitz, V.: Classical negation in logic programs and disjunctive databases. New Gener. Comput. 9, 365–385 (1991)

Gent, I., Maaren, H.V., Walsh, T. (eds.) SAT 2000. Highlights of Satisfiability Research in the Year 2000. IOS (2000)

Giunchiglia, E., Giunchiglia, F., Tacchella, A.: SAT-based decision procedures for classical modal logics. J. Autom. Reason. 28, 143–171 (2002). Reprinted in [23]

Giunchiglia, E., Maratea, M.: On the relation between SAT and ASP procedures (or, between smodels and cmodels). In: Proceedings of the 21th International Conference on Logic Programming (ICLP), pp. 37–51. Springer (2005a)

Giunchiglia, E., Maratea, M.: Evaluating search strategies and heuristics for efficient answer set programming. In: Advanced in Artificial Intelligence: Conference of the Italian Association for Artificial Intelligence, AI*IA '05, Milan, Italy, September 20–23, 2005, Proceedings, pp. 37–51. Springer (2005b)

Giunchiglia, E., Maratea, M., Lierler, Y.: SAT-based answer set programming. In: Proc. 19th National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25-29, 2004, San Jose, California. AAAI, The MIT Press (2004)

Giunchiglia, E., Maratea, M., Tacchella, A.: In: Effectiveness of look-ahead techniques in a modern SAT solver. In: 9th International Conference on Principles and Practice of Constraint Programming (CP-03), pp. 842–846, (2003)

Giunchiglia, E., Maratea, M., Tacchella, A., Zambonin, D.: Evaluating search heuristics and optimization techniques in propositional satisfiability. In: Automated Reasoning, First International Joint Conference (IJCAR), vol. 2083 of Lecture Notes in Computer Science, pp. 347–363. Springer (2001)

Goldberg, E., Novikov, Y.: BerkMin: A fast and robust SAT solver. In: Proc. of the Design, Automation and Test in Europe Conference and Exposition 2003, pp. 142–149. IEEE Computer Society (2003)

Heljanko, K., Niemelä, I.: Bounded LTL model checking with stable models. Theory and Practice of Logic Programming 3(4&5), 519–550 (2003). Also available as (CoRR: arXiv:cs.LO/0305040)

Janhunen, T.: Translatability and intranslatability results for certain classes of logic programs'. Series A: Research report 82, Helsinki University of Technology, Laboratory for Theoretical Computer Science, Espoo, Finland (2003)

Janhunen, T.: Representing normal programs with clauses. In: Proc. of 16th European Conference on Artificial Intelligence, ECAI 2004, pp. 358–362. IOS (2004)

Janhunen, T., Niemelä, I.: GnT – A solver for disjunctive logic programming. In: Proc. of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR), pp. 331–335. Springer (2004)

Janhunen, T., Niemelä, I., Seipel, D., Simons, P., You, J.-H.: Unfolding partiality and disjuntion in stable model semantics. Accepted to the ACM Transaction on Computational Logic (2005)

Lahiri, S.K., Seshia, S.A., Bryant, R.E.: Modeling and verification of out-of-order microprocessors in UCLID. In: Formal Methods in Computer-Aided Design, 4th International Conference, FMCAD 2002, Portland, Oregon, November 6–8, 2002, Proceedings, pp. 142–159 (2002)

Le Berre, D., Simon, L.: The essentials of the SAT'03 Competition'. In: Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5–8, 2003 Selected Revised Papers, vol. 2919 of LNCS (2003)

Lee, J., Lifschitz, V.: Loop formulas for disjunctive logic programs. In: Proc. ICLP-03, (2003)

Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV system for knowledge representation and reasoning. Accepted to ACM Transactions on Computational Logic (ToCL) (2005)

Li, C.M., Anbulagan: Heuristics based on unit propagation for satisfiability problems. In: Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97). San Francisco, pp. 366–371, Morgan Kaufmann (1997)

Lierler, Y.: Disjunctive answer set programming via satisfiability. In: Answer Set Programming, vol. 142 of CEUR Workshop Proceedings (2005)

Lierler, Y., Lifschitz, V.: Computing answer sets using program completion. Available at http://www.cs.utexas.edu/users/tag/cmodels.html , 2003

Lifschitz, V.: Foundations of logic programming. In: Brewka, G. (ed.), Principles of Knowledge Representation. CSLI, pp. 69–128, (1996)

Lifschitz, V., Razborov, A.: Why are there so many loop formulas? ACM Transactions on Computational Logic, 7, 261–268 (2006)

Lifschitz, V., Tang, L.R., Turner, H.: Nested expressions in logic programs. Ann. Math. Artif. Intell. 25, 369–389 (1999)

Lin, F., Zhao, J.: On tight logic programs and yet another translation from normal logic programs to propositional logic. In: Proc. IJCAI (2003a)

Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT Solvers. In: Proc. 18th National Conference on Artificial Intelligence and Fourteenth Conference on Innovative Applications of Artificial Intelligence (AAAI/IAAI-02). Menlo Park, California, pp. 112–118. AAAI (2002)

Lin, F., Zhao, Y.: Answer set programming phase transition: A study on randomly generated programs. In: Proc. ICLP, (2003b)

Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by SAT solvers. Artif. Intell. 157(1–2), 115–137 (2004)

Lloyd, J., Topor, R.: Making Prolog more expressive. J. Log. Program. 3, 225–240 (1984)

Marek, V., Subrahmanian, V.: The relationship between logic program semantics and non-monotonic reasoning. In: Levi, G., Martelli, M. (eds.) Logic Programming: Proceedings of the 6th Int'l Conf., pp. 600–617, (1989)

Marek, V., Truszczynski, M.: Stable models as an alternative programming paradigm. In: The Logic Programming Paradigm: A 25 Years perspective, Lecture Notes in Computer Science. Springer (1999)

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Proc. 38th Design Automation Conference (DAC'01), pp. 530–535 (2001)

Niemelä, I.: Logic programs with stable model semantics as a constraint programming paradigm. Ann. Math. Artif. Intell. 25, 241–273 (1999)

Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6–10, 2005, Proceedings, pp. 321–334, (2005)

Nogueira, M., Balduccini, M., Gelfond, M., Watson, R., Barry, M.: An A-Prolog decision support system for the space shuttle. In: Working Notes of the AAAI Spring Symposium on Answer Set Programming, (2001)

Plaisted, D., Greenbaum, S.: A structure-preserving clause form translation. J. Symbol. Comput. 2, 293–304 (1986)

Sheridan, D.: The Optimality of a Fast CNF Conversion and its use with SAT. In: Proceedings of SAT, International Conference on Theory and Applications of Satisfiability Testing, Vancouver (Canada) (2004)

Siekmann, J., Wrightson, G. (eds.) Automation of Reasoning: Classical Papers in Computational Logic 1967–1970, Vol. 1–2. Springer (1983)

Silva, J.P.M., Sakallah, K.A.: GRASP – A New Search Algorithm for Satisfiability. Technical report, University of Michigan, (1996)

Simons, P., Niemelä, I., Timo, S.: Extending and implementing the stable model semantics. Artif. Intell. 138(1–2), 181–234 (2002)

Syrjanen, T.: Lparse Manual. http://www.tcs.hut.fi/Software/smodels/lparse.ps.gz , 2003

Tseitin, G.: On the complexity of proofs in propositional logics. Semin. Math. 8 (1970). Reprinted in [59].

Ward, J., Schlipf, J.S.: Answer set programming with clause learning. In: Logic Programming and Nonmonotonic Reasoning, 7th International Conference, LPNMR 2004, Fort Lauderdale, Florida, January 6–8, 2004, Proceedings, pp. 302–313 (2004)

Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: Efficient conflict driven learning in a Boolean satisfiability solver. In: International Conference on Computer-Aided Design (ICCAD'01), pp. 279–285, (2001)