\toolnamelp2pb: 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 [34] of a logic program can be used to encode search problems [60, 63, 50]. ASP is rapidly gaining adoption, with applications in domains such as decision support for the Space Shuttle [64], product configuration [76], phylogenetic inference [46, 12], knowledge management [38], e-Tourism [66], biology [33], robotics [6], and machine learning [42, 13].

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 \myciteAspCore2, 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 [\reftogringo, \reftoDLV] and solvers [\reftoclasp, \reftowasp, \reftominisatid] — 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) \mycitecdcl 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. In fact, the relation goes two ways, \toolnameclasp, a native ASP solver has long been one of the best performing SAT solvers. A recent example of such positive reinforcement between domains is found in recent constraint ASP systems [\reftoclingcon], which use techniques from SAT modulo theories \myciteSMT and from constraint programming \myciteCP – in particular, lazy clause generation \mycitelcg.

Next to native solvers, also various ASP tools are available based on translations to other formalisms: to SAT \mycitelp2sat, to difference logic \mycitelp2diff, to mixed integer programming \mycitelp2mip, and to SAT modulo acyclicity \mycitelp2acyc. Our current work fits in this line, by translating answer set programs into (linear) pseudo-Boolean (PB) constraints \mycitePB.

Most modern ASP solvers are built on conflict-driven clause learning and thus on the resolution proof system. This also holds for ASP solvers with native support for aggregates, which typically employ lazy clause generation techniques, essentially compiling their theory lazily into clauses and henceforth relying on the underlying CDCL solver. The advantage of building on CDCL technology is that this has been researched intensely, and the simplicity of using only clauses allows for highly optimized implementations, resulting in efficient, well-engineered solvers. The disadvantage is that the resolution proof system is known to be weak; for several very simple problems, resolution proofs are exponentially large; the most notorious such problem is the pigeon hole problem. In practice this means that modern CDCL solvers can, for instance, not solve the problem “do 15 pigeons fit in 14 holes?” One way to avoid this limitation, is using symmetry exploitation methods, which are well-researched in SAT [2, 20, 19, 62], and have also been ported to ASP [22, 18], but the detection of symmetries is often very brittle, e.g. , adding redundant constraints often removes symmetries. Another option is using a stronger proof system, such as the cutting planes proof system \myciteCuttingPlanes. This proof system works on linear constraints over the integers, or, when restricted to $0-1$ variables, on so-called pseudo-Boolean constraints. Recent research in the field of pseudo-Boolean solving has resulted in a new and efficient solver, \toolnameRoundingSAT\myciteRoundingSAT, that builds on previous work to integrate conflict-driven search with the cutting plane proof system \mycite\reftoPRS,tcad/ChaiK05,\reftojsat/SheiniS06,jsat/ManquinhoS06,\reftoSAT4J. This recent improvement in psuedo-Boolean solving triggers the question whether answer set programming could also benefit from these techniques.

The main contribution of this paper is the introduction and experimental validation of a new tool \toolnamelp2pbthat translates ground logic programs into pseudo-Boolean theories. This tool is valuable both for the ASP community and for the PB community. For ASP, it enables the use of an extra class of solvers. Furthermore, since we translate into the well-accepted OPB standard format for pseudo-Boolean problems¹¹1See http://www.cril.univ-artois.fr/PB10/format.pdf., compatibility of future pseudo-Boolean solvers is obtained for free, allowing us to quickly test the potential of novel PB solving techniques for logic programming. Additionally, the OPB format is supported by important industrial tools such as \toolnamegurobi\mycite\reftogurobi. For the PB community, this tool provides access to a new set of applications and benchmarks. Additionally, it establishes answer set programming as a modelling language for PB solvers, thereby bypassing the need to write by hand a program that generates benchmarks for every new class of benchmarks considered.

We experimentally validate \toolnamelp2pbon two classes of benchmarks. On novel ASP models of four benchmark families where the difference between cutting planes and resolution is known to be essential, our approach, unsurprisingly, outperforms traditional ASP solvers. On benchmarks from the latest ASP competition, we find that overall, traditional ASP solvers are still more efficient, but several benchmark families (mainly optimization problems) are found where the cutting plane proof system pays off.

