public void encode ( final MiniSatStyleSolver s , final LNGIntVector lits , int rhs ) { assert lits . size ( ) > 0 ; hasEncoding = false ; this . cardinalityUpoutlits . clear ( ) ; this . cardinalityLwoutlits . clear ( ) ; if ( rhs == 0 ) { for ( int i = 0 ; i < lits . size ( ) ; i ++ ) addUnitClause ( s , not ( lits . get ( i ) ) ) ; return ; } assert rhs >= 1 && rhs <= lits . size ( ) ; if ( rhs == lits . size ( ) ) return ; hasEncoding = true ; int mod = ( int ) Math . ceil ( Math . sqrt ( rhs + 1.0 ) ) ; if ( this . modulo == - 1 ) this . modulo = mod ; else mod = this . modulo ; for ( int i = 0 ; i < lits . size ( ) / mod ; i ++ ) { final int p = mkLit ( s . nVars ( ) , false ) ; MaxSAT . newSATVariable ( s ) ; this . cardinalityUpoutlits . push ( p ) ; } for ( int i = 0 ; i < mod - 1 ; i ++ ) { int p = mkLit ( s . nVars ( ) , false ) ; MaxSAT . newSATVariable ( s ) ; this . cardinalityLwoutlits . push ( p ) ; } this . cardinalityInlits = new LNGIntVector ( lits ) ; this . currentCardinalityRhs = rhs + 1 ; if ( this . cardinalityUpoutlits . size ( ) == 0 ) this . cardinalityUpoutlits . push ( this . h0 ) ; this . toCNF ( s , mod , this . cardinalityUpoutlits , this . cardinalityLwoutlits , lits . size ( ) ) ; assert this . cardinalityInlits . size ( ) == 0 ; this . update ( s , rhs ) ; }
Encodes a cardinality constraint .