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.
gringo, please consult the Potassco website.
gringoautomatically under Linux.
satgrndenables the claculation of classical 2-valued models for a logic program and this is how clause programs get their intended meaning.
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
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.
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.
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
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
section of ASPTOOLS). The structure of the graph is listed as facts, we
remove the vertex-relation and rename the arc-relation
planar as the edge-relation for our encoding.
gringo to ground the problem specification, translate
it into CNF, and call a SAT solver (the command
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.
The outputs of
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)
(available in the
section of ASPTOOLS)
is a simple scanner that replaces numbers by their symbolic names
(and omits negative numbers by default).
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).
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).
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.