public boolean isBMO ( boolean cache ) { assert orderWeights . size ( ) == 0 ; boolean bmo = true ; final SortedSet < Integer > partitionWeights = new TreeSet <> ( ) ; final SortedMap < Integer , Integer > nbPartitionWeights = new TreeMap <> ( ) ; for ( int i = 0 ; i < nSoft ( ) ; i ++ ) { final int weight = softClauses . get ( i ) . weight ( ) ; partitionWeights . add ( weight ) ; final Integer foundNB = nbPartitionWeights . get ( weight ) ; if ( foundNB == null ) nbPartitionWeights . put ( weight , 1 ) ; else nbPartitionWeights . put ( weight , foundNB + 1 ) ; } for ( final int i : partitionWeights ) orderWeights . push ( i ) ; orderWeights . sortReverse ( ) ; long totalWeights = 0 ; for ( int i = 0 ; i < orderWeights . size ( ) ; i ++ ) totalWeights += orderWeights . get ( i ) * nbPartitionWeights . get ( orderWeights . get ( i ) ) ; for ( int i = 0 ; i < orderWeights . size ( ) ; i ++ ) { totalWeights -= orderWeights . get ( i ) * nbPartitionWeights . get ( orderWeights . get ( i ) ) ; if ( orderWeights . get ( i ) < totalWeights ) { bmo = false ; break ; } } if ( ! cache ) orderWeights . clear ( ) ; return bmo ; }
Tests if the MaxSAT formula has lexicographical optimization criterion .