The rest of this paper is structured as follows. In Section 2, we introduce preliminaries on ASP and pseudo-Boolean constraints. In Sections 3 and 4, we discuss our translation and its implementation respectively. Section 5 contains our experiments. In Section 6, we discuss some closely related work and we conclude in Section 7.

A vocabulary is a set of symbols, also called atoms; vocabularies are denoted by $\sigma,\tau$. A literal is an atom $p$ or its negation $\bar{p}$. An interpretation $\struct$ of a vocabulary \mσis a subset of $\m{\sigma}$. We use the truth values true ($\ltrue$) and false ($\lfalse$) and will identify $\ltrue$ with $1$ and $\lfalse$ with $0$, as is common in pseudo-Boolean theories. The truth value of an atom $p\in\sigma$ in an interpretation \struct(denoted $p^{\struct}$) is $1$ if $p\in\struct$ and $0$ otherwise. The truth value of literals, conjunctions of literals, and clauses (disjunctions of literal) are defined as usual.

Our tool accepts input in the \lparse–\smodelsintermediate format \mycitelparsemanual. In case disjunction is present in the head of a rule, it is first eliminated using \toolnamelpshift [41]. Of course, this is not correct in general, but only for the classes of programs considered here, where disjunction is head-cycle free (or, more general, head-elementary set free). The input is split into two parts: one part contains all rules containing aggregates (in the \lparse–\smodelsformat these are the constraint rules, weight rules, and minimize rules) while the other part contains all other rules, as well as the other information present in the \lparse–\smodelsintermediate format (the symbol table, and compute statements). For constraint and weight rules (the former are a special case of the latter) in the first part, the transformation from Proposition 2 is used to split them into a choice rule (the combination of the rules $h\lrule\bar{h^{\prime}},h^{\prime}\lrule\bar{h}$) which is added to the second part and two pseudo-Boolean constraints as described below Proposition 2 to be included in the output. A minimize statement directly corresponds to a linear term, and is hence translated directly into a corresponding minimisation statement in the OPB format. As mentioned in Section 3, we make use of existing tools as much as possible. Therefore, the second part (with the additional rules) is then given to the pipeline $\toolname{lp2normal}\mid\toolname{lp2lp2}\mid\toolname{lp2sat}$; the combination of these three tools translates a non-disjunctive logic program into an equivalent propositional theory in CNF [11, 41]. Our tool subsequently transforms each clause produced by \toolnamelp2satinto a simple linear constraint and combines this with the linear constraints obtained from the first part to produce a complete pseudo-Boolean theory that characterizes exactly the stable models of the original logic program. We do not describe the complete implementation, but instead discuss a couple of peculiar points.

The experiments and set-ups were chosen to shine light on following research questions:

1. 1.

   How well do modern Pseudo-Boolean solvers perform on ASP models of problems where cutting planes is known to be stronger than resolution?

2. 2.

   To which extent is the cutting plane proof system promising for traditional ASP?

The benchmarks were ran on the VUB Hydra cluster. Each solver call was assigned a single core on a 10-core INTEL E5-2680v2 (IvyBridge) processor, a timelimit of 20 minutes and a memory-limit of 12GB, thereby matching the limits of the latest ASP competition \myciteASPComp7. The following benchmarks were used:

