SATGRND

The tool is an adapter that can be used in between an ASP grounder and a SAT solver. The adapter can be used to instantiate clause specifications (also called clause programs) into ground clauses and thus to produce input sets for SAT solvers. Optionally, the output can be produced in the PB format, in the CPLEX format, or SMT library 2.0 format (QF_IDL or QF_BV), which enables the use of a wide variety of solvers but essentially writing a single clause program for each problem of interest.

Implementation

• The latest public version of SATGRND (v. 1.24, 1.21) has been tested with gringo (v. 3.0.4).
• To obtain a copy of gringo, please consult the Potassco website.
• We provide a shell script that will fetch gringo automatically under Linux.
• For obtaining a SAT solver, we refer to a number of websites: lingeling, minisat, owbo-acycglucose, clasp (in its SAT mode), etc.
• Technically, the transformation implemented by satgrnd enables the claculation of classical 2-valued models for a logic program and this is how clause programs get their intended meaning.

Simple Example

We suggest to write encodings in two parts: one for domains and one for the search part. Below we give an encoding of the very basic graph coloring problem. A database of directed edges will be added as facts. In the domain part, the nodes are inferred by the given domain rules. The search part expresses the choice of colors for each node: the number n of colors is a parameter to be specified from the command line of gringo (n=3 by default). Moreover, clauses enforce the coloring condition, i.e., any pair of nodes connected by an edge must have different colors.

#const n=3.

node(X) :- edge(X,Y).
node(Y) :- edge(X,Y).

colored(X,C) : C = 1..n :- node(X).
-colored(X,C) | -colored(Y,C) :- edge(X,Y), C = 1..n.

#hide.
#show colored/2.
#show -colored/2.

The predicates related with the search part (and their negations) must be kept visible. Only then satgrnd can assign the classical 2-valued semantics to them. The tool is compatible with smodels-format, and it is used as illustrated below.

$ planar 100 $RANDOM | fgrep -v vertex | sed 's/arc/edge/g' > graph-100.lp
$ gringo -cn=3 color.lp graph-100.lp | satgrnd | lingeling
$ gringo -cn=3 color.lp graph-100.lp | satgrnd | owbo-acycglucose -print-method=1 -verbosity=0

First, we create a random 100-vertex planar graph using planar (available in the misc section of ASPTOOLS). The structure of the graph is listed as facts, we remove the vertex-relation and rename the arc-relation of planar as the edge-relation for our encoding. Then we call gringo to ground the problem specification, translate it into CNF, and call a SAT solver (the command lingeling above) to check the existence of a coloring for the nodes. If owbo-acycglucose is used with the option flags indicated, the satisfying assignment will be printed out in symbolic form. For other SAT solvers, the following instructions may be useful.

Satisfying Assignments in Symbolic Form

The outputs of gringo and satgrnd include a mapping from atom numbers back to their symbolic names. If this is not understood by the back-end solver, the following example may be useful to understand the solution found:

$ gringo -cn=4 color.lp graph-100.lp | satgrnd > color.cnf
$ lingeling color.cnf | interpret -p -d color.cnf | egrep '^v'
v color(0,4) color(85,2) color(86,4) color(29,2) color(58,1)
v color(68,4) color(82,1) color(80,3) color(48,4) color(40,2) color(39,1)
...

The tool interpret (available in the misc section of ASPTOOLS) is a simple scanner that replaces numbers by their symbolic names (and omits negative numbers by default).

Sample Encodings

In each encoding, we have given the intuitive readings of predicates to help reading. There are basically three sections in each file: domain rules, clauses determining solutions, and solution extraction. Clauses typically begin with a literal of interest (having to become true if the rest of the clause is falsified).

• Graph coloring with a sample planar random graph having 100 nodes (obtained and used above)
• The famous n-queens problem
• Solving SuDoku puzzles, e.g., using Gordon Royle's clues
• Forming acyclic graphs (undirected forests) with n nodes
• Optimal basic block instruction scheduling with a small sample instance
• Full propositional logic using function symbols and Tseitin transformation
• Haplotype inference with an experimental encoding for both ASP and MaxSAT(PB) solvers (see the full benchmark set for details, 118MB)

Related Publications

M. Gebser, T. Janhunen, R. Kaminski, T. Schaub, and S. Tahsharrofi: Writing Declarative Specifications for Clauses. In Proceedings of the 15th European Conference on Logics in Artificial Intelligence (JELIA'16), 256—271, Larnaca, Cyprus, November 2016 (slides). Previous version presented at the 3rd International Workshop on Grounding, Transforming, and Modularizing Theories with Variables (GTTV'15), Lexington, Kentucky, September 2015 (slides).

Applications of SATGRND

B. Bogaerts, T. Janhunen, and S. Tasharrofi: Stable-Unstable Semantics: Beyond NP with Normal Logic Programs. Theory and Practice of Logic Programming, 16(5—6), 570—586, 2016. Special issue on ICLP'16.

B. Bogaerts, T. Janhunen, and S. Tasharrofi: Declarative solver development: Case studies. In Proceedings of the 15th International Conference (KR'16), 74—83, Cape Town, South Africa, April 2016.

B. Bogaerts, T. Janhunen, and S. Tasharrofi: Solving QBF instances with nested SAT solvers. In Proceedings of the AAAI-16 Workshop on Beyond NP, Phoenix, Arizona, USA, February 2016.

T. Janhunen, S. Tasharrofi, and E. Ternovska: SAT-to-SAT: Declarative extension of SAT solvers with new propagators. In Proceedings of the 30th AAAI Conference on Artificial Intelligence (AAAI'16), 978—984, Phoenix, Arizona, USA, February 2016.