News for hackers. Stuff that matters.
Re:The Silent (R)evolution of SAT by bmc7505 on Friday May 26, 2023 @01:18PM (#36087057)
It depends on the sharding granularity. If you choose a low sharding ratio, then you waste a whole core, but that's assuming 1:1 shards to cores. If you shatter the search space using a large multiple of the number of cores, e.g. 1000:1, then shuffle the shards and have each core pick a shard off the queue, if any core ever gets stuck with a bad shard (i.e., conflict), it discards and picks a new one off the queue. This requires no communication and ensures all cores stay hot. I guess you might also need some preprocessing to remove trivially-conflicting shards.
Re:The Silent (R)evolution of SAT by klyrs on Saturday May 27, 2023 @12:58AM (#36092189)
You're not wrong, but it still only works for the most naive algorithm.