Boolean satisfiability (SAT) is one of the most well-known NP-complete problems and has been extensively studied. State-of-the-art solvers exist and have found a wide range of applications. However, they still do not scale well to formulas with hundreds of variables for uniform 3-SAT problems. To tackle this fundamental scalability challenge, we introduce CNNSAT, a fast and accurate statistical decision procedure for SAT based on convolutional neural networks. CNNSAT's effectiveness is due to a precise and compact representation of Boolean formulas. On both real and synthetic formulas, CNNSAT is highly accurate and orders of magnitude faster than the state-of-the-art solver Z3. We also describe how to extend CNNSAT to predict satisfying assignments when it predicts a formula to be satisfiable.
[Second Update] I still find the method proposed in this paper appealing, and think that it may have practical applications in addition to providing significant research contributions. A key question that was raised by the other two reviewers was whether the proposed approach was fairly evaluated against existing state-of-the-art solvers. The authors have responded to these concerns by adding clarifications and new baselines to their paper. However, based on the discussions to date, I feel that I am not sufficiently familiar with related work on SAT solvers to say whether the other reviewers' concerns have been fully addressed. If they have been, I'd strongly lean towards accepting the paper. As for the concerns from my original review: the transferability experiments reported in the author comments below are quite informative, and I'd encourage the authors to incorporate them into the paper (or an appendix if space is an issue). I'd also encourage the author to incorporate the full comparisons against Z3, PicoSAT, MiniSAT, Glucose, Dimetheus, and CaDiCaL from Section 5.1. (I've updated my rating for the paper from 5 to 6, and my confidence score from 3 to 2.)
[First Update] Based on the feedback of the other two reviewers, I believe that I was missing some important context about SAT solvers when I wrote my initial review. Reviewer 1 and Reviewer 2 both raised serious concerns about the types of SAT instances that were used to evaluate the experimental setup, as well as about the use of Z3 as a baseline for solving random SAT instances. (No author response was provided.) Given this additional information, I've lowered my score for the paper from an 8 to a 5. I do think that the approach is interesting, but have reservations about the experimental evaluation and the claims made by the current submission. (Note: As the paper authors point out in the comment below, this update was mistakenly submitted a few days before the end of the rebuttal period.)
[Original Title] Interesting idea, impressive results for a first paper
[Summary] The authors propose a method of using convolutional neural networks to determine whether large boolean formulas (containing hundreds of variables and thousands of clauses) are satisfiable. The resulting models are accurate (correctly distinguishing between satisfiable and unsatisfiable formulas more between 90% and 99% of the time, depending on the dataset) while taking 10x - 100x less time than an off-the-shelf solver (Z3), offering slightly better quality on some problems and slightly worse quality on others. In addition to determining whether formulas are satisfiable, the authors propose and evaluate a method for finding satisfying assignments. They also evaluate their system on SMT benchmarks, where it also shows 10x-100x speed-ups, albeit with somewhat lower accuracy (e.g., 73% - 92% accuracy; I couldn't find baselines for these experiments).
[Key Comments] Unless I'm missing something major, I'd prefer to accept this paper, since the problem appears novel and the experimental results seem very promising for a first paper on a new problem.
[Pro 1] The paper seems polished and well-written. I generally found it well-motivated and easy to follow.
[Pro 2] To the best of my knowledge, the problem domain (machine learning for satisfiability problems that are so large that they are difficult to solve using conventional methods) is both novel and well-motivated.
[Pro 3] Algorithms seem conceptually straightforward (but might be a bit challenging to implement in practice due to the large input size), and yield excellent results. The magnitude of speed-ups reported in the paper (10x - 100x) is large enough to be exciting from a research perspective, and also seems like it should be large enough to have significant practical applications.
[Pro 4] Results are evaluated on a variety of different boolean satisfiability and SMT problems.
[Con 1] To improve reproducibility, it would be helpful if the authors could provide more details about their model training setup. Figure 2 is a good start, but adding details about the layer sizes, types of pooling layers used, and the model training setup would help clarify the experiments.
[Con 2] It seems like a significant number of labeled training examples (i.e., examples that are already known to be satisfiable or unsatisfiable) are needed in order to train a neural network. This seems like it could present a bootstrapping problem for certain domains: it may be computationally expensive to generate ground-truth labels for training examples, but a significant number of labels are needed to train a good prediction model. I'd be very interested to see a study of how well trained models transfer across domains: how well do models trained on one domain (e.g., a synthetic problem where labeled training data is cheap to generate) transfer to a different domain (e.g., a real-world problem where training labels are expensive to compute)? However, this is a minor point for a first paper on a new problem, and I think the paper is interesting enough to merit acceptance without such an analysis.