private void biasPhases ( ) { final double [ ] score = new double [ 2 * ( maxvar ( ) + 1 ) ] ; for ( final CLClause c : this . clauses ) { if ( c . redundant ( ) || c . satisfied ( ) ) { continue ; } double inc = 1 ; for ( int size = c . size ( ) ; size > 0 ; size -- ) { inc /= 2.0 ; } for ( int i = 0 ; i < c . lits ( ) . size ( ) ; i ++ ) { final int p = c . lits ( ) . get ( i ) ; if ( p > 0 ) { score [ p * 2 ] += inc ; } else { score [ ( - p * 2 ) - 1 ] += inc ; } } } for ( int idx = 1 ; idx <= maxvar ( ) ; idx ++ ) { this . phases . set ( idx , ( score [ idx * 2 ] > score [ ( idx * 2 ) - 1 ] ) ? ( byte ) 1 : ( byte ) - 1 ) ; } }
Initializes the initial phases of literals .