Re:Modern SAT solvers: fast, neat and underused
by 6gvONxR4sf7o on Sunday May 19, 2019 @02:55PM
(#19954800)
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?
[ Parent
| on HN ]
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.
Re:Modern SAT solvers: fast, neat and underused
by smallnamespace on Monday May 20, 2019 @12:27AM
(#19957515)
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.