Computing minimal answer sets w.r.t. a subset of atoms

[mahi045]

Can I compute (subset) minimal answer sets w.r.t. a subset of atoms (like this) using clingo?

Thanks in advance.

[rkaminsk]

I did not read the paper but your can compute subset minimal solutions with clingo. For example, to calculate subset minimal solutions over the shown atoms, you can use

clingo --dom-mod=false,show --enum-mode=domRec --heuristic=domain

@BenKaufmann and @javier-romero, is the call correct?

The idea is that the solver's decision heuristic picks atoms subject to subset minimization and makes them false as long as such atoms are available. Like this, the first solution found is subset minimal. The search can then be continued recording a nogood that prevents supersets of this solution.

You can also use heuristic directives in your program that prioritize assigning certain atoms and then just use --enum-mode=domRec or even record nogoods yourself via the API. Be sure to always use --heuristic=domain.

[mahi045]

@rkaminsk Thanks for your response. I have another question: does the domain heuristic also work with theory propagator? In my case, for given program $P$, the theory propagator adds clauses $X$ to the solver. Does the clingo computes subset minimal answer sets of $P$ satisfying clauses $X$? or clingo computes subset minimal answer sets of $P \cup X$ ?

[rkaminsk]

The domain heuristic should work just fine with propagators.

[javier-romero]

Clingo will compute subset minimal answer sets of $P \cup X$.

If you do not activate the heuristic, clingo computes answer sets of $P \cup X$. You can think that in this case clingo checks possible answer sets of $P \cup X$ in any order, until one is found to be an actual answer set.

If you activate the heuristic, then clingo checks the possible answer sets of $P \cup X$ in the order of subset minimality. Hence, when one actual answer set is found, it is guaranteed to be subset minimal among all answer sets.

Of course, clingo is much clever than that, and does not generate possible answer sets and check them, but I hope this gives an idea.

[mahi045]

@rkaminsk @javier-romero I appreciate the detailed response. I would like to clarify one point: Do the subset minimal answer sets of $P \cup X$ belong to the subset minimal answer sets of $P$ (is it $\subseteq$-relation)?

If it does not hold, then adding clauses $X$ generates a new subset minimal answer set in $P$, or the theory propagator introduces some new subset minimal answer sets.

[rkaminsk]

Not sure what you mean. The propagator has to be seen as part of the program. You cannot simply use it to add "queries" on top of the subset minimal answer sets as this would raise complexity.

[javier-romero]

Adding to what Roland said, you should see the propagator as a set of clauses.

Then we can talk about X simply as a set of clauses.

In this case, the subset minimal answer sets of $P \cup X$ are not necessarily subset minimal answer sets of $P$.

For example, take $P$ to be the program that has the choice rule {a}. and X to consist of the clause {a} that enforces the atom a to be true:

• Program $P \cup X$ has a unique answer set {a} which is also its unique subset minimal answer set.
• Program $P$ has two answer sets, {} and {a}. The first one is the unique subset minimal answer set of $P$.

So, the minimal answer set {a} of $P \cup X$ is not a minimal answer set of $P$.

According to this, one can say what you said above: adding clauses generates a new minimal answer set of $P$ ({a} in the example), and the propagator (indirectly) introduces some new subset minimal answer set ({a} in the example).

[mahi045]

@rkaminsk @javier-romero Thank you for the detailed explanation. I understand that introducing the clause will result in new subset minimal answer sets. However, in my situation, I aim to preserve all subset minimal answer sets of $P$ that satisfy the clauses $X$, without introducing new ones.

Could you advise on the complexity of modifying Clingo's implementation to support this requirement?

[rkaminsk]

If you have two normal programs P and Q, it should be possible to write a disjunctive program that captures the subset minimal stable models of P filtered by Q. It is just very cumbersome to write such a program. Javier might have some tools ready. Another downside is that this probably won't scale to large problems.

Another approach could be to just compute the subset minimal solutions and then filter them in a post processing step. Scaling is probably also an issue here.

[javier-romero]

You can find the subset minimal answer sets that contain some atom query using asprin, here is an example:

$ cat query.lp 
dom(1..2).                                                                                                                                                                                                                                           
1 {a(X) : dom(X)}.                                                                                                                                                                                                                                   
query :- a(X) : dom(X).                                                                                                                                                                                                                              
#preference(p,subset){a(X)}.                                                                                                                                                                                                                         
#optimize(p).                                                                                                                                                                                                                                        

$ asprin query.lp 0
asprin version 3.1.1
Reading from query.lp
Solving...
Answer: 1
dom(1) dom(2) a(2)
OPTIMUM FOUND
Answer: 2
dom(1) dom(2) a(1)
OPTIMUM FOUND

Models       : 2
  Optimum    : yes
  Optimal    : 2
Calls        : 7
Time         : 0.106s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.104s
$ asprin query.lp 0 --meta=query
asprin version 3.1.1
Reading from query.lp
Solving...
UNSATISFIABLE

Models       : 0
  Optimum    : no
Calls        : 1
Time         : 0.074s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.074s

This should work for your case, writing some rules that derive query whenever all clauses in X are satisfied.

The implementation translates the problem to a disjunctive logic program and uses clingo to solve it. The problem is that, as Roland said, this does not scale well.

One could also use:

• https://github.com/potassco/qasp2qbf

for this task.

Another different question arises if you do not want to write the clauses in X explicitly in a logic program, but you want to use a propagator for that.

In that case, there may be some sophisticated approach that I am not aware of, but all I can suggest is to do as Roland said: iterate over the subset minimal models, and then check with the propagator whether they satisfy the clauses generated by the propagator.

[mahi045]

Thank you for the information you provided.