Learning Better Representations From Less Data For Propositional Satisfiability

Summary

The paper presents NeuRes, a neural symbolic system designed to solve the Boolean satisfiability problem of CNF (Conjunctive Normal Form). NeuRes utilizes a message-passing graph neural network to embed the information contained in CNF and attempts to predict clause pairs for propositional resolution and value assignments for satisfiability. NeuRes proposes three novel attention mechanisms to better select clause pairs for resolution and employs expert iteration to progressively optimize the generated proofs. The experimental results demonstrate the effectiveness of the proposed NeuRes system.

Strengths

- The approach proposed in the paper is novel, featuring a parallel mechanism for concurrently proving unsatisfiability and attempting to find a truth value assignment. This mechanism is expected to speed up the proving process significantly. - The three proposed attention variants each have distinct characteristics and are suitable for different situations. The expert iteration process effectively shortens the proof length. - The paper is well-written and easy to follow.

Weaknesses

- The paper does not include a thorough ablation study to evaluate the effectiveness of each proposed component. i.e. It lacks an assessment of the true value assignment task’s effectiveness. - As noted in the Limitation (Section 9), the efficiency of the neural method is concerning. It adds substantial computational overhead for clause selection using the neural network. However, overall, I believe this work represents a solid advancement in neuro-symbolic approaches for SAT solvers.

Questions

- Is there a comparison of the efficiency of the three different attention mechanisms as well as the baseline method (NeuroSAT)? It appears that full attention produces the most promising results, but it is also the least efficient.

Rating

6

Confidence

2

Soundness

3

Presentation

3

Contribution

3

Limitations

Yes, the authors adequately addressed the limitations and posed no negative societal impact.

Summary

The paper integrates attention-based neural networks into the SAT solving process based on resolution. The neural networks aim to predict pairs of disjunctive clauses to merge. The paper proposes several variants of neural networks for this task and conducted experiments to check their performance. Although the resolution is the algorithm to check unsatisfiability, the proposed framework simultaneously addresses the satisfiability task by decoding the embeddings of formulas.

Strengths

+ The address problem, the unsatisfiability of propositional formulas, is a fundamental, important problem in computer science. + Unifying resolution, a classic SAT solving algorithm, and attention-based neural networks. + The paper considers extensive variants of the neural models and checks their experimental performance. + It is experimentally demonstrated that the proposed approach outperforms the previous work, NeuroSat, and the expert iteration can shorten generated unsatisfiability proofs.

Weaknesses

- It is not clear how big the gap between the proposed approach and the highly-engineered SAT solvers is. It is not critical that the highly-engineered SAT solvers work better, but revealing the gap in the current state clarifies the current position of neural SAT solvers. - Some aspects of the proposed approach and experiment design are unclear (see the below question).

Questions

* How big is the gap between the proposed approach and the highly-engineered SAT solvers? * What is $\overline{E^L}$? How different is it from $E^L$? * The advantage of Casc-Attn is claimed to be "it ... can be used to select a tuple of arbitrary length." Does this advantage is utilized in the implementation? * The paper says that at train time only the positive literal embeddings are used to derive truth assignments, but at test time, the negative literal embeddings are used. Why is this okay although the derivation of truth assignments from the negative embeddings should not be learned? * What is the ratio between sat and unsat problems in the synthesized dataset? * At the beginning of Section 6, the paper mentions the training and test datasets, but does not the validation dataset. I think it should be used because hyperparameters should be adjusted. What validation dataset is used? * (Minor) What is Res-Aided model (mentioned at the beginning of Section 8)? I find this terminology only there.

Rating

7

Confidence

3

Soundness

3

Presentation

3

Contribution

3

Limitations

I think the limitations are discussed appropriately.

Summary

The paper presents NeuRes, a system to solve SAT/UNSAT problems. In particular, it is able to provide UNSAT certificates via resolution proofs. The system constructs a resolution proof by iteratively selecting two clauses from all clauses, producing the resolvent from the two clauses, and adding it back to the clause formula. The selection of two clauses is done by a selector network. They experiment with different attention mechanisms in the selector network, including full attention, selecting an anchor variable and then doing full attention on the subset of clauses including the anchor variable, etc. When training, they use an off-the-shelf symbolic solver to generate resolution proofs and train to predict the clause selection with a teacher forcing style. The experiments show that NeuRes is able to generate resolution proofs for UNSAT problems (99.6% problems solved) for small problems with 40 variables, and also shows some generalizability to larger problems.

