SAT-based ASP Solving and Optimization via a General Transitive Closure Framework

Answer set programming (ASP) in the NP fragment can be solved by translating into propositional satisfiability (SAT). However, for non-tight programs, this requires additional encodings to enforce acyclicity of the underlying dependency graph, making acyclicity handling a key challenge in translating ASP encodings of decision and optimization problems into SAT and maximum satisfiability (MaxSAT). Various SAT encodings of acyclicity exploiting structural graph properties have recently been proposed for various settings. Focusing on ASP, we show that such encodings are captured by a generalized transitive closure framework. The framework can be instantiated for obtaining various types of refined transitive closure encodings. We consider four concrete instantiations framework, analyzing their correctness and size. Putting the framework into practice, we show through extensive empirical evaluation that current state-of-the-art SAT and MaxSAT solvers are competitive with and often even outperform state-of-the-art native ASP solvers on both decision and optimization problems.