3 ms·
Unlikely, for reasons explained in this video: https://youtu.be/bEovhfxJsM4?t=2339 https://youtu.be/bEovhfxJsM4?t=2339 However, apparently it can write a progr
by supersat 3y ago
Unlikely, for reasons explained in this video: https://youtu.be/bEovhfxJsM4?t=2339 https://youtu.be/bEovhfxJsM4?t=2339
However, apparently it can write a program using the Z3 SAT solver to find a solution.
- zacmps 3y agoIt seems like it might be possible to get around this by letting the model emit moves like ` discard last 5` which would also let it keep a history of it's previous branches.