upper bound disappears

[davideklund]

I ran the following simple example with maraboupy:

from maraboupy import Marabou
from maraboupy import MarabouCore
from maraboupy.Marabou import createOptions

inquery = MarabouCore.InputQuery()
inquery.setNumberOfVariables(1)

inquery.setLowerBound(0, 1.5)
inquery.setUpperBound(0, 0.5)

options = createOptions()
exitCode, variables, stats = MarabouCore.solve(inquery, options, "")

print(exitCode)
print(variables)

I got the result sat with model as follows:

sat
{0: 1.5}

The upper bound seems to be preprocessed away. I expected unsat because of the incompatible upper and lower bounds. Is this the expected behavior?

Python version: 3.9
maraboupy version: 2.0.0
Operating system: Ubuntu-20-04

Full output:

Engine::processInputQuery: Input query (before preprocessing): 0 equations, 1 variables
Engine::processInputQuery: Input query (after preprocessing): 0 equations, 0 variables

Input bounds:

Branching heuristics set to PseudoImpact

Engine::solve: Initial statistics

17:08:27 Statistics update:
        --- Time Statistics ---
        Total time elapsed: 0 milli (00:00:00)
                Main loop: 0 milli (00:00:00)
                Preprocessing time: 0 milli (00:00:00)
                Unknown: 0 milli (00:00:00)
        Breakdown for main loop:
                [0.00%] Simplex steps: 0 milli
                [0.00%] Explicit-basis bound tightening: 0 milli
                [0.00%] Constraint-matrix bound tightening: 0 milli
                [0.00%] Degradation checking: 0 milli
                [0.00%] Precision restoration: 0 milli
                [0.00%] Statistics handling: 0 milli
                [0.00%] Constraint-fixing steps: 0 milli
                [0.00%] Valid case splits: 0 milli. Average per split: 0.00 milli
                [0.00%] Applying stored bound-tightening: 0 milli
                [0.00%] SMT core: 0 milli
                [0.00%] Symbolic Bound Tightening: 0 milli
                [0.00%] SoI-based local search: 0 milli
                [0.00%] SoI-based local search: 0 milli
                [0.00%] Unaccounted for: 0 milli
        --- Preprocessor Statistics ---
        Number of preprocessor bound-tightening loop iterations: 1
        Number of eliminated variables: 1
        Number of constraints removed due to variable elimination: 0
        Number of equations removed due to variable elimination: 0
        --- Engine Statistics ---
        Number of main loop iterations: 1
                0 iterations were simplex steps. Total time: 0 milli. Average: 0.00 milli.
                0 iterations were constraint-fixing steps. Total time: 0 milli. Average: 0.00 milli
        Number of active piecewise-linear constraints: 0 / 0
                Constraints disabled by valid splits: 0. By SMT-originated splits: 0
        Last reported degradation: 0.0000000000. Max degradation so far: 0.0000000000. Restorations so far: 0
        Number of simplex pivots we attempted to skip because of instability: 0.
        Unstable pivots performed anyway: 0
        --- Tableau Statistics ---
        Total number of pivots performed: 0
                Real pivots: 0. Degenerate: 0 (0.00%)
                Degenerate pivots by request (e.g., to fix a PL constraint): 0 (0.00%)
                Average time per pivot: 0.00 milli
        Total number of fake pivots performed: 0
        Total number of rows added: 0. Number of merged columns: 0
        Current tableau dimensions: M = 0, N = 0
        --- SMT Core Statistics ---
        Total depth is 0. Total visited states: 1. Number of splits: 0. Number of pops: 0
        Max stack depth: 0
        --- Bound Tightening Statistics ---
        Number of tightened bounds: 0.
                Number of rows examined by row tightener: 0. Consequent tightenings: 0
                Number of explicit basis matrices examined by row tightener: 0. Consequent tightenings: 0
                Number of bound tightening rounds on the entire constraint matrix: 0. Consequent tightenings: 0
                Number of bound notifications sent to PL constraints: 0. Tightenings proposed: 0
        --- Basis Factorization statistics ---
        Number of basis refactorizations: 2
        --- Projected Steepest Edge Statistics ---
        Number of iterations: 0.
        Number of resets to reference space: 1. Avg. iterations per reset: 0
        --- SBT ---
        Number of tightened bounds: 0
        --- SoI-based local search ---
        Number of proposed phase pattern update: 0. Number of accepted update: 0 [0.00%]
        Total time (% of local search time) updating SoI phase pattern : 0 milli [0.00%]
        Total time obtaining current assignment: 0 milli [0.00%]
        Total time getting SoI phase pattern : 0 milli [0.00%]
        --- Context dependent statistics ---
        Number of pushes / pops: 0 / 0
                [0.00%] Pre-Push hook: 0 milli
                [0.00%] Push : 0 milli
                [0.00%] Post-Pop hook: 0 milli
                [0.00%] Pop : 0 milli
                [0.00%] Total context-switching time: 0 milli
        --- Proof Certificate ---
        Number of certified leaves: 0
        Number of leaves to delegate: 0

