Learning Ordered Binary Decision Diagrams (OBDDs) from large-scale datasets is an important topic of explainable artificial intelligence. However, existing search-based methods are still limited in scalability regarding dataset size, since they must explicitly encode the satisfaction of all examples in a dataset. To tackle this challenge, we introduce an OBDD encoding method to parameterize a neural network. This method frees satisfaction encoding of all examples in a dataset while leveraging mini-batch training techniques to enhance learning efficiency. Our main theoretical contribution is to prove that our approach enables the simulation of OBDD inference within a continuous space. Besides, we identify faithful OBDD encoding to fulfill the properties required by OBDDs, allowing to interpret an OBDD directly from the learned parameter assignment. With faithful OBDD encoding, we present an end-to-end neural model named ØBDDNet, being capable of coping with large-scale datasets. Experimental results exhibit better scalability and competitive prediction performance of ØBDDNet compared to state-of-the-art OBDD learners. Valuable insights about faithful OBDD encoding are derived from the ablation study. The implementation is available at: https://github.com/jmq-design/OBDD-NET.

Linear temporal logic (LTL) satisfiability checking has a high complexity, i.e., PSPACE-complete. Recently, neural networks have been shown to be promising in approximately checking LTL satisfiability in polynomial time. However, there is still a lack of neural network-based approach to the problem of checking LTL satisfiability and generating traces as evidence, simply called SAT-and-GET, where a satisfiable trace is generated as evidence if the given LTL formula is detected to be satisfiable. In this paper, we tackle SAT-and-GET via bridging LTL trace checking to neural network inference. Our key theoretical contribution is to show that a well-designed neural inference process, named after neural trace checking, is able to simulate LTL trace checking. We present a neural network-based approach VSCNet. Relying on the differentiable neural trace checking, VSCNet is able to learn both to check satisfiability and to generate traces via gradient descent. Experimental results confirm the effectiveness of VSCNet, showing that it significantly outperforms the state-of-the-art (SOTA) neural network-based approaches for trace generation, on average achieving up to 41.68% improvement in semantic accuracy. Besides, compared with the SOTA logic-based approach nuXmv and Aalta, VSCNet achieves averagely 186X and 3541X speedups on large-scale datasets, respectively.