protected boolean decide ( ) { assert propagated ( ) ; int decision = 0 ; while ( decision == 0 && ! this . decisions . empty ( ) ) { final int lit = this . decisions . top ( ) ; this . decisions . pop ( lit ) ; if ( val ( lit ) == 0 ) { decision = lit ; } } if ( decision == 0 ) { return false ; } assert decision > 0 ; if ( this . phases . get ( decision ) < 0 ) { decision = - decision ; } this . stats . decisions ++ ; this . stats . levels += this . level ; assume ( decision ) ; return true ; }
Checks if there are unassigned literals left .