[Bug report] SAT value assignment where inputs do not respect the bounds #883
Description
Hi team,
I was using Marabou as a verifier to get explanations, where I have some input bounds and output constraints. I happened to look into the SAT assignment values and it seems that there exists at least one of the inputs (in a single SAT instance) which is assigned a value that violates the bound constraints.
...
...
...
375 36.2586881171909
#Violations: 1
375 36.742568132079505
#Violations: 1
375 37.65474850399638
#Violations: 1
375 36.56927988878896
#Violations: 1
375 36.75547149581293
#Violations: 1
375 37.42207874929872
#Violations: 1
375 37.18463553240071
#Violations: 1
SAT set/explanation: [364, 483, 713, 742, 186, 316, 230, 160, 599, 469, 743, 317, 158, 746, 745, 602, 2, 529, 525, 537, 543, 53, 234, 384, 568, 311, 0, 292, 360, 598, 31, 85, 724, 509, 372, 748, 588, 15, 244, 327, 17, 437, 269, 682, 770, 619, 780, 539, 348, 601, 169, 181, 512, 755, 206, 112, 10, 163, 683, 27, 218, 727, 666, 382, 383, 594, 698, 608, 275, 354, 668, 470, 584, 428, 301, 587, 600, 150, 376, 597, 154, 268, 52, 596, 130, 627, 661, 260, 216, 109, 164, 179, 654, 182, 540, 593, 125, 161, 592, 686, 297, 313, 16, 581, 298, 552, 488, 231, 320, 591, 532, 172, 465, 442, 312, 400, 630, 296, 340, 744, 284, 691, 72, 657, 670, 207, 707, 451, 708, 30, 566, 617, 639, 353, 233, 663, 289, 519, 42, 726, 414, 147, 330, 547, 14, 180, 413, 675, 183, 562, 391, 106, 419, 411, 377, 638, 709, 350, 399, 255, 344, 229, 610, 341, 655, 692, 548, 589, 612, 714, 632, 621, 518, 585, 492, 259, 705, 100, 358, 386, 696, 626, 622, 205, 326, 405, 635, 396, 447, 355, 191, 199, 491, 71, 563, 557, 299, 507, 472, 81, 667, 646, 192, 132, 738, 631, 201, 658, 352, 496, 409, 455, 545, 435, 381, 325, 475, 136, 407, 333, 710, 278, 371, 456, 736, 583, 423, 131, 464, 258, 433, 463, 611, 329, 171, 227, 490, 256, 665, 628, 535, 146, 694, 609, 436, 116, 516, 718, 162, 502, 693, 441, 637, 393, 408, 118, 629, 378, 506, 735, 648, 323, 473, 380, 662, 586, 530, 427, 737, 664, 725, 636, 734, 379, 647, 351, 559, 719, 417, 702, 117, 324, 720, 434, 142, 517, 406, 489, 283, 461, 137, 462, 200, 145, 251, 421, 733, 620, 143, 505, 450, 389, 732, 362, 144, 114, 771, 228, 477, 531, 590, 449, 558, 618, 723, 193, 751, 250, 334, 86, 361, 478, 249, 695, 418, 422, 697, 390, 446, 474]
Number of violated SAT assignments = 330
Explanation size = 330
In the above example, the output is of the form:
<pixel_number> <input_val_of_pixel>
#Violations: <number_of_input_violations_in_the_SAT_assignment>
followed by the explanation, its size and the number of SAT responses with any input value where the bound is not respected.
The above case is of MNIST digits and the input is normalised to be in [0,1], while we can see in the example output, pixel 375 gets a value 37.18463553240071.
- Yes, it is reproduced in Marabou installation via
pip(v2.0.0) as well as GitHub's latest version, August '24 and April '24 versions. - In the given example, it is not only pixel
375that gets an invalid assignment. There are other pixels as well in other SAT responses with an invalid value.
Queries:
Q. Is it something that I am misunderstanding? If yes, can you please clarify where I am possibly going wrong?
Q. Is there a specific instance of type of constraint that is resulting this type of issue?
Hoping @MatthewDaggitt (probably a more recent and active contributor to Marabou?), @wu-haoze or any of the authors/contributors can answer the queries.
Looking forward to a response. Please feel free to ask any question that can help clarify the issue. I am happy to test in other setting as much as possible.
Best,
Sushmita