6 ms·

Super short answer: SAT doesn’t exhibit the nice properties other optimization problems often have where you can tell when you’re near a correct answer. So it

Super short answer: SAT doesn’t exhibit the nice properties other optimization problems often have where you can tell when you’re near a correct answer. So it doesn’t resemble most continuous optimization problems. Regarding parallelism, there has been research into parallel SAT, but it’s hard in part due to the problem of sharing information between threads/tasks in conflict clause learning algorithms. I don’t remember specific papers but a quick search on google scholar or looking at past SAT competitions would turn up material if you’re interested in the topic.

bmc7505 3y ago
> SAT doesn’t exhibit the nice properties other optimization problems often have where you can tell when you’re near a correct answer. You mean like a metric? Not all SAT instances have a natural metric, maybe a large fraction could be relaxed to MAXSAT, but it seems parallel solvers are not very popular in that setting either, i.e., there is no parallel track and parallel solvers are disqualified [1] from participating. I'm not sure I follow how metrics are related to parallelism though. A naive strategy would be to try every assignment in parallel on 2^n processors. There are plenty of better strategies for search space splitting [2] and stochastic local search [3] algorithms that seem amenable to parallelization. [1]: https://maxsat-evaluations.github.io/2023/rules.html https://maxsat-evaluations.github.io/2023/rules.html [2]: http://sat.inesc-id.pt/~ruben/papers/martins-ictai10-talk.pdf http://sat.inesc-id.pt/~ruben/papers/martins-ictai10-talk.pd... [3]: https://link.springer.com/article/10.1023/A:1006350622830 https://link.springer.com/article/10.1023/A:1006350622830
- calf 3y ago
  n is like a million variables so you would need 2^n gazillion cores. I'm no expert but my thesis advisor is cited in the OP article, so I'm just guessing but it's an interesting question. It's not for the lack of trying in the part of SAT researchers; after the hardware advances with SAT solvers implementation in the early 2000s, they would've looked at parallelism and concurrency as well. But with continuous optimization (like with training machine learning), there's gradient descent which tells you where to guess next. But with Boolean logic there's nothing like that, the needle is either in the next bale of hay, or it isn't.
  - bmc7505 3y ago
    The 2^n idea is just a thought experiment, but you should be able to realize linear or close-to-linear speedup using a communication-free algorithm that shards the search space evenly across available cores, no? I don't see why this strategy isn't more widely used. I can see how continuity accelerates the search for solutions, but I see that more as an orthogonal property, not a limitation of parallelism. Even if your domain is continuous, accelerating gradient descent is nontrivial, and many discrete optimizations problems benefit from parallelism.
    - klyrs 3y ago
      It is obviously true that the worst-case runtime of a problem on n variables and m clauses is O(m2^n), and that the brute-force algorithm can be sharded out to 2k cores and run in time O(m2^(n-k)). If your approach is brute-force, yes, you might as well use this technique. But, notice that a shard whose k preset bits are in direct conflict should take zero time -- it's smarter to detect a conflict and terminate than carry on computing all 2^(n-k) invalid assignments. Each such conflicting shard decreases the benefit of your parallelization -- a depth-first solver wouldn't spend almost any time on that particular branch, but you've wasted a whole core on it. The real question is, what if your algorithm is smarter than brute force? Such algorithms may spend considerable time preprocessing, which is not trivially parallelized, resulting in many cores duplicating tons of work with very little effective speedup.
      - bmc7505 3y ago
        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.
- tgflynn 3y ago
  > there is no parallel track and parallel solvers are disqualified [1] from participating. Maybe that's as much a cause as an effect. What's the incentive to create and improve parallel solvers if there's no place that evaluates and rewards your work ?
  - zero_k 3y ago
    No, parallel SAT solvers are NOT disqualified, in fact there is a parallel track. Seriously? Every year there is a winner for the parallel track. Here's last year's: https://satcompetition.github.io/2022/results.html https://satcompetition.github.io/2022/results.html
    - bmc7505 3y ago
      That’s SATComp, I was talking about the MAXSAT competition.
- andrewprock 3y ago
  Unless I'm missing something, space splitting should be trivial. If you have two cores and three propositional variables x1, x2, x3, you could simply set x1 to tier on one core and false on the other, and then perform two parallel SAT searches on a space with one less variable.
  - bmc7505 3y ago
    Using a naive splitting strategy is trivial, but ensuring the distribution is well-balanced across the subspaces is not. You need to preprocess the formula by setting the variables, then doing some propagation, then restarting, otherwise one core will get stuck doing a bunch of useless work.
  - c-cube 3y ago
    The difficulty is which variables to pick so that all subspaces are of comparable difficulty. Cube and conquer is a nice paper on that problem.
  - thesz 3y ago
    What you describe looks like cube-and-conquer technique [1]. [1] https://www.cs.utexas.edu/~marijn/publications/cube.pdf https://www.cs.utexas.edu/~marijn/publications/cube.pdf The thing is much more deeper than what you described. You need to choose which variables you will assign, that's first. Then you have to assign them, and it is important to do as carefully because assignment may produce inbalanced search space. Splitting on one variable when there are hundredths of thousands of them is very, very inefficient.

