Artificial neural networks (ANN) have found extensive use in solving real-world problems in recent years, where their exceptional information processing is the main advantage. Facing increasingly complex problems, there is a need to improve their information processing. In this thesis, we explore new ways of synthesizing ANNs by reducing the synthesis problem to the Boolean satisfiability problem (SAT) that is, the problem of determining whether a given Boolean formula is satisfiable. Also known as the SAT problem, it aims to determine if there exists such a combination of Boolean variables in a propositional formula for which the formula evaluates to true. We derived a general formula in conjunctive normal form (CNF) representing the synthesis of a neural network. Given randomly generated datasets, we were able to construct CNF formulas whose satisfying assignments encode neural networks consistent with the datasets. These formulas were run through an off-the-shelf SAT solver, where the outputted models simulated the synthesis of neural networks consistent with the datasets. The experiments conducted in this thesis showed that our method had the ability to produce feed-forward neural networks of varying sizes consistent with randomly generated datasets of binary strings.