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 <#113 (comment)>, 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