3 ms·

It's not difficult to reduce scheduling problems that are usually done with dynamic programming etc. to SAT. Then there's SATPLAN. If I had VC money I would be

It's not difficult to reduce scheduling problems that are usually done with dynamic programming etc. to SAT. Then there's SATPLAN. If I had VC money I would be seeking young'uns trying to change the world with SATPLAN, of course in a way that's married to machine learning. (Machine learning doesn't "think", it "learns"; logic-based AI "thinks" but can't "learn"). E: part 1 says at the outset: > As an example, the often-talked-about dependency management problem, is also NP-Complete and thus translates into SAT[2][3], and SAT could be translated into dependency manager. The problem our group worked on, generating key and lock cuttings based on user-provided lock-chart and manufacturer-specified geometry, is also NP-complete.< Part 3 is already deep in the rabbit hole of comparing heuristics. People like me just write something that "compiles" to DIMACS and fires Minisat.

6gvONxR4sf7o 7y ago
A primary problem in marrying logic to ML is doing so in a differentiable way. i.e. when your SAT part of the system is suboptimal, how do you know which parameters of the learned part to change, and in which direction?
- nl 7y ago
  We propose Differentiable Satisfiability and Differentiable Answer Set Programming (Differentiable SAT/ASP) for multi-model optimization. Models (answer sets or satisfying truth assignments) are sampled using a novel SAT/ASP solving approach which uses a gradient descent-based branching mechanism. https://arxiv.org/abs/1812.11948 https://arxiv.org/abs/1812.11948
- smallnamespace 7y ago
  From the article, a lot of the heuristics seems to revolve around and 1) which variables to try first 2) which learned clauses to keep in your set. Assign scores and differentiate on those scores. This is (very loosely) how AlphaGo also works - you take a tree-based algorithm (MCTS) and then use neural nets to score the next node to expand.
- mlevental 7y ago
  you don't need differentiability you just need a learning rule. there are learning algorithms that don't use gradient ascent.

6gvONxR4sf7o 7y ago

A primary problem in marrying logic to ML is doing so in a differentiable way. i.e. when your SAT part of the system is suboptimal, how do you know which parameters of the learned part to change, and in which direction?

nl 7y ago
We propose Differentiable Satisfiability and Differentiable Answer Set Programming (Differentiable SAT/ASP) for multi-model optimization. Models (answer sets or satisfying truth assignments) are sampled using a novel SAT/ASP solving approach which uses a gradient descent-based branching mechanism. https://arxiv.org/abs/1812.11948 https://arxiv.org/abs/1812.11948
smallnamespace 7y ago
From the article, a lot of the heuristics seems to revolve around and 1) which variables to try first 2) which learned clauses to keep in your set. Assign scores and differentiate on those scores. This is (very loosely) how AlphaGo also works - you take a tree-based algorithm (MCTS) and then use neural nets to score the next node to expand.
mlevental 7y ago
you don't need differentiability you just need a learning rule. there are learning algorithms that don't use gradient ascent.