MCPcopy Create free account
hub / github.com/NeuralNetworkVerification/Marabou / encodeLeakyReLUConstraint

Method encodeLeakyReLUConstraint

src/engine/MILPEncoder.cpp:193–254  ·  view source on GitHub ↗

Source from the content-addressed store, hash-verified

191}
192
193void MILPEncoder::encodeLeakyReLUConstraint( GurobiWrapper &gurobi,
194 LeakyReluConstraint *lRelu,
195 bool relax )
196{
197 if ( !lRelu->isActive() || lRelu->phaseFixed() )
198 {
199 return;
200 }
201 unsigned sourceVariable = lRelu->getB();
202 unsigned targetVariable = lRelu->getF();
203 double slope = lRelu->getSlope();
204 double sourceLb = _tableau.getLowerBound( sourceVariable );
205 double sourceUb = _tableau.getUpperBound( sourceVariable );
206
207 if ( sourceLb >= 0 )
208 {
209 List<GurobiWrapper::Term> terms;
210 terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", targetVariable ) ) );
211 terms.append( GurobiWrapper::Term( -1, Stringf( "x%u", sourceVariable ) ) );
212 gurobi.addEqConstraint( terms, 0 );
213 }
214 else if ( sourceUb <= 0 )
215 {
216 List<GurobiWrapper::Term> terms;
217 terms.append( GurobiWrapper::Term( 1, Stringf( "x%u", targetVariable ) ) );
218 terms.append( GurobiWrapper::Term( -slope, Stringf( "x%u", sourceVariable ) ) );
219 gurobi.addEqConstraint( terms, 0 );
220 }
221 else
222 {
223 if ( relax )
224 {
225 /*
226 We have added f - b >= 0 and f >= 0. Additionally, we add
227 (ub - slope * lb) / (ub - lb) * (b - ub) >= (f - ub)
228 which is the upper bound in the triangular relaxation
229 */
230
231 double lambda = ( sourceUb - slope * sourceLb ) / ( sourceUb - sourceLb );
232 List<GurobiWrapper::Term> terms;
233 terms.append( GurobiWrapper::Term( lambda, Stringf( "x%u", sourceVariable ) ) );
234 terms.append( GurobiWrapper::Term( -1, Stringf( "x%u", targetVariable ) ) );
235 gurobi.addGeqConstraint( terms, ( lambda - 1 ) * sourceUb );
236 }
237 else
238 {
239 double xPoints[3];
240 double yPoints[3];
241 xPoints[0] = sourceLb;
242 yPoints[0] = slope * sourceLb;
243 xPoints[1] = 0;
244 yPoints[1] = 0;
245 xPoints[2] = sourceUb;
246 yPoints[2] = sourceUb;
247 gurobi.addPiecewiseLinearConstraint( Stringf( "x%u", sourceVariable ),
248 Stringf( "x%u", targetVariable ),
249 3,
250 xPoints,

Callers

nothing calls this directly

Calls 13

StringfClass · 0.85
getSlopeMethod · 0.80
TermClass · 0.50
isActiveMethod · 0.45
phaseFixedMethod · 0.45
getBMethod · 0.45
getFMethod · 0.45
getLowerBoundMethod · 0.45
getUpperBoundMethod · 0.45
appendMethod · 0.45
addEqConstraintMethod · 0.45
addGeqConstraintMethod · 0.45

Tested by

no test coverage detected