search

fbacchus / MaxHS

MaxHS: a hybrid Maxsat solver developed by Jessica Davies and Fahiem Bacchus
Other
24 stars 7 forks source link

ERROR incorrect model reported #6

Closed vuphan314 closed 2 years ago

vuphan314 commented 2 years ago

@fbacchus Dr. Bacchus, MaxHS sometimes prints ERROR incorrect model reported. I have some questions:

  1. Why does this error occur?
  2. When this error occurs, is the optimal cost (o line) still correct?

Thank you in advance.

An example wcnf file is attached: or-50-5-6.txt.

Output:

$ maxhs or-50-5-6.txt -no-printOptions -verb=0
c MaxHS 4.0.0
c Instance: or-50-5-6.txt
c Instance: or-50-5-6.txt
c Dimacs Vars: 100
c Dimacs Clauses: 450
c Dimacs Top: 1000000
c HARD: #Clauses = 250, Total Lits = 650, Ave Len = 2.6000 #units = 0
c SOFT: #Clauses = 200, Total Lits = 200, Ave Len = 1.0000
c Total Soft Clause Weight (+ basecost): 1934 (+ 0)
c SOFT%: 44.4444%
c #distinct weights: 3, mean = 9.6692, std. dev = 0.5616, min = 9, max = 10
c Total Clauses: 450
c Parse time: 0.000141
c Wcnf Space Required: 0.0000MB
c ================================
c Using IBM CPLEX version 20.1.0.0 under IBM's Academic Initiative licencing program
c Solved by disjoint phase.
o 934.948500
s OPTIMUM FOUND
v 0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
c ERROR incorrect model reported
c SAT: #calls 2
c SAT: Total time 0.0000
c SAT: #muser calls 0 (0.0000 % successful)
c SAT: Minimize time 0.0000 (0.0000%)
c SAT: Avg constraint minimization 0.0000
c SAT: number of variables substituted 0
c GREEDY: #calls 0
c GREEDY: Total time 0.0000
c CPLEX: #calls 0
c CPLEX: Total time 0.0000
c CPLEX: #constraints 0
c CPLEX: #non-core constraints 0
c LP-Bounds: Total time 0.0000
c LP-Bounds: #calls 0
c LP-Bounds: Forced 0 variables
c MEM MB: 35.0000
c CPU: 0.0023
fbacchus commented 2 years ago

Thanks for the bug report---as I had said the use of floating point weights had not been well tested in maxhs (although any bugs should be minor like this one).

This one arose from comparing two floats calculated differently with equality---however the two numbers were not exactly the same due to floating point errors (differed by 10^-10).

I have fixed this by comparing that the two numbers are close (within absGap which is a parameter set to 10^-6). The fix is on top of the 2021 eval version...so just pull the latest and recompile.

vuphan314 commented 2 years ago

Thank you for the explanation and the fix https://github.com/fbacchus/MaxHS/commit/c8df41ac63e27c2cb32905302e6ede3118b7a07b!

I am closing this issue.