1. 1.

   Four benchmark families inspired by the work of Elffers et al. [24], using problems described there, as well as the same types of instances as in that paper (e.g., the shapes of the graphs considered). These four families are known to be (with the right encoding) easy for the cutting-plane proof system in the sense that polynomial cutting plane proofs exist, but are hard for CDCL solvers. All our ASP encodings are straightforward and use aggregates. The four families are:

   Pigeon Hole

   The problem here is to fit $n$ pigeons in $m$ holes with at most one pigeon residing in each hole. All our instances are unsatisfiable with $n=m+1$.

   Even Colouring

   This problem takes as input a connected graph in which each vertex has an even degree. The problem is to determine if a black-white colouring of the edges exists such that each nodes has the same number of incident black and white edges. The problem is satisfiable if and only if the number of edges is even. Our instances are long toroidal grids in which one auxiliary vertex is inserted to break a single edge in two. All these instances are thus unsatisfiable.

   Vertex Cover

   The input to this problem is a connected graph and a number $S$. The problem is to decide if a size $S$ vertex cover exists, i.e., a subset of the nodes of size $S$ such that each edge is incident to some vertex in the set. We again use long toroidal grids, here with an even number of rows; in that case an instance is satisfiable if and only if $S\geq m\cdot\lceil n/2\rceil$ where $m$ is the number of rows and $n$ the number of columns. All our instances are unsatisfiable and have $S=m\cdot\lceil n/2\rceil-1$.

   Dominating Set

   This problem again takes a graph and a number $S$ as input. The problem is to decide if the input graph has a size-$S$ dominating set, i.e., a set of vertices such that each vertex is either in the set or adjacent to a vertex in teh set. Our instances are long hexagonal grid. All our instances are unsatisfiable and have $S=\lfloor v/4\rfloor$ where $v$ is the number of vertices in the graph.

   The instances selected in these four benchmark families all scale linearly, that is, after starting from a small instance, we increase the size of the instance by a fixed step size.

2. 2.

   All decision and optimization problems from the 2017 ASP competition \myciteASPComp7, which includes many benchmarks from earlier competitions, with the exception of:

   • •

     Problems including non head-cycle-free disjunction, since those were problems beyond the first level of the polynomial hierarchy that can hence not be translated compactly into pseudo-Boolean theories.

   • •

     The video streaming benchmark family, since it contains very high coefficients (higher than what \toolnameRoundingSATsupports).

   For each benchmark family, the 20 instances selected for the competition were used.

All benchmarks and instances are available at https://github.com/wulfdewolf/lp2pb_benchmarks.

We compared four solver configurations:

• •
  \m\toolname

  C\toolnamec\xspace: $\gringo\mid\toolname{clasp}$

• •
  \m\toolname

  C\toolnamepb\xspace: $\gringo\mid\toolname{lp2pb}\mid\toolname{RoundingSAT}$

• •
  \m\toolname

  C\toolnamen-pb\xspace: $\gringo\mid\toolname{lp2normal}\mid\toolname{lp2lp2}\mid\toolname{lp2sat}\mid\toolname{RoundingSAT}$

• •
  \m\toolname

  C\toolnamen-c\xspace: $\gringo\mid\toolname{lp2normal}\mid\toolname{lp2lp2}\mid\toolname{clasp}$

Of each of the used tools, the latest available version was used, i.e. \gringo5.4.0, \toolnameclasp3.3.5, \toolnamelp2normal2.27, \toolnamelp2lp21.23, \toolnamelp2sat1.24, \toolnamelp2pb1.0²²2https://github.com/wulfdewolf/lp2pb, and \toolnameRoundingSATat commit fd464d43a³³3At the time of the writing, this commit has not been released yet. For reproducability, the binary can be found on our experiment github repository..

A comparison between \m\toolnameC\toolnamec\xspaceand \m\toolnameC\toolnamepb\xspaceshould give insights into how a state-of-the-art ASP solvers compares to a state-of-the-art pseudo-Boolean solver after our translation. Interpreting the results of \m\toolnameC\toolnamen-pb\xspacerequires some care. For decision problems, in \m\toolnameC\toolnamen-pb\xspace, the input given to \toolnameRoundingSATis a CNF. It is well-known that despite the fact that cutting planes can be exponentially more powerful than resolution, this power is not used by conflict-driven pseudo-Boolean solvers on CNF input, where they essentially produce resolution proofs (see e.g., [78]). For decision problems, a comparison between \m\toolnameC\toolnamen-pb\xspaceand \m\toolnameC\toolnamen-c\xspaceshould thus give an idea of the difference in engineering and optimizations between \toolnameRoundingSATand \toolnameclasp. For optimization problems, this comparison does not hold since bounds on the objective function that are added during branch-and-bound search are typically non-clausal. Finally, a comparison between \m\toolnameC\toolnamepb\xspaceand \m\toolnameC\toolnamen-pb\xspaceshould give an indication of how valuable the pseudo-Boolean constraints (coming from aggregates) are for \toolnameRoundingSAT, i.e., how much is gained by using our translation compared to a plain CNF translation.

