Advanced

Change History

Topics that don't fit elsewhere, but still are related to challenge checkers.

Message: Re: Checker timing out

Changed By: PattuX
Change Date: January 02, 2020 01:16AM

Re: Checker timing out
As I said earlier it's not that surprising. Many finds usually just implies many DT/attribute combinations and basically free choice of attributes for each cell. It is just for users with few finds, but still enough to fill the DT grid, that it becomes rather hard to find a solution. And checking ALL combinations is really, really, really impossible. If there are for example 10 possible choices per cell that'd make 10^81 possiblities, a bit more than the number of atoms in the universe. The checker currently is a bit smarter than that but I suspect for some of these hard users it would still take years to check.

Locally, I used a SAT solver which has the advantage of being able to "learn" from failed attempts and recognize future attempts that would fail in a similar way earlier. The issue is that challenge checkers are not allowed to use any external resources outside of the ones PGC provides. So I'd have to write my own SAT solver in Lua and have it in a checker script. I've wanted to do this already anyway at some point, but it will probably take some time.

Oh, and as rrrragan mentioned the 50 second limit is esentially a timeout. The scriptwriter automatically stops the search after 50 seconds if it didn't give any results and then leaves 10 seconds to produce output and such. If you didn't interrupt the search in the script but let the server cancel the checker request the user would just get a not so nice error message.
Changed By: PattuX
Change Date: January 02, 2020 01:16AM

Re: Checker timing out
As I said earlier it's not that surprising. Many finds usually just implies many DT/attribute combinations and basically free choice of attributes for each cell. It is just for users with few finds, but still enough to fill the DT grid, that it becomes rather hard to find a solution. And checking ALL combinations is really, really, really impossible. If there are for example 10 possible choices per cell that'd make 10^81 possiblities, a bit more than the number of atoms in the universe. The checker currently is a bit smarter than that but I suspect for some of these hard users it would still take years to check.

Locally, I used a SAT solver which has the advantage of being able to "learn" from failed attempts and recognize future attempts that would fail in a similar way earlier. The issue is that challenge checkers are not allowed to use any external resources outside of the ones PGC provides. So I'd have to write my own SAT solver in Lua and have it in a checker script. I've wanted to do this already anyway at some point, but it will probably take some time.

Oh, and as rrgan mentioned the 50 second limit is esentially a timeout. The scriptwriter automatically stops the search after 50 seconds if it didn't give any results and then leaves 10 seconds to produce output and such. If you didn't interrupt the search in the script but let the server cancel the checker request the user would just get a not so nice error message.

Original Message

Author: PattuX
Date: January 02, 2020 12:41AM

Re: Checker timing out
As I said earlier it's not that surprising. Many finds usually just implies many DT/attribute combinations and basically free choice of attributes for each cell. It is just for users with few finds, but still enough to fill the DT grid, that it becomes rather hard to find a solution. And checking ALL combinations is really, really, really impossible. If there are for example 10 possible choices per cell that'd make 10^81 possiblities, a bit more than the number of atoms in the universe. The checker currently is a bit smarter than that but I suspect for some of these hard users it would still take years to check.

Locally, I used a SAT solver which has the advantage of being able to "learn" from failed attempts and recognize future attempts that would fail in a similar way earlier. The issue is that challenge checkers are not allowed to use any external resources outside of the ones PGC provides. So I'd have to write my own SAT solver in Lua and have it in a checker script. I've wanted to do this already anyway at some point, but it will probably take some time.