Erroneous output with empty solution value

[Armael]

Hi! I'm trying to investigate using open-wbo-inc for a project, and while it has performed very well, it seems I just hit a problematic instance on which open-wbo-inc misbehaves.

On the following instance, I get the following output (note the empty solution line):

c
c Open-WBO:  a Modular MaxSAT Solver -- based on Glucose4.1 (core version)
c Version:   Inc -- MaxSAT Evaluation 2018
c Authors:   Saurabh Joshi, Prateek Kumar, Ruben Martins, Sukrut Rao
c Contributors:  Alexander Nadel, Vasco Manquinho
c Contact:   open-wbo@sat.inesc-id.pt -- http://sat.inesc-id.pt/open-wbo/
c
c WARNING: for repeatability, setting FPU to use double precision
c |                                                                                                       |
c ========================================[ Problem Statistics ]===========================================
c |                                                                                                       |
c |  Problem Format:             MaxSAT                                                                   |
c |  Problem Type:             Weighted                                                                   |
c |  Number of variables:         16933                                                                   |
c |  Number of hard clauses:         51                                                                   |
c |  Number of soft clauses:         62                                                                   |
c |  Number of cardinality:           0                                                                   |
c |  Number of PB :                   0                                                                   |
c |  Parse time:                   0.00 s                                                                 |
c |                                                                                                       |
c Limiting number of clusters to number of weights
c #Diff Weights= 17 | #Modified Weights= 17
c Warn: changing to LSU algorithm.
c GTE auxiliary #clauses = 3000000
c Warn: changing to Adder encoding.
s OPTIMUM FOUND
v 

Perhaps interestingly, removing the last clause of the input yields a different result:

c
c Open-WBO:  a Modular MaxSAT Solver -- based on Glucose4.1 (core version)
c Version:   Inc -- MaxSAT Evaluation 2018
c Authors:   Saurabh Joshi, Prateek Kumar, Ruben Martins, Sukrut Rao
c Contributors:  Alexander Nadel, Vasco Manquinho
c Contact:   open-wbo@sat.inesc-id.pt -- http://sat.inesc-id.pt/open-wbo/
c
c WARNING: for repeatability, setting FPU to use double precision
c |                                                                                                       |
c ========================================[ Problem Statistics ]===========================================
c |                                                                                                       |
c |  Problem Format:             MaxSAT                                                                   |
c |  Problem Type:             Weighted                                                                   |
c |  Number of variables:         16932                                                                   |
c |  Number of hard clauses:         51                                                                   |
c |  Number of soft clauses:         61                                                                   |
c |  Number of cardinality:           0                                                                   |
c |  Number of PB :                   0                                                                   |
c |  Parse time:                   0.00 s                                                                 |
c |                                                                                                       |
c Limiting number of clusters to number of weights
c #Diff Weights= 17 | #Modified Weights= 17
c Warn: changing to LSU algorithm.
c GTE auxiliary #clauses = 2615732
c Overflow in the Encoding
s UNKNOWN

[sbjoshi]

@Armael Could you please let us know the following details?

1) Which branch did you use to build Open-WBO-Inc? 2) How did you run the tool? Please specify exact command line (including runsolver or other timeout utility you might have used).

[Armael]

Ah, I should have included that indeed.

1. I'm using the master branch (commit 40a68e90f7c3)
2. I compiled the tool in release mode using make r, then ran it on the instance with ./open-wbo-inc_release ./input.wcnf
3. I'm using Archlinux with gcc 10.1.0 and gmp 6.2.0
4. Interestingly, if I build the tool in debug mode (with make) rather than release mode, I get an assertion failure instead:

c
c Open-WBO:  a Modular MaxSAT Solver -- based on Glucose4.1 (core version)
c Version:   Inc -- MaxSAT Evaluation 2018
c Authors:   Saurabh Joshi, Prateek Kumar, Ruben Martins, Sukrut Rao
c Contributors:  Alexander Nadel, Vasco Manquinho
c Contact:   open-wbo@sat.inesc-id.pt -- http://sat.inesc-id.pt/open-wbo/
c
c WARNING: for repeatability, setting FPU to use double precision
c |                                                                                                       |
c ========================================[ Problem Statistics ]===========================================
c |                                                                                                       |
c |  Problem Format:             MaxSAT                                                                   |
c |  Problem Type:             Weighted                                                                   |
c |  Number of variables:         16933                                                                   |
c |  Number of hard clauses:         51                                                                   |
c |  Number of soft clauses:         62                                                                   |
c |  Number of cardinality:           0                                                                   |
c |  Number of PB :                   0                                                                   |
c |  Parse time:                   0.00 s                                                                 |
c |                                                                                                       |
c Limiting number of clusters to number of weights
c #Diff Weights= 17 | #Modified Weights= 17
open-wbo-inc: /home/armael/Src/Open-WBO-Inc/solvers/glucose4.1/../../encodings/Enc_Totalizer.cc:310: void openwbo::Totalizer::build(Glucose::Solver*, Glucose::vec<Glucose::Lit>&, int64_t): Assertion `rhs >= 1 && rhs <= lits.size()' failed.
zsh: abort (core dumped)  ./open-wbo-inc /tmp/input2.wcnf

[sbjoshi]

@Armael Upon a cursory look at your input file, it seems that it is not as per the required form. Open-WBO-Inc internally uses off-the-shelf SAT solvers, almost all of which requires that the number of variables that you provide in the "p" line has to exactly match with the distinct numbers you are using as variables. That does not seem to be the case here.

Your input instance has the following p-line p wcnf 46166 113 902047172869

But I don't think that you have 46166 many variables in the formula that you have specified. The largest variable index Open-WBO-Inc read was 16933 but I believe that you do not even have 16933 different variables in the formula that you have specified.

I suggest that you preprocess your formula so that the number of distinct variables you are using in the formula matches exactly with what you specify in the p-line.

Let us know if there's still a problem.

[Armael]

The number 46166 comes from a larger instance which had the same issue and that I tried to minimize by hand by removing clauses. However, post-processing the (minimized) instance to renumber the variables doesn't seem to fix the issue.

This is the resulting instance. If I'm not mistaking, this one uses the same number of variables that it advertises in the p-line, and it makes the solver crash with the same error.

[Armael]

FWIW, here's a very small instance (also derived from the previous one here) that triggers the Overflow in the encoding error:

p wcnf 3 5 8
8 1 0
8 -1 2 0
8 3 0
8 -3 -2 0
1 1 0

This produces the following output:

c Limiting number of clusters to number of weights
c #Diff Weights= 1 | #Modified Weights= 1
c Warn: changing to LSU algorithm.
c GTE auxiliary #clauses = 0
c Overflow in the Encoding
s UNKNOWN

Notice how the instance is trivially UNSAT (the soft clause is useless here, but the solver seems to crash with an assertion failure if there are no soft clauses in the input).

[sbjoshi]

@Armael

• In this example the first and last clauses are exactly the same (except the weight difference), this is not expected.
• If all the clauses are hard clauses, one is requested to run a SAT solver rather than a MaxSAT solver. It does not make a sense to run a MaxSAT solver on a formula where every clause is hard.
• I notice that the weight of the hard clauses is 8 but the weight of the single soft clause is 1. The expected form of input is as follows : if soft clauses have weights (2,3,5) then the weight of the hard clauses should be exactly 1 more than the sum of weights of all the soft clauses (2+3+5+1=11). I request that you try with hard clause weight as per this formula and let us know if the error still persists.
• I agree that some of the issues can be handled via preprocessing and better documentation, but for now I suggest that you try changing the weights as I mentioned above.