protected boolean minimizeLit ( final int root ) { assert marked ( root ) != 0 ; CLClause reason = var ( root ) . reason ( ) ; if ( reason == null ) { return false ; } final int oldSeenSize = this . seen . size ( ) ; int nextSeen = oldSeenSize ; boolean res = true ; int lit = root ; while ( true ) { int other ; for ( int p = 0 ; res && p < reason . lits ( ) . size ( ) ; p ++ ) { other = reason . lits ( ) . get ( p ) ; if ( other == lit ) { continue ; } assert val ( other ) == VALUE_FALSE ; if ( marked ( other ) != 0 ) { continue ; } final CLVar v = var ( other ) ; if ( v . reason ( ) == null ) { res = false ; } else if ( ! this . control . get ( v . level ( ) ) . mark ( ) ) { res = false ; } else { mark ( other ) ; } } if ( ! res || nextSeen == this . seen . size ( ) ) { break ; } lit = - this . seen . get ( nextSeen ++ ) ; reason = var ( lit ) . reason ( ) ; assert reason != null ; } if ( ! res ) { unmark ( oldSeenSize ) ; } return res ; }
Minimize the first UIP clause by trying to remove a given literal .