Improved Encodings of Acyclicity for Translating Answer Set Programming into Integer Programming

Abstract

<p>In this work, we introduce novel translations of Answer Set Programming (ASP) into Integer Programming (IP). While building upon a previously introduced IP translation, we revisit the translation of acyclicity constraints essential for capturing answer sets precisely. By leveraging vertex elimination graphs, we demonstrate that a new translation of acyclicity can yield integer programs with a more restrictive linear relaxation compared to previous methods. This enhancement enables IP solvers to prune the search space more efficiently. Furthermore, we show how acyclicity can be expressed more concisely in IP given any feedback vertex set of the underlying dependency graph. Experimental results underscore the improved efficiency of our methods over the previously implemented translation. The new vertex elimination based translation with Gurobi as the back-end solver turns out competitive against Clingo, a state-of-the-art native ASP solver, in a number of non-tight Answer Set Optimization (ASO) benchmarks.</p>