private void minimisationWithBinaryResolution ( final LNGIntVector outLearnt ) { long lbd = computeLBD ( outLearnt , - 1 ) ; int p = not ( outLearnt . get ( 0 ) ) ; if ( lbd <= lbLBDMinimizingClause ) { myflag ++ ; for ( int i = 1 ; i < outLearnt . size ( ) ; i ++ ) permDiff . set ( var ( outLearnt . get ( i ) ) , myflag ) ; int nb = 0 ; for ( final MSWatcher wbin : watchesBin . get ( p ) ) { int imp = wbin . blocker ( ) ; if ( permDiff . get ( var ( imp ) ) == myflag && value ( imp ) == Tristate . TRUE ) { nb ++ ; permDiff . set ( var ( imp ) , myflag - 1 ) ; } } int l = outLearnt . size ( ) - 1 ; if ( nb > 0 ) { for ( int i = 1 ; i < outLearnt . size ( ) - nb ; i ++ ) { if ( permDiff . get ( var ( outLearnt . get ( i ) ) ) != myflag ) { p = outLearnt . get ( l ) ; outLearnt . set ( l , outLearnt . get ( i ) ) ; outLearnt . set ( i , p ) ; l -- ; i -- ; } } outLearnt . removeElements ( nb ) ; } } }
A special clause minimization by binary resolution for small clauses .