Cardinality constraints do not work with minicard

[rjungbeck]

import pysat.solvers
import pysat.formula

cnfp=pysat.formula.CNFPlus()
cnfp.append(list(range(1, 10)))
cnfp.append([list(range(-9, -3)), 3], is_atmost=True)

with pysat.solvers.Solver("minicard") as solver:
    solver.append_formula(cnfp)
    solver.solve()
    model=solver.get_model()
    print(model)

Prints:

    [1, -2, -3, -4, -5, -6 ,-7, -8, -9]

[alexeyignatiev]

Something is wrong with your example. Can you recheck?

[rjungbeck]

I corrected the sample

[alexeyignatiev]

Thanks. This is indeed a bug. Method append_formula() should handle both clauses and AtMost constraints for Minicard. Currently, only clauses are added to the solver (as for any other SAT solver), i.e. AtMost constraints are ignored by this method. I am going to fix this shortly.

[alexeyignatiev]

This should be fixed in version 0.1.4.dev25. Please, check.

[rjungbeck]

The simple case from the original problem works now. But using minicard through RC2 does not work:

import pysat.solvers
import pysat.formula
import pysat.examples.rc2

def main():
    wcnfp=pysat.formula.WCNFPlus()
    wcnfp.append([[1, -2, 3], 1], is_atmost=True)

    wcnfp.append([1,2])
    wcnfp.append([-2], weight=1)
    wcnfp.append([-2, -3])

    with pysat.examples.rc2.RC2(solver="minicard", formula=wcnfp) as solver:
        model=solver.compute()
        print(model)
        print(solver.cost)

if __name__=="__main__":
    main()

It returns

[1, - 2, ,3] 
0

So it does not see the cardinality constraint

[alexeyignatiev]

Well, RC2 was not designed to work with WCNFPlus. But I can fix this as soon as I have time. It should be easy. Thanks for reporting!

[rjungbeck]

The bootstrap_with parameter of Solver still ignores cardinality constraints :

import pysat.solvers
import pysat.formula

def main():
    cnfp=pysat.formula.CNFPlus()
    cnfp.append([[1, 2], 1], is_atmost=True)
    cnfp.append([[-1, -2], 1], is_atmost=True)
    cnfp.append([[1], 1], is_atmost=True)
    with pysat.solvers.Solver("minicard", bootstrap_with=cnfp) as solver:
        #solver.append_formula(cnfp)
        if solver.solve():
            model=solver.get_model()
            print(model)

if __name__=="__main__":
    main()

Using solver.append_formula works.

[alexeyignatiev]

Hi @rjungbeck,

Thanks for reporting the bugs. These should (hopefully!) be fixed in version 0.1.5.dev1. Please, check.

[rjungbeck]

Now

with pysat.solvers.Solver("minicard") as solver:
    solver.append_formula([[1, 2, 3]])

does not work anymore.

(NB: Itstill works for the other solvers).

[alexeyignatiev]

Oops, I forgot about this one, sorry!

Apparently, this bug was fixed but I forgot to report here. This is what I get if I run the following code with the latest version (0.1.5.dev6):

>>> with Solver(name='minicard') as solver:
...     solver.append_formula([[1, 2, 3]])
...     for model in solver.enum_models():
...         print(model)
...
[1, -2, -3]
[1, 2, -3]
[1, 2, 3]
[-1, 2, 3]
[-1, -2, 3]
[1, -2, 3]
[-1, 2, -3]

I am closing it now. If the issue remains on your machine, please, reopen.