Invalid SAT Witness (with Colab Reproduction)

[YalcinerMustafa]

Hi Marabou team,

I encountered a case where Marabou returns a SAT witness that violates a linear equality constraint explicitly specified in the .ipq file. To demonstrate the issue, I’ve created a Google Colab script that uses maraboupy to load and solve the query (which represents a ReLU neural network), and then shows that one of the linear equality constraints is actually not satisfied by the returned witness.

The main steps in the colab are as follows:

1. Solving the Query with Marabou
   The script first loads an .ipq file that captures the input-output behavior of a neural network.
   Then, Marabou solves the query and returns a SAT witness where all input variables are set to 0 and values are assigned to all intermediate and output variables.

2. Manual Evaluation of a Constraint
   We select one specific linear equality constraint from the .ipq file for which we know that the constraint is violated.
   The constraint is specified in the colab and is of the form:
   x_target = a₁ * x₁ + a₂ * x₂ + ... + aₙ * xₙ
   We use Marabou’s values for the variables on the right-hand side to compute a value for x_target based on this equation in our own python code. Then we compare this computed value to the value Marabou assigned to x_target.

3. Discrepancy Detection
   The manually computed value of x_target does not match the value assigned by Marabou in its solution. The difference is significant, showing that the constraint is violated and that the SAT witness is incorrect.

4. Sanity Check via ONNX Runtime
   The variable x_target happens to correspond to the output node of the neural network. We independently evaluate the network using ONNX Runtime on the fixed input and obtain a value for the output node. This ONNX-derived value matches our manual computation, confirming that the Marabou-assigned value is incorrect.

I’ve encountered similar incorrect SAT witnesses in other cases as well and was not yet able to come up with a workaround for them.
That is why I'd highly appreciate any advice on this issue and I am happy to provide more details.

Best regards,

Mustafa

Link to relevant files that are also automatically downloaded within the colab:

[tempate]

Hello. I have come across the same issue using Marabou with onnx. Setting solveWithMILP=False solved it for me.

[YalcinerMustafa]

@tempate Thank you very much for your suggestion.

Unfortunately, it did not resolve our issue.
According to the documentation, solveWithMILP determines whether the InputQuery should be solved using a MILP encoding, thereby bypassing the Reluplex implementation [1].
The default value is already solveWithMILP=False, which is what we're using in our Colab environment.

Although we do intend to use the Reluplex algorithm, we also tested setting solveWithMILP=True with the Gurobi backend, but this resulted in the same error.

[1] From Marabou.py:
solveWithMILP (bool, optional): Whether to solve the input query with a MILP encoding. Currently only works when Gurobi is installed. Defaults to False.

[paulsushmita]

Hello @YalcinerMustafa!

I am facing a similar issue where Marabou finds a satisfying assignment but the assignment violates the input bound constraints. Could you find a solution to your problem?

[YalcinerMustafa]

Hello @paulsushmita
thanks for sharing.
Unfortunately, we could not find a bugfix.
We presume that the bug might be due to numeric instability within Marabou, making it very hard to fix when unfamiliar with the code.