pwn1
commented
5 years ago Closed pwn1 closed 5 years ago
pwn1
commented
5 years ago 
rubengmartins
commented
5 years ago I tried to duplicate the issue but it does not trigger the assertion for me.
For the instance you provided I get:
c | Problem Format: MaxSAT |
c | Problem Type: Weighted |
c | Number of variables: 262 |
c | Number of hard clauses: 941 |
c | Number of soft clauses: 161 |
c | Number of cardinality: 0 |
c | Number of PB : 0 |
c | Parse time: 0.00 s |Is this the same instance you got that error? The number of variables and clauses seem to differ.
The 'o' line returned by Open-WBO (and other MaxSAT solvers) corresponds to an upper bound on the solution (with respect to the sum of unsatisfied soft clauses). The optimal solution is smaller or equal to that value.
pwn1
commented
5 years ago You are right, I must have run it on one instance and uploaded another (and also misunderstood the 'o' line). However, the instance that I uploaded does trigger the assertion on my machine. Here is the output:
c
c Open-WBO: a Modular MaxSAT Solver -- based on Glucose4.1 (core version)
c Version: September 2018 -- Release: 2.1
c Authors: Ruben Martins, Vasco Manquinho, Ines Lynce
c Contributors: Miguel Neves, Saurabh Joshi, Norbert Manthey, Mikolas Janota
c Contact: open-wbo@sat.inesc-id.pt -- http://sat.inesc-id.pt/open-wbo/
c
c | |
c ========================================[ Problem Statistics ]===========================================
c | |
c | Problem Format: MaxSAT |
c | Problem Type: Weighted |
c | Number of variables: 262 |
c | Number of hard clauses: 941 |
c | Number of soft clauses: 161 |
c | Number of cardinality: 0 |
c | Number of PB : 0 |
c | Parse time: 0.00 s |
c | |
c ==========================================[ Solver Settings ]============================================
c | |
c | Algorithm: OLL |
c | Cardinality Encoding: Totalizer |
c | |
o 2548838
Assertion failed: (var(a) < S->nVars() && var(b) < S->nVars()), function addBinaryClause, file /Users/pn/openwbo/open-wbo/solvers/glucose4.1/../../encodings/Encodings.cc, line 48.
Abort trap: 6I wonder if this could be a compiler issue. I have the current github repo version, compiled on a mac with clang. Are you using gcc?
The above output was from the open-wbo binary. If I use open-wbo_release, it produces the 'o' line then appears to get stuck (produces no more output).
pwn1
commented
5 years ago It seems to be OK on Linux compiled with GCC 7.4.0.
rubengmartins
commented
5 years ago I am using clang version: Apple LLVM version 10.0.1 (clang-1001.0.46.4) and I don't have that issue.
I will try to reproduce it with other versions of clang. What version are you currently using?
pwn1
commented
5 years ago I have exactly the same version of clang. I have recompiled it just now and it does not throw an exception. This time I did 'make clean' before compiling, I think I didn't do that last time. The only cause I can think of is that it linked old .o files, which would suggest something wrong with the dependencies. Sorry about this, I should have realised I was not doing a clean compile.
Hi,
Open-WBO seems to overshoot the optimal value then fail an assertion. I have an independent source for the optimal value being 2246639 for this instance (found by both maxhs and SCIP).
I'll attach the instance.
Thanks, Peter