---

Engine::solve: sat assignment found

17:08:27 Statistics update:
        --- Time Statistics ---
        Total time elapsed: 0 milli (00:00:00)
                Main loop: 0 milli (00:00:00)
                Preprocessing time: 0 milli (00:00:00)
                Unknown: 0 milli (00:00:00)
        Breakdown for main loop:
                [0.00%] Simplex steps: 0 milli
                [0.00%] Explicit-basis bound tightening: 0 milli
                [0.00%] Constraint-matrix bound tightening: 0 milli
                [0.00%] Degradation checking: 0 milli
                [0.00%] Precision restoration: 0 milli
                [0.00%] Statistics handling: 0 milli
                [0.00%] Constraint-fixing steps: 0 milli
                [0.00%] Valid case splits: 0 milli. Average per split: 0.00 milli
                [0.00%] Applying stored bound-tightening: 0 milli
                [0.00%] SMT core: 0 milli
                [0.00%] Symbolic Bound Tightening: 0 milli
                [0.00%] SoI-based local search: 0 milli
                [0.00%] SoI-based local search: 0 milli
                [100.00%] Unaccounted for: 0 milli
        --- Preprocessor Statistics ---
        Number of preprocessor bound-tightening loop iterations: 1
        Number of eliminated variables: 1
        Number of constraints removed due to variable elimination: 0
        Number of equations removed due to variable elimination: 0
        --- Engine Statistics ---
        Number of main loop iterations: 2
                0 iterations were simplex steps. Total time: 0 milli. Average: 0.00 milli.
                0 iterations were constraint-fixing steps. Total time: 0 milli. Average: 0.00 milli
        Number of active piecewise-linear constraints: 0 / 0
                Constraints disabled by valid splits: 0. By SMT-originated splits: 0
        Last reported degradation: 0.0000000000. Max degradation so far: 0.0000000000. Restorations so far: 0
        Number of simplex pivots we attempted to skip because of instability: 0.
        Unstable pivots performed anyway: 0
        --- Tableau Statistics ---
        Total number of pivots performed: 0
                Real pivots: 0. Degenerate: 0 (0.00%)
                Degenerate pivots by request (e.g., to fix a PL constraint): 0 (0.00%)
                Average time per pivot: 0.00 milli
        Total number of fake pivots performed: 0
        Total number of rows added: 0. Number of merged columns: 0
        Current tableau dimensions: M = 0, N = 0
        --- SMT Core Statistics ---
        Total depth is 0. Total visited states: 1. Number of splits: 0. Number of pops: 0
        Max stack depth: 0
        --- Bound Tightening Statistics ---
        Number of tightened bounds: 0.
                Number of rows examined by row tightener: 0. Consequent tightenings: 0
                Number of explicit basis matrices examined by row tightener: 1. Consequent tightenings: 0
                Number of bound tightening rounds on the entire constraint matrix: 0. Consequent tightenings: 0
                Number of bound notifications sent to PL constraints: 0. Tightenings proposed: 0
        --- Basis Factorization statistics ---
        Number of basis refactorizations: 2
        --- Projected Steepest Edge Statistics ---
        Number of iterations: 0.
        Number of resets to reference space: 1. Avg. iterations per reset: 0
        --- SBT ---
        Number of tightened bounds: 0
        --- SoI-based local search ---
        Number of proposed phase pattern update: 0. Number of accepted update: 0 [0.00%]
        Total time (% of local search time) updating SoI phase pattern : 0 milli [0.00%]
        Total time obtaining current assignment: 0 milli [0.00%]
        Total time getting SoI phase pattern : 0 milli [0.00%]
        --- Context dependent statistics ---
        Number of pushes / pops: 0 / 0
                [0.00%] Pre-Push hook: 0 milli
                [0.00%] Push : 0 milli
                [0.00%] Post-Pop hook: 0 milli
                [0.00%] Pop : 0 milli
                [0.00%] Total context-switching time: 0 milli
        --- Proof Certificate ---
        Number of certified leaves: 0
        Number of leaves to delegate: 0
sat
{0: 1.5}

[wu-haoze]

Hi David, thanks for pointing this out. This indeed seems to be an uncommon case that’s not handled properly. I’ll look into it and submit a fix. Andrew

[davideklund]

Great, thanks a lot!