sat4j issueshttps://gitlab.ow2.org/sat4j/sat4j/-/issues2018-11-12T16:07:10Zhttps://gitlab.ow2.org/sat4j/sat4j/-/issues/127OPBSolver exports files with empty objectives2018-11-12T16:07:10ZGhost UserOPBSolver exports files with empty objectivesI tried the OPBSolverDecorator for exporting .opb files. In some cases, my objective function is empty because I am solving a pure SAT instance (using the PB solver because of "at most 1"-constraints).
In these cases, the OPBSolverDecor...I tried the OPBSolverDecorator for exporting .opb files. In some cases, my objective function is empty because I am solving a pure SAT instance (using the PB solver because of "at most 1"-constraints).
In these cases, the OPBSolverDecorator outputs a .opb format that the command line sat4j-pb.jar does not understand. The text opb file then contains the following line:
min: ;
This is because the "toString()" method does a null-check on the objective function, but it does no empty-check on it. I think my fix for it is suboptimal:
```
if (this.obj != null) {
String objStr = obj.toString();
if (objStr.trim().length() > 0) {
tmp.append("\n");
tmp.append("min: ");
tmp.append(this.obj);
tmp.append(";");
}
}
```https://gitlab.ow2.org/sat4j/sat4j/-/issues/126How do I do an industry standard export for Partial Weighted MaxSat problems?2018-07-07T05:11:53ZGhost UserHow do I do an industry standard export for Partial Weighted MaxSat problems?I have filed this as question, but it might result in a change request:
I am using the WeightedMaxSatDecorator for solving Partial Weighted MaxSat problems. Most constraints are in (weighted) cnf, but there are some cardinality constrai...I have filed this as question, but it might result in a change request:
I am using the WeightedMaxSatDecorator for solving Partial Weighted MaxSat problems. Most constraints are in (weighted) cnf, but there are some cardinality constraints. If I do not want to convert them to CNF constraints, I cannot export a wcnf file but must export something other.
I think the .opb format is suitable for that case. Am I right?
I tried to create .opb output using the OPBStringSolver or the LPStringSolver. Both have the same problem:
The WeightedMaxSatDecorator calls the method "registerLiteral(int p)" on the decorated solver. Since both the OPBStringSolver and the LPStringSolver extend the DimacsStringSolver, the method DimacsStringSolver.registerLiteral(int p) is called, which throws an UnsupportedOperationException.
So, if one of these StringSolvers is suitable for my problem: Would it be a solution to override the method in that suitable solver so that it does not do anything?
An, if none of these StringSolvers is suitable: Is there another way of exporting all input that the WeightedMaxSatDecorator got into a standard file format?https://gitlab.ow2.org/sat4j/sat4j/-/issues/123Does Sat4j provide model counting capability?2018-07-07T05:11:53ZMouhammad SakrDoes Sat4j provide model counting capability?