Statistics Update Verbosity

[SuryaB1]

System Info: 2019 Intel Core i9 MacBook Pro macOS Ventura 13.4 (22F66) Python 3.8.16

Hi,

I'm running a program that performs thousands of queries on Marabou via the Python API, and my program outputs some logs right before each query occurs. Starting after about 20 seconds of program execution (with output consisting of my program's logs and Marabou statistics logs), I have been only seeing Marabou's statistics logs for more than an hour now, and I believe either one of two things is happening.

My first guess as to what is happening is that all of the program's queries have been completed and now Marabou is outputting overdue statistics updates. I suspect this because I do not see my program's logs anymore, and my program's logs for my last query were printed in the middle of one of Marabou's statistics updates. If this guess is true, I would like to turn off these statistics updates. I attempted to do so by setting the verbose parameter of MaraboutNetwork.solve() to False, which did not work.

Q1: How can I turn off these statistics updates, if this interpretation is correct?

My second guess was that all of these statistics updates are corresponding to Marabou's processing of just my last query, meaning I would need to go look into what is wrong with my last query before all of these statistic updates.

Q2: What interpretation regarding these statistic updates is correct?

Thank you!

Below is one such statistics update out of the many that were printed:

23:24:20 Statistics update:
        --- Time Statistics ---
        Total time elapsed: 4335925 milli (01:12:15)
                Main loop: 4335905 milli (01:12:15)
                Preprocessing time: 19 milli (00:00:00)
                Unknown: 1 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: 46 milli
                [0.00%] Precision restoration: 0 milli
                [0.48%] Statistics handling: 20953 milli
                [0.00%] Constraint-fixing steps: 0 milli
                [0.67%] Valid case splits: 29146 milli. Average per split: 0.00 milli
                [0.01%] Applying stored bound-tightening: 543 milli
                [92.56%] SMT core: 4013436 milli
                [4.47%] Symbolic Bound Tightening: 193658 milli
                [0.00%] SoI-based local search: 0 milli
                [0.00%] SoI-based local search: 0 milli
                [1.80%] Unaccounted for: 78119 milli
        --- Preprocessor Statistics ---
        Number of preprocessor bound-tightening loop iterations: 9
        Number of eliminated variables: 10
        Number of constraints removed due to variable elimination: 4
        Number of equations removed due to variable elimination: 0
        --- Engine Statistics ---
        Number of main loop iterations: 4850000
                4 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: 430 / 622
                Constraints disabled by valid splits: 0. By SMT-originated splits: 192
        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: 4
                Real pivots: 4. 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 = 8, N = 19
        --- SMT Core Statistics ---
        Total depth is 289. Total visited states: 2910029. Number of splits: 1939966. Number of pops: 970062
        Max stack depth: 290
        --- Bound Tightening Statistics ---
        Number of tightened bounds: 6788953.
                Number of rows examined by row tightener: 4. Consequent tightenings: 6
                Number of explicit basis matrices examined by row tightener: 1. Consequent tightenings: 7
                Number of bound tightening rounds on the entire constraint matrix: 0. Consequent tightenings: 0
                Number of bound notifications sent to PL constraints: 5598. Tightenings proposed: 0
        --- Basis Factorization statistics ---
        Number of basis refactorizations: 2
        --- Projected Steepest Edge Statistics ---
        Number of iterations: 4.
        Number of resets to reference space: 4858762. Avg. iterations per reset: 0
        --- SBT ---
        Number of tightened bounds: 6788953
        --- 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 : 18968619 milli [0.00%]
        Total time obtaining current assignment: 0 milli [0.00%]
        Total time getting SoI phase pattern : 140550 milli [0.00%]
        --- Context dependent statistics ---
        Number of pushes / pops: 6798727 / 6798438
                [0.07%] Pre-Push hook: 3001 milli
                [0.02%] Push : 668 milli
                [0.07%] Post-Pop hook: 3053 milli
                [0.05%] Pop : 2112 milli
                [0.20%] Total context-switching time: 8836 milli
        --- Proof Certificate ---
        Number of certified leaves: 0
        Number of leaves to delegate: 0

[wu-haoze]

Hi @SuryaB1 , if everything runs normally, then those can very likely be overdue statistics printing of several previous queries you run. To print things in real time (instead of backloading them to the end) you could add -u to your python command, e,g. python -u script.py

To turn off those outputs during the solving, you could set the verbosity flag when creating a Marabou option. https://github.com/NeuralNetworkVerification/Marabou/blob/8854d50af873364ef0c0ae61bc1d7144f9e9c519/maraboupy/examples/2_ONNXExample.py#L20-L58

[SuryaB1]

Thank you for the quick response. Using options = Marabou.createOptions(verbosity = 0) turned off all statistics updates.