In this paper, we leverage the efficiency of Binarized Neural Networks (BNNs)to learn complex state transition models of planning domains with discretizedfactored state and action spaces. In order to directly exploit this transitionstructure for planning, we present two novel compilations of the learnedfactored planning problem with BNNs based on reductions to Weighted PartialMaximum Boolean Satisfiability (FD-SAT-Plan+) as well as Binary LinearProgramming (FD-BLP-Plan+). Theoretically, we show that our SAT-basedBi-Directional Neuron Activation Encoding is asymptotically the most compactencoding in the literature and maintains the generalized arc-consistencyproperty through unit propagation -- an important property that facilitatesefficiency in SAT solvers. Experimentally, we validate the computationalefficiency of our Bi-Directional Neuron Activation Encoding in comparison to anexisting neuron activation encoding and demonstrate the effectiveness oflearning complex transition models with BNNs. We test the runtime efficiency ofboth FD-SAT-Plan+ and FD-BLP-Plan+ on the learned factored planning problemshowing that FD-SAT-Plan+ scales better with increasing BNN size andcomplexity. Finally, we present a finite-time incremental constraint generationalgorithm based on generalized landmark constraints to improve the planningaccuracy of our encodings through simulated or real-world interaction.