LP2PB: Translating Answer Set Programs into Pseudo-Boolean Theories

Answer set programming (ASP) is a well-established knowledge representation formalism that grew from the observation that stable models [33] of a logic program can be used to encode search problems [59, 62, 49]. ASP is rapidly gaining adoption, with applications in domains such as decision support for the Space Shuttle [63], product configuration [75], phylogenetic inference [45, 11], knowledge management [37], e-Tourism [65], biology [32], robotics [5], and machine learning [41, 12]. The success of ASP can, to a large extend, be explained by two factors. The first factor is a rich, first-order language, ASP-Core2 [13], to express knowledge in, with an easy-to-understand modeling methodology known as generate-define-and-test. The second factor is the availability of a large number of reliable tools -- grounders [31, 46] and solvers [28, 3, 16] -- that allow to efficiently compute stable models of a given logic program. Throughout its history, ASP has always benefited from progress in other domains of combinatorial search. For instance, the addition of conflict-driven clause learning (CDCL) [60] to Boolean satisfiability (SAT) solvers is often recognized as one of the most important leaps forward in SAT solving; this technique was very quickly adopted in ASP.