negate

[algebravic]

The following has been puzzling me for days, until I saw a subtlety. I wanted to generate a not equals constraint. So I took the clauses generated by CardEnc.equals, and fed them through negate. Much to my surprise I found out that those clauses were satisfied by something which also satsified the equals clauses. Eventually I realized that the following occurred: Suppose that F(X,Y) is a formula, where Y are auxilliary variables. It can happen that, for a given assignment x to X that there are assignments y_1 and y_2 for Y so that F(x,y_1) is true, and F(x,y_2) is false, so that using negate doesn't really effect the complement. So do you know of a not-equals constraint?

After I posted this I thought that I could do this by using the OR of an atmost and an atleast. Alas that suffers from the same problem that I described above. The most immediate way to make a not equals constraint that I can think of would use a BDD and the Tseitin encoding. I'm sure that there are others.

So I cobbled together a BDD generation of the not equals constraint. Actually, in my problem, I wanted an OR of a bunch of these. Fortunately, in the Tseitin encoding of a BDD, the values of the auxilliary variables are all functions of the input variables, so that the anomaly that I noted above doesn't happen. So far it seems to be working.

[alexeyignatiev]

Victor, yes, negating a formula with auxiliary variables is non-trivial as you need to account for them when applying the negation. In the best-case scenario, you have a single Boolean variable y enforcing your original non-clausal formula to be satisfied. To negate it, you would need to replace the corresponding unit clause (y) with the "opposite" unit clause (-y). But in general, if no such final auxiliary variable exists, you should indeed be careful.

To encode a not-equals constraint, you can use one at-most constraint and one at-least constraint. Say you want to encode not-equals-k. Then you can represent it as a disjunction [ at-most-(k-1) \/ at-least-(k+1) ].

The simplest way (but not the best) to do this via the facilities provided by PySAT is to have these two constraints separately encoded into CNFs M (for at-most-k-1) and L (for at-least-k+1) as normal and then introduce two additional variables m and l such that -m should be added in every clause of M while -l is added in every clause of L. Then you add the clauses of both augmented M and L into your result CNF and add one final clause (m \/ l) in there. This should do the trick. You need to be careful with auxiliary variables though: the sets of auxiliary variables used in M, L, and in (m \/ l) must not intersect.

[algebravic]

Alexey, Thank you. That was a help. I wonder if a function for disjunctions of formulas would be useful to have standard instead of making the user figure it out on their own.

[alexeyignatiev]

Good point. This should be more-or-less easy to implement as a method of class CNF. I will look into it once I have time.