CNF for soft clauses

[AlbertoSinigaglia]

Quick question... why are you accepting only conjunction as soft clauses and not CNF formulas?
First of all, this reduces the expressivity of the model, and second of all, does not seem that difficult to generalize to CNF, at the end of the day, you already have all the code to check if a CNF formula si satisfied, and so there should be no much code to change for that

What I mean is something like (given 2 literals):

using something like this:

model = WCNF()
model.append([[1, -2], [-1, 2]], weight=1)

[alexeyignatiev]

You are right that it is technically simple to do. However, this is not supported by the WCNF format. And PySAT currently sticks to this well-known format.

Something along the lines you are suggesting seems to be provided by a weighted extension of "group CNF". I need to think about it. If my understanding is correct, this could be done.

[AlbertoSinigaglia]

I've taken a look at the implementation, and creating a variant of WCNF it's not hard once we enforce the fact that the weight must be positive (just moving the burder of the negation to the user)

on the other hand, the implementation of the MaxSat solvers are very tied to the representation of the clauses, I've taken a look at the FM algorithm and I can fix everything, except the fact that you have the sels variable that it's not easy to change in order to consider the full CNF soft clause, instead of a single combination of literal... I'll take a look at other solver that you have in the library, hopefully finding something more "OOP", and therefore easier to change...

[alexeyignatiev]

There is no need to modify the solvers. What needs to be done is a nicely implemented GCNF format with a method to_wcnf(), which would make a trivial transformation of the formula to WCNF. Solvers could then just apply the method if encountered a GCNF formula.

[AlbertoSinigaglia]

sorry, with solver you mean RC2/FM or what?
Because I don't see how you can encode a CNF formula (soft clauses of GCNF) as just conjunction of literal (soft clauses of WCNF)

[alexeyignatiev]

Yes, I mean exactly example MaxSAT solvers and MUS/MCS enumerators. They don't need any major changes as it will be enough to read a GCNF and transform it to WCNF.

The translation is to simply introduce selectors for each soft group of clauses and make the result extended clauses hard.

Assume that '+' represents disjunction, '-' denotes negation while '' represents conjunction. And let's say you have a set H of hard clauses h1, h2, ..., and two groups of soft clauses S1 = (-x1 + x2) (x3) and S2 = (x2 + -x3) * (-x1 + -x3). The weight of S1 is 10 while the weight of S2 is 15. Then you can introduce two selector variables x4 and x5 and write down a new (WCNF) formula:

p wcnf N M TOP
10 4 0
15 5 0
TOP h1 0
TOP h2 0
...
TOP -4 -1 2 0
TOP -4 3 0
TOP -5 2 -3 0
TOP -5 -1 -3 0

[AlbertoSinigaglia]

Ok so, I tried to find something on google that refers to this "GCNF" but I found anything... however, I tried to understand what to do from your example how it should work, and the following code should do it.

Assuming the soft clauses that you showed in the example (and an arbitrary hard clause just to test):

weights = [15, 10]
hard_clauses = [
    [31],
    [56, 66],
]
soft_clauses = [
    [[-1, 2], [3]],
    [[2, -3], [-1, -3]]
]

flat = lambda arr: [item for sublist in arr for item in sublist]
max_var = max([abs(l) for l in flat(flat(soft_clauses)) + flat(hard_clauses)])

new_soft_clauses = []
new_hard_clauses = hard_clauses[:]
new_weight = weights[:]
for clause in soft_clauses:
    max_var+=1
    current_new_variable = max_var
    new_soft_clauses.append(current_new_variable)
    for subclause in clause:
        new_hard_clauses.append(subclause[:] + [-current_new_variable])
print(new_hard_clauses, "\n", new_soft_clauses,"\n", new_weight)

the following is the result:

# hard clauses, consider that 4 and 5 in your example here are 67 and 68
[
   [31], 
   [56, 66], 
   [-1, 2, -67], 
   [3, -67], 
   [2, -3, -68], 
   [-1, -3, -68]] 
# soft clauses
[67, 68] 
# weights
[15, 10]

Please let me know if this make sense...

[AlbertoSinigaglia]

Hi there, back again.

"""This is not being extensively tested""", but I tried on my project (binarized neural networks), and it's giving the correct result (aka the assignments that I'm getting are the same of those that I'm getting brute forcing all the possible combinations)

The code I've used is the following:

class GroupWCNF(object):
    def __init__(self):
        self.nv = 0
        self.hard = []
        self.soft = []
        self.wght = []

    def append(self, clause, weight=None):
        # just for safety...
        if not isinstance(clause, list):
            clause = [clause]
        # loop over the new clauses to find the highest variable
        for subclause in clause:
            if isinstance(subclause, list):
                self.nv = max([abs(l) for l in subclause] + [self.nv])
            else:
                self.nv = max(abs(subclause), self.nv)
        if weight:
            self.soft.append(list(clause))
            self.wght.append(weight)
        else:
            self.hard.append(list(clause))

    def toWCNF(self):
        new_soft_clauses = []
        new_hard_clauses = self.hard[:]
        max_var = self.nv # max_var will be the new variable introduced
        for clause in self.soft:
            max_var+=1
            new_soft_clauses.append([max_var])
            for subclause in clause:
                new_hard_clauses.append(subclause + [-max_var])
        wcnf = WCNF()

        wcnf.extend(new_hard_clauses)
        wcnf.extend(new_soft_clauses, weights=self.wght)

        return wcnf

[alexeyignatiev]

I am absolutely sure GCNF has been described before. For instance, it appeared in the MUS track of the SAT Competition 2011. I will look into this when I get time.

[alexeyignatiev]

Closing this now.