to_string

[yoni206]

It would be great to have a way of pretty-printing formulas, by providing a dictionary between the variables (numerals) and application-specific name. This is easy to do for ordinary CNF using dictionaries, but I am not sure how to do this for pseudo-Boolean constraints. This would be nice to have for debugging applications that use pysat.

[alexeyignatiev]

Good point, @yoni206. But what do you mean by "application-specific name"? The standard (and most straightforward) way to implement formula's __str__() is to make it return its DIMACS representation.

[yoni206]

I mean that typically in the application you would have a dictionary between the variable number (which would appear in the CNF) and some representation of what this variable represents (maybe an object, with an str method). So passing that dictionary between numbers and strings would be a bonus.

This can be done in the application level for CNF, but I don't see how to do this for cardinality / PB constraints. The simplest and great thing to have would be the ability to query what kind of constraint it is, what are the weights and what are the variables. If I have that, then I can pretty print this in my application.

On Mon, Sep 12, 2022 at 2:21 AM Alexey Ignatiev @.***> wrote:

Good point, @yoni206 https://github.com/yoni206. But what do you mean by "application-specific name"? The standard (and most straightforward) way to implement formula's str() is to make it return its DIMACS representation.

— Reply to this email directly, view it on GitHub https://github.com/pysathq/pysat/issues/113#issuecomment-1243065316, or unsubscribe https://github.com/notifications/unsubscribe-auth/ADAKGRHL3WNOI7RROYTXS33V5ZSO5ANCNFSM6AAAAAAQJYHKSM . You are receiving this because you were mentioned.Message ID: @.***>

[alexeyignatiev]

Have a look at the functionality of IDPool. It is meant to represent this kind of dictionary.

[RexYuan]

@yoni206 do you mean that, for ordinary CNF, given clauses

[
  [1, -2, 3],
  [2, -3]
]

and dictionary

{
  1: "a",
  2: "b",
  3: "c"
}

you want to print out something like this?

(a | ~b | c) & (b | ~c)

[alexeyignatiev]

I guess this string may help a non-SAT researcher understand the meaning of the formula but a SAT practitioner would perhaps prefer a formula in DIMACS. It has been a standard for many years and everybody speaks this "language". What I meant above was that the mapping from integer variable identifiers to the corresponding objects can be provided by means of the already existing IDPool. I presume it can be added into comments line sitting in a CNF object.

[yoni206]

@RexYuan yes, but also for cardinality constraints.

[RexYuan]

@yoni206 How about using two dictionaries like this?

card_clauses = [
  [[1, -2, 3], 2],
  [[2, -3], 1]
]
card_names = {
  2: "n",
  1: "m"
}
var_names = {
  1: "a",
  2: "b",
  3: "c"
}

then you have

a + ~b + c <= n
b + ~c <= m

Of course, this would run into a problem if there are different names for a cardinality, but I think then they are already indistinguishable on the constraint level.

[yoni206]

yeah that could work