There is a rich history of research on using SAT solvers to search for computing stable models of logic programs. One approach works by introducing loop formulas on-the-fly [53, 48, 37] and in fact lies at the basis of most modern native ASP solvers [\reftoclasp, \reftowasp]. Another approach is studying translations of ASP into SAT that are more compact than the (worst-case) exponential blow-up loop formulas induce [9, 52, 40, 44]. These translations introduce auxiliary variables; some of them induce a one-to-one correpondence between the stable models of the original program and the models of the obtained propositional theory, while others duplicate some models. What all these methods have in common is that aggregates are encoded into clause, either lazily (as done in native solvers, often following the lazy clause generation paradigm \myciteLCG), or eagerly, for instance by applying normalization tools [11] that eliminate the aggregates before the actual SAT-translation is called. Our work closely relates to the translation based approach. In fact, internally our tool makes use of the tools of Janhunen and Niemelä [44] to translate the part of the program without aggregates into SAT; the actual translation used can easily be changed in \toolnamelp2pb. The main difference with the standard translational approaches is that aggregates are not normalized but preserved.

Also \toolnameDLV2[3] has an option (--pre=wbo) to translate ASP programs into PB theories; however, this translation is limited to tight programs and it cannot handle multilevel optimisation problems.

Another related tool is \toolnamemingo\mycitemingo, which integrates answer set programming and mixed integer programming \myciteMIP, thus allowing more types of constraints (using non-Boolean variables) than PB theories. These non-Boolean variables are used, among others, to encode the level mapping characterization [55] that ensures stability of the obtained models. Unlike our translation, \toolnamemingodoes not guarantee a one-to-one correspondence between the models of the obtained theory and the stable models of the original program, making it unsuitable for model counting. Our approach does guarantee this, mainly by building on the guarantees from the used translation of aggregate-free logic programs to SAT [44]. Another difference is that part of the focus of \toolnamemingois on developing an extension of the ASP language in which mixed-integer constraints can be written directly in the program. Nowadays, this approach is common in various Constraint-ASP formalisms [23, 49, 7, 43, 70].

A final related tool is \toolnamepbmodels\mycitepbmodels, which also uses pseudo-Boolean solvers to find stable models. The main difference is that \toolnamepbmodelsis designed as a wrapper around a PB solver that iteratively calls the solver for supported models, next checks for stability and if the result is not stable, adds loop formulas, while \toolnamelp2pboutputs a translation that can be fed to a PB solver to be solved in a single solver call, which benefits the solver’s internal constraint learning mechanism.

One direction for future work is investigating an extension of our translation to support recursive aggregates. The semantics of recursive aggregates constitute an intense topic of debate, as can be witnessed by the number of papers written about them [27, 73, 65, 26, 36, 5]. However, for monotonic (and in fact, convex aggregates [57]), most of them agree — the notable exception being [36]. Hence, an extension of our tool that works for recursive aggregates under the condition that they be convex, would be valuable. The most lightweight way to achieve this would be to start from the translation of \mycitemingo, which builds on the level mapping of Liu and You [55], and modify it to use Boolean variables. An unresolved challenge in that case is how a one-to-one correspondence between the stable models of the program and the models of the resulting theory can be achieved.

Another interesting, but perhaps more ambitious direction for future work is to develop a new native ASP solver that uses the cutting plane proof system under the hood, for instance by developing an extension of \toolnameRoundingSATwith support for recursive rules.

To conclude, we presented a novel tool, called \toolnamelp2pb, to translate logic programs into pseudo-Boolean formulas and experimentally validated its performance on a large set of benchmarks. The results are mixed. On the one hand, overall traditional ASP solvers seem to outperform pseudo-Boolean solvers on the benchmark traditionally tackled with ASP. But on the other hand, a couple of benchmark families was identified on which pseudo-Boolean reasoning can provide a real advantage, thus warranting further research into using the cutting plane proof system in ASP solving.

The resources and services used in this work were provided by the VSC (Flemish Supercomputer Center), funded by the Research Foundation - Flanders (FWO) and the Flemish Government. We are very grateful to Jakob Nordström and Jo Devriendt for interesting discussions on this topic and for providing us with the latest version of \toolnameRoundingSAT.