Skip to content

Disabling Query Optimization in MarabouCore to Preserve Intermediate Variable Bounds #877

@ace-shifu

Description

@ace-shifu

Description

When using the pip-installed maraboupy library, MarabouCore appears to optimize queries during preprocessing, causing intermediate variables (x2, x3, x4, x5 in my case) to lose their bounds information (showing min/max float values instead). How can we disable this optimization to preserve bounds for intermediate variables?

Minimal Reproduction

from maraboupy import MarabouCore
from maraboupy.Marabou import createOptions

# Initialize query
inputQuery = MarabouCore.InputQuery()
inputQuery.setNumberOfVariables(8)

# Mark input variables
inputQuery.markInputVariable(0, 0)
inputQuery.markInputVariable(1, 1)

# Define equations (x2 = x0+x1, x3 = x0-x1)
equation1 = MarabouCore.Equation()
equation1.addAddend(1, 0)
equation1.addAddend(1, 1)
equation1.addAddend(-1, 2)
equation1.setScalar(0)
inputQuery.addEquation(equation1)

equation2 = MarabouCore.Equation()
equation2.addAddend(1, 0)
equation2.addAddend(-1, 1)
equation2.addAddend(-1, 3)
equation2.setScalar(0)
inputQuery.addEquation(equation2)

# Add clip constraints (x4 = clip(x2,0,3), x5 = clip(x3,-0.5,1))
MarabouCore.addClipConstraint(inputQuery, 2, 4, 0, 3)
MarabouCore.addClipConstraint(inputQuery, 3, 5, -0.5, 1)

# Set input bounds
inputQuery.setLowerBound(0, -1.1)
inputQuery.setUpperBound(0, -1.0)
inputQuery.setLowerBound(1, -2.1)
inputQuery.setUpperBound(1, -2.0)

# Calculate bounds
options = createOptions()
exitCode, bounds, stats = MarabouCore.calculateBounds(inputQuery, options, "")

Observed Behavior

Preprocessing reduces the equation count (from 10 to 8) and variable count (from 16 to 11). Intermediate variables show unbounded behavior:

bound of x2: (-1.79e+308, 1.79e+308)
bound of x3: (-1.79e+308, 1.79e+308)
bound of x4: (-1.79e+308, 1.79e+308) 
bound of x5: (-1.79e+308, 1.79e+308)

Expected Behavior

Intermediate variables should respect their natural bounds derived from:

x2 = x0 + x1 → (-3.2, -3.0)
x3 = x0 - x1 → (0.9, 1.0)
x4 = clip(x2,0,3) → [0,3]
x5 = clip(x3,-0.5,1) → [0.9,1.0]

So, What configuration option(s) can disable the preprocessing optimization that removes these variable bounds? We need to retain bounds information for intermediate variables in our analysis pipeline.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions