Question about edge case

[sirandreww]

I'm trying to build a witness file for an AIG that has all initial states violate the constraints. Meaning that the model is safe simply because a counter example cannot exist. Is there a way for me to do this without folding the constraint? Currently I am attempting to encode the property as "original property AND the constraints are not violated".

Here are more details: Original AIG:

aag 9 3 2 0 4 1 1
2
4
6
8 15 8
10 14 1
2
15
12 8 1
14 10 1
16 14 10
18 17 13

Witness File:

aag 10 3 2 0 5 1 1
2
4
6
8 15 8
10 14 1
21
15
12 8 1
14 10 1
16 14 10
18 17 13
20 15 3
c
WITNESS for some AIG file, this file should be checked by certifaiger.
Original output wires: []
Original bad wires: [2]
Original constraint wires: [15]

[Froleyks]

Without checking your (very detailed, thank you!) example, have you checked out the constraint branch? If we don't find a flaw in the theory, it will be merged this week. It basically does exactly that, not needing to fold the constraint into the property.

[sirandreww]

I will check it out, thank you :)

[Froleyks]

I look into your example. No, the constraint branch does not help. To produce a (trivial) witness for your R ^ C = false circuit you could do:

R' = P' = false F' = F C' = C

However, in Aiger R' = false is difficult to express. Usually, constraints are there for exactly this kind of thing... but the very strong P => P' check doesn't allow this. We are working on a more relaxed version that ensures that C' syntactically only depends on shared variables and would make it easier to produce witnesses for this.

Any update to the checker will only make it more relaxed, so previously valid certificates will not be invalidated.

Is this just an edge case optimization in case it comes up in the actual benchmark, or can this situation (R => -C) occur in your model checking algorithm?

[sirandreww]

In the meantime this comes up in randomly generated tests that I'm doing to prepare for HWMCC. So not part of the algorithm, but a possible input to the model checker. Why would a syntactic check of shared variables suffice to check constraints?

[Froleyks]

C' is still part of the other checks. We check if C' depends on a literal not in the original model to then switch to a stronger version (QBF) for some of the checks that is more likely to pass.

[Froleyks]

I did some theory and updated the (experimental) constraint branch. The shared constraint test resulting in QBFs is currently disabled since I don't want to deal with QBF if possible and don't have an example of an (aiger) model checking algorithm requiring it. Your witness still doesn't pass (are you convinced it should?). But you can replace the Bad and Constraint with 0 (line 7+8) and the witness passes.

[Froleyks]

Constraint has been merged into main. Please report if you still have problems building your desired witnesses.

[sirandreww]

Testing now, I'll let you know