oscarsuen / guessgame

Guessing Game Problem
0 stars 0 forks source link

Extra constraints in Z3 #8

Open oscarsuen opened 3 weeks ago

oscarsuen commented 3 weeks ago

We currently add both a symmetry constraint $p{i+1}=p{N-i}$ and a decreasing constraint $p_{i+1}<p_i$ for $i<\frac N2$. While not strictly necessary to find the solution, they may speed up the computation. We are unsure though because of #7.

Another option is to remove $p_i$ for $i>\frac N2$ altogether as variables.