SATNet: Bridging deep learning and logical reasoning with differentiable SAT | Hacker News Reader

SATNet: Bridging deep learning and logical reasoning with differentiable SAT

arxiv.org

116 pointspizza17 comments

there's also this https://arxiv.org/abs/1812.11948

and there's also this: https://github.com/MatthiasNickles/delSAT

Can someone comment on the deeper distinctions between this and DeepMinds ILP paper on learning explanatory rules from noisy data? AFAIK thats a special case of SAT?

ILP and SAT are quite different. ILP is much higher level in that it can define new predicates and do recursion, which have no counterparts in SAT. On the other hand, SAT is much more scalable and can be applied to instances orders of magnitude larger. I think ILP's expressiveness and lack of scalability are related.

To clarify - ILP meaning Inductive Logic Programming vs Integer Linear Programming?

Inductive Logic Programming. DeepMind work in question is https://arxiv.org/abs/1711.04574.

ILP usually translates to SAT. You can see ILP as a high-level interface to SAT.

I think you mean ILP as in Integer Linear Progamming. The quote above mentioned δILP which is "differentiable Inductive Logic Programming".

No.

I meant was ASP is a higher level 'interface' to SAT, sorry for the confusion. Work done at Imperial by Law and Evans in ILP compiles down to SAT solving via ASP. IDK if δILP goes to SAT.

To complement this.

Inductive Logic Progamming (ILP) is a class of machine learning algorithms that learn logic programs from examples and background knowledge (where background knowledge is a logic theory, i.e. another logic program, as ar the examples).

SAT is the boolean satisfiability problem, the problem of finding variable assignments to the variables of a boolean formula that make the formula true.

So the two are not similar and one is not an instance of the other.

The δILP paper describes a differentiable ILP system that learns logic programs with a differentiable logic representation.

Finally, the paper above (SATNet) describes a differentiable satisfiabiilty solver that can be incorporated in a neural network architecture to enable the nerual net to solve satisfiability problems and perform reasoning.

Looks like they (SATNet) are not incorporating a real (exact) SAT solver but their differentiable "SAT solver" is a MAXSAT estimator which gives an approximation of the maximum number of clauses that can be made true.

Thanks. I should read this more carefully - I just skimmed it, to be honest.

This seems like a promising direction.

code: https://github.com/locuslab/satnet

Great, hopefully this'll get us past the halting problem.

The halting problem is formally proven to be undecidable.

In some senses we are past the halting problem once we accept that that we will sometimes be wrong or unable to answer. Insofar as it has anything to do with the halting problem, this seems just another way to do that. Might still be useful.

Reply on news.ycombinator.com