search

anniecherk / sweetpea-py

MIT License
1 stars 0 forks source link

Occasional duplicate solutions? #1

Closed drautb closed 6 years ago

drautb commented 6 years ago

I've noticed that sometimes when I run SweetPea on the basic Stroop test, the following solution is output twice:

color blue | text blue | congruent? con
color red  | text blue | congruent? inc
color red  | text red  | congruent? con
color blue | text red  | congruent? inc

The two corresponding solutions from unigen are:

v-1 2 -3 4 5 -6 7 -8 -9 10 -11 12 13 -14 15 -16 17 -18 -19 20 21 -22 -23 24 -25 -26 -27 28 -29 30 -31 -32 33 -34 -35 -36 -37 -38 39 -40 -41 -42 -43 44 -45 -46 47 -48 -49 50 -51 -52 53 -54 -55 56 -57 -58 59 -60 -61 62 -63 -64 65 -66 -67 68 -69 -70 71 -72 -73 74 -75 -76 77 -78 -79 80 -81 -82 -83 -84 -85 86 -87 -88 -89 -90 -91 -92 -93 94 -95 -96 97 -98 -99 -100 -101 -102 -103 -104 105 -106 -107 108 -109 -110 -111 -112 113 -114 -115 -116 -117 -118 119 -120 -121 0:1
v-1 2 -3 4 5 -6 7 -8 -9 10 -11 12 13 -14 15 -16 17 -18 -19 20 21 -22 -23 24 -25 -26 -27 28 -29 30 -31 -32 33 -34 -35 -36 -37 -38 39 -40  41 -42 -43 44 -45 -46 47 -48 -49 50 -51 -52 53 -54 -55 56 -57 -58 59 -60 -61 62 -63 -64 65 -66 -67 68 -69 -70 71 -72 -73 74 -75 -76 77 -78 -79 80 -81 -82 -83 -84 -85 86 -87 -88 -89 -90 -91 -92 -93 94 -95 -96 97 -98 -99 -100 -101 -102 -103 -104 105 -106 -107 108 -109 -110 -111 -112 113 -114 -115 -116 -117 -118 119 -120 -121 0:1

The assignments for the first 24 variables are identical, which explains the duplicate output. In fact, the only variable assignment that is different between the two solutions is 41, it's true for one solution, and false in the other.

I'm not sure yet if this is a bug in what the python code is generating, or the backend, but I figured I'd record it here so we don't forget about it.

drautb commented 6 years ago

@anniecherk I realized during our discussion today that when I was working on making the core generate the full CNF file, I hadn't seen variable 41 in the formula at all. I think this may just be an off-by-one error. The frontend is providing 41 to the backend as the fresh variable, but then maybe the backend increments fresh before using it, so it starts with 42, leaving 41 unconstrained?

I haven't verified, but that's what came to mind this morning. I imagine that if the frontend provided the last used variable as the fresh variable, rather than 1 + the last used variable, then this wouldn't be an issue.

drautb commented 6 years ago

This was resolved by 9e5f537de6a84d3e67e2c5b8f6a7d59fa5cc277d.