bmc7505 3y ago

> SAT doesn’t exhibit the nice properties other optimization problems often have where you can tell when you’re near a correct answer. You mean like a metric? Not all SAT instances have a natural metric, maybe a large fraction could be relaxed to MAXSAT, but it seems parallel solvers are not very popular in that setting either, i.e., there is no parallel track and parallel solvers are disqualified [1] from participating. I'm not sure I follow how metrics are related to parallelism though. A naive strategy would be to try every assignment in parallel on 2^n processors. There are plenty of better strategies for search space splitting [2] and stochastic local search [3] algorithms that seem amenable to parallelization. [1]: https://maxsat-evaluations.github.io/2023/rules.html https://maxsat-evaluations.github.io/2023/rules.html [2]: http://sat.inesc-id.pt/~ruben/papers/martins-ictai10-talk.pdf http://sat.inesc-id.pt/~ruben/papers/martins-ictai10-talk.pd... [3]: https://link.springer.com/article/10.1023/A:1006350622830 https://link.springer.com/article/10.1023/A:1006350622830

calf 3y ago
n is like a million variables so you would need 2^n gazillion cores. I'm no expert but my thesis advisor is cited in the OP article, so I'm just guessing but it's an interesting question. It's not for the lack of trying in the part of SAT researchers; after the hardware advances with SAT solvers implementation in the early 2000s, they would've looked at parallelism and concurrency as well. But with continuous optimization (like with training machine learning), there's gradient descent which tells you where to guess next. But with Boolean logic there's nothing like that, the needle is either in the next bale of hay, or it isn't.
- bmc7505 3y ago
  The 2^n idea is just a thought experiment, but you should be able to realize linear or close-to-linear speedup using a communication-free algorithm that shards the search space evenly across available cores, no? I don't see why this strategy isn't more widely used. I can see how continuity accelerates the search for solutions, but I see that more as an orthogonal property, not a limitation of parallelism. Even if your domain is continuous, accelerating gradient descent is nontrivial, and many discrete optimizations problems benefit from parallelism.
  - klyrs 3y ago
    It is obviously true that the worst-case runtime of a problem on n variables and m clauses is O(m2^n), and that the brute-force algorithm can be sharded out to 2k cores and run in time O(m2^(n-k)). If your approach is brute-force, yes, you might as well use this technique. But, notice that a shard whose k preset bits are in direct conflict should take zero time -- it's smarter to detect a conflict and terminate than carry on computing all 2^(n-k) invalid assignments. Each such conflicting shard decreases the benefit of your parallelization -- a depth-first solver wouldn't spend almost any time on that particular branch, but you've wasted a whole core on it. The real question is, what if your algorithm is smarter than brute force? Such algorithms may spend considerable time preprocessing, which is not trivially parallelized, resulting in many cores duplicating tons of work with very little effective speedup.
    - bmc7505 3y ago
      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.
tgflynn 3y ago
> there is no parallel track and parallel solvers are disqualified [1] from participating. Maybe that's as much a cause as an effect. What's the incentive to create and improve parallel solvers if there's no place that evaluates and rewards your work ?
- zero_k 3y ago
  No, parallel SAT solvers are NOT disqualified, in fact there is a parallel track. Seriously? Every year there is a winner for the parallel track. Here's last year's: https://satcompetition.github.io/2022/results.html https://satcompetition.github.io/2022/results.html
  - bmc7505 3y ago
    That’s SATComp, I was talking about the MAXSAT competition.
andrewprock 3y ago
Unless I'm missing something, space splitting should be trivial. If you have two cores and three propositional variables x1, x2, x3, you could simply set x1 to tier on one core and false on the other, and then perform two parallel SAT searches on a space with one less variable.
- bmc7505 3y ago
  Using a naive splitting strategy is trivial, but ensuring the distribution is well-balanced across the subspaces is not. You need to preprocess the formula by setting the variables, then doing some propagation, then restarting, otherwise one core will get stuck doing a bunch of useless work.
- c-cube 3y ago
  The difficulty is which variables to pick so that all subspaces are of comparable difficulty. Cube and conquer is a nice paper on that problem.
- thesz 3y ago
  What you describe looks like cube-and-conquer technique [1]. [1] https://www.cs.utexas.edu/~marijn/publications/cube.pdf https://www.cs.utexas.edu/~marijn/publications/cube.pdf The thing is much more deeper than what you described. You need to choose which variables you will assign, that's first. Then you have to assign them, and it is important to do as carefully because assignment may produce inbalanced search space. Splitting on one variable when there are hundredths of thousands of them is very, very inefficient.