Projected AllSAT with partial solutions in clingo

[masinag]

Hi, I have a couple of questions on clingo, and more in general on ASP.

In the SAT community, the AllSAT task is the task of finding all the solutions (models) of a propositional formula. For example, given (a | b | ~c) & (~a | b | c) & (~a | ~b) then, all the models of the formula are

 a ~b  c
~a  b  c
~a  b ~c
~a ~b ~c

Since the number of models can grow exponentially, it is typically convenient to enumerate partial models, i.e., models where only a subset of the atoms are assigned a truth value. In the example above, a possible set of partial models is

 a ~b  c
~a  b
~a ~b ~c

Notice that the model (~a b) does not assign a truth value to c, and hence represents the two total models (~a b c) and (~a b ~c). This is different from ASP where atoms not in the solution are assumed to be false by default.

Moreover, another notion is that of projected models, i.e., models of a subset of the atoms.
For instance, the models projected on {a, b} are just

a ~b
~a b
~a ~b

I wanted to ask:

1. Are there similar concepts in ASP, and, if so, how can I use clingo to enumerate:
   • partial models
   • projected on a subset of the atoms
     My understanding is that we can enumerate projected models with the option --project=show, but I am not sure the concept of partial model exists.
2. Is there a way to easily convert a CNF SAT problem (e.g. in DIMACS format) to an equivalent LP problem?

[rkaminsk]

1. Enumeration together with projection is available in clingo. You can either use --project=show or add an explicit #project directive to the program. (It is not that partial model are enumerated; you get one model that has projected atoms in it (which is visible in the output if you use the #project directive).
2. Yes, you add a choice rule for every variable in the dimacs formula and then add integrity constraints capturing the clauses. This should be implemented as a dimacs to aspif converter. There might already be tools available for this.

[BenKaufmann]

As an example. Given:

$ cat /tmp/ex-pro.lp 
{a;b;c}.
:- not a, not b, c.
:- a, not b, not c.
:- a, b.

#project a.
#project b.

Running $ clingo /tmp/ex-pro.lp --project -n0 produces all models projected on {a,b}:

clingo version 5.7.1
Reading from /tmp/ex-pro.lp
Solving...
Answer: 1

Answer: 2
b
Answer: 3
a c
SATISFIABLE

Details: https://www.cs.uni-potsdam.de/wv/publications/DBLP_conf/cpaior/GebserKS09.pdf

[BenKaufmann]

Regarding partial models: if SAT-preprocessing is enabled, internally clingo might actually compute partial models. E.g. when running the above example with option --sat-pre, clingo eliminates c during preprocessing and then computes partial models over {a,b}. However, these partial models are first extended to full models in a "post-processing" step before they are printed/reported.

[masinag]

(It is not that partial model are enumerated; you get one model that has projected atoms in it (which is visible in the output if you use the #project directive).

In principle, models can be both projected and partial. For instance, given the problem (~a | b | d) & (a | c), projected onto {a, b, c}, then a set of partial, projected models is

a
~a c

where:

• a is a model since it can be extended to a d, and represents 4 total models on {a, b, c}
• ~a c is a model (e.g., it can be extended to ~a c d), and represents 2 total models on {a, b, c}

So, I understand that in clingo (and in general in ASP?) there is no notion of partial models, or at least they cannot be returned by the solver. Am I correct?

Thank you anyway for the tips, also on the conversion from DIMACS.

[rkaminsk]

There is no notion of partial models in clingo.