Pdf documentation

[BoltMaud]

Dear,

Page 50 of the pdf documentation (https://pysathq.github.io/docs/pysat.pdf) there is a warning that says "LSU supports only unweighted problems." but just below inputs are WCNF type. Do you confirm the warning ?

Thanks,

BoltMaud

[alexeyignatiev]

Hi @BoltMaud,

Yes, I confirm that LSU supports only unweighted formulas.

Originally, WCNF is a standard MaxSAT file format, which can be used to represent both unweighted and weighted partial CNF formulas. The description of the format can be found e.g. here.

Similarly, PySAT has two builtin formula types: CNF and WCNF. While the former type is a simple "list" of clauses, the latter one is a weighted partial CNF. Thus, a WCNF formula can be seen as a conjunction of two "lists" of clauses: (1) hard clauses (that must be satisfied) and (2) soft clauses (that we would prefer to satisfy). If all soft clauses have weight 1, the formula is deemed unweighted partial. Otherwise, it is weighted.

As a result, LSU supports unweighted WCNF formulas, i.e. whose soft clauses have weight 1. Hope this helps.

Do not hesitate to ask other questions if you have any.

Best, Alexey

[BoltMaud]

Hi @alexeyignatiev ,

Thank you very much for your rapid and complete message. I had misunderstood unweighted WCNF formulas which may good enough for my work!

All the best,

BotlMaud

[alexeyignatiev]

No problem! Feel free to contact me again if needed.

[BoltMaud]

Hi again, Just a very quick question : Is there a MaxSAT implemented algorithm that solves weighted WCNF formulas with atMostk constraints ? Thanks again, Mathilde

[alexeyignatiev]

I am not sure what you mean by "solving WCNF formulas with AtMostK constraints". Every MaxSAT algorithm either uses cardinality constraints (AtMost1 or AtMostK) or pseudo-Boolean constraints. Can you explain to me what exactly you want to achieve?

[alexeyignatiev]

For example, our MaxSAT solver RC2, which by the way is a part of PySAT, implements the OLL/RC2 algorithm for MaxSAT and is currently the best performing MaxSAT solver, according to the MaxSAT Evaluations 2018 and 2019.

[BoltMaud]

Yes, I am using RC2 but with WCNF objects. I would like to use this kind of constraints :

cnf.append([[1, 2, 3], 1], is_atmost=True)

where cnf is then a WCNFPlus. Does RC2 work with this ?

[alexeyignatiev]

Well, do you mean you have a formula containing this kind of native cardinality constraints? Or do you mean you want to instruct RC2 to replace cardinality constraints that it creates during the solving process with this kind of native cardinality constraints?

[alexeyignatiev]

At this point, RC2 can handle WCNFPlus formulas but only if this kind of native cardinality clauses are hard (i.e. they cannot be soft). Also, if you set the underlying solver to 'mc', the solver should use native cardinality constraints when running the RC2 algorithm.

UPDATE: sorry, you have to set the solver to 'mc' in both cases. Otherwise, RC2 will of course be unable to deal with native cardinality constraints.

[BoltMaud]

I have a formula that contains this kind of contraints.

Ok, thank you for your answers. I will check if my constraints are hard or soft. Thank you for this library too :) !

[alexeyignatiev]

Thank you for using it. :) By the way, as far as I recall, LSU should also be able to deal with WCNFPlus formulas under the same conditions.

[BoltMaud]

This seems to work with LSU but not with RC2. It seems that RC2 prefers to get a good cost than respecting the cardinality constraint. To convince myself, I have created the small MaxSAT problem below :

Let's define the following formula : a and (b equivalent to c)

• b and c respectively cost 1 if they are True
• but we can only have 1 variable to True in [b,c]
• even if b and c are weighted we should have [1, -2, -3] for [a, not b, not c] as the native cardinality constraint is hard

# construction of the formula
from pysat.formula import WCNFPlus
wcnfplus = WCNFPlus()
# a
wcnfplus.append([1])
# b equivalent to c
wcnfplus.append([-2,3])
wcnfplus.append([2,-3])
# costs
wcnfplus.append([2], 1)
wcnfplus.append([3], 1)
# atmost
wcnfplus.append([[2,3], 1], is_atmost=True)
wcnfplus2=wcnfplus.copy()
wcnfplus3=wcnfplus.copy()

• Result with LSU

  from pysat.examples.lsu import LSUPlus
  solve= LSUPlus(wcnfplus)
  solve.solve()
  model=solve.get_model()
  print("LSU",[s for s in model])

  # output
  LSU [1, -2, -3]

• Result with RC2

  from pysat.examples.rc2 import RC2
  solve= RC2(wcnfplus2,solver='mc')
  solve.compute()
  model=solve.model
  print("RC2",[s for s in model])

  # output
  RC2 [1, 2, 3]

• Result with RC2 when removing weighted variables

  wcnfplus3.soft=[]
  solve= RC2(wcnfplus3,solver='mc')
  solve.compute()
  model=solve.model
  print("RC2 when removing soft clauses",[s for s in model])

  # output
  RC2 when removing soft clauses [1, -2, -3]

[alexeyignatiev]

Hi Mathilde,

I have checked your example with the most recent version of PySAT and it works both with LSU and RC2. Can you check the version of the toolkit you are using and update it if it is not up-to-date (it should be 0.1.5.dev4)? Support of native WCNFPlus has been added to RC2 just recently.

Best, Alexey

[BoltMaud]

Hi Alexey,

Thanks for this direction. It is now working on my computer too!

Best, Mathilde