Quick-Start

Be sure that you have newground installed. Then create a logic program file test.lp:

a(1).
a(2).
b(1).

#program rules.

c(X) :- a(X), not b(X).

Note that the part above #program rules is grounded by traditional means, whereas the part below is grounded via Body-decoupled Grounding.

With test.lp saved to disk you can use newground to create the rewritten program:

$ newground test.lp

The output should be:

$ newground test.lp
a(1).
a(2).
b(1).
r3_X(2) | r3_X(1).
r3_X(2) :- sat.
r3_X(1) :- sat.
sat_r3 :- r3_X(2),c(2).
sat_r3 :- r3_X(1),c(1).
sat_r3 :- r3_X(2),not a(2).
sat_r3 :- r3_X(1),not a(1).
sat_r3 :- r3_X(2),b(2).
sat_r3 :- r3_X(1),b(1).
domain_rule_3_variable_X(2).
domain_rule_3_variable_X(1).
{c3(X) : domain_rule_3_variable_X(X)} .
c(X) :- c3(X).
r3_unfound(2) :- not a(2).
r3_unfound(1) :- not a(1).
r3_unfound(2) :- b(2).
r3_unfound(1) :- b(1).
:- not sat.
sat :- sat_r3.
:- c3(2), #sum{1,0 : r3_unfound(2)} >=1 .
:- c3(1), #sum{1,0 : r3_unfound(1)} >=1 .
dom(1).
dom(2).
#show a/1.
#show b/1.
#show c/1.

You can directly save the output to disk by e.g.:

$ newground test.lp > output.lp

By e.g. using clingo (or idlv), you can convince yourself that the answer-sets are the same. Note that the answer-sets are equal with respect to the intersection of the output of the BDG-reduction with the predicates of the original program. To simulate this behavior we use the –project option, together with the show statements from the output.

$ clingo --project --model 0 output.lp
clingo version 5.6.2
Reading from output.lp
Solving...
Answer: 1
a(1) a(2) b(1) c(2)
SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.001s

When comparing to the original program be sure to remove the #program rules. line, by e.g., creating a copy of test.lp (test_2.lp) and removing the line there. Then the outputs are the same.

$ clingo --project --model 0 test_2.lp
clingo version 5.6.2
Reading from test_2.lp
Solving...
Answer: 1
a(1) a(2) b(1) c(2)
SATISFIABLE

Models       : 1
Calls        : 1
Time         : 0.000s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s