Gives non-satisfying assignments as output

[yashpote]

Hi,

I ran this command
python3 waps.py registerlesSwap.sk_3_10.cnf

The samples I got were
1, -2 -3 4 5 -6 7 -8 9 -10 -11
2, -2 3 -4 5 -6 -7 -8 -9 10 -11
3, 2 3 4 5 -6 7 -8 9 -10 -11
4, 2 3 4 -5 6 7 8 -9 -10 -11
5, -2 -3 4 5 -6 7 -8 9 -10 -11
6, -2 3 -4 -5 6 7 8 9 -10 -11
7, 2 -3 4 -5 6 7 8 -9 -10 -11
8, 2 -3 4 5 -6 7 8 -9 -10 -11
9, -2 -3 4 5 -6 7 8 -9 -10 -11
10, -2 -3 -4 -5 6 7 8 -9 -10 -11

The second sample does not satisfy the CNF.
This can be confirmed by adding the clause 10 0 to the CNF and then
cryptominisat5 registerlesSwap.sk_3_10_extraClause.cnf which returns UNSAT

registerlesSwap.sk_3_10_extraClause.zip
registerlesSwap.sk_3_10.zip