Strengths

* The method is able to generate resolution proofs for UNSAT problems, which is a certificate for UNSAT problems, unlike previous methods such as NeuroSAT. * The method shows some generalizability to larger problems, which is a good sign for the method to be applied to larger problems. * The method is sometimes able to generate shorter resolution proofs than the teacher, and they propose a bootstrapping method to further improve the performance based on those shorter proofs.

Weaknesses

* Resolution-based UNSAT certification may not be as useful or practical as clausal proofs like the DRAT format, due to resolution-based proofs potentially being too large for large SAT instances.

Questions

* Could you explain how the method applies to SAT problems? If it's an UNSAT problem, then I can see that it terminates at deriving an empty clause, but how does it work for SAT problems? * How does the model size of NeuRes compare to the baseline NeuroSAT on the SAT problems? How does the solving time compare between the two methods?

Rating

6

Confidence

2

Soundness

3

Presentation

3

Contribution

3

Limitations

The limitation about the performance of neural methods on SAT solving still lags behind symbolic solvers is discussed.

Summary

The authors proposed an attention-based architecture that autoregressively selects pairs of clauses for propositional resolution. The framework can generate proofs of unsatisfiability and accelerate the process of finding satisfying truth assignments simutaneously. Emprical evaluation shows that the resulting model achieves better performance than NeuroSAT in terms of both correctly classified and proven instances.

Strengths

+ The model learns to pick resolution pairs rather than naively predicts binary satisfiability, resulting in an overall elegant approach that combines classic symbolic reasoning and machine learning. An unsat "prediction" always comes with a valid proof, and a sat prediction is alway correct. + Detailed attention mechanisms are presented in a progressive manner. Each attention mechanism is accompanied by proper motivation and explanation. The approach is clearly well thought-out and optimized carefully. Again, not applying pretrained language models blatantly stands out in the flooded submissions today. + I like the idea of predicting additionally the truth assignment. Although in principle the assignment can be read off once the resolution is complete, it's always better to terminate early. And by learning to pick the resolution pairs and assigning truth values simultaneously, more semantics can hopefully be injected into the models. Well done!

Weaknesses

- Speed can potentially be an issue since every resolution step invokes a forward pass of the model, and for large problems, the calls can be quite numerous.

Questions

- How easy do you think the approach can be combined with traditional SAT optimization? - Have you thought about extending the approach to anything beyond propositional SAT?

Rating

8

Confidence

4

Soundness

3

Presentation

4

Contribution

3

Limitations

The authors discussed the limitation in section 9 and I agree with them.

Summary

This paper presents a deep-learning-based approach for generating resolution proofs for SAT formulas. The proposed method outperforms NeuroSAT on proving/predicting satisfiability on a family of benchmarks.

Strengths

- Instead of directly learning to predict satisfiability, this paper proposes to learn the strategy to apply the resolution rule. I like this general approach, as it can provide actual proofs of both satisfiability and unsatisfiability. - Breaking down the resolution strategy prediction task to two steps (i.e., choosing a variable and then choosing two clauses) is a nice optimization that reduces the computational cost. - The approaches are explained clearly and the paper is relatively self-contained.

Weaknesses

- At its core, the key technical contribution of the paper is that instead of learning an end-to-end SAT solver, the paper proposes to learn a resolution strategy that selects the clauses to resolve for a given formula. This is a fine idea and similar in spirit to many existing lines of work in ML applied to constraint solving, where the goal is to learn a particular heuristics (e.g., branching, restart) to replace some hand-crafted ones. However, to evaluate the proposed method, the paper should compare with existing resolution strategies (potentially including learning-based ones if they exist already) on statistics such as proof lengths and runtime. The comparison with NeuroSAT to me is quite apple-to-orange. - Related to the point above, the paper is entitled "learning better representations from less data", instead of something along the line of "learning to perform resolution". The current title can be a little misleading because words like "better" and "less" do not make much sense when the underlying learning task changes (from satisfiability prediction to resolution clause selection). - The paper only considers very simple SAT instances and it seems difficult to scale the presented approach to much larger real-world instances.

Questions

1. Could you compare the learned resolution strategy with existing ones? 2. Have you conducted ablation studies of the effect of the model architecture to proof length/success rate?

Rating

4

Confidence

4

Soundness

3

Presentation

1

Contribution

3

Limitations

The paper discusses the scalability/efficiency limitation of the proposed method. I do not see the potential negative societal impact of their work.