Improving SAT-Solvers with a Genetic Algorithm and Deep Reinforcement Learning

Introduction

This project is an attempt to use deep reinforcement learning together with a genetic algorihm to improve state of the art solvers for the boolean satisfiability problem. The code is based on the source code of "Learning to Evolve, Jan Schuchardt, Vladimir Golkov, Daniel Cremers [2019]" and the previous work from Yoav Schneider. The current project now contains both the code that was used for a previous approach and the first modules for the new approach. The old one differs heavily from the new one as you can see on the latest presentations slides from 2020. The old approach focused on using simple genetic algorithms to modify the current solution for a problem. One can think of it as a WalkSAT approach. This strategy, however, has major drawbacks as discussed in the presentation slides and is therefore not really relevant anymore. Nevertheless, the code may still serve as a reference for future development and thus is still included in the code base.

Folder structure

Overview

• DATA/: Folder containing various satisfiable SAT problems encoded in DIMACS cnf format. The existing problems are taken from here, but one can also easily create new problem instances using src/utils/SAT_problem_generator.py. Note that these problem will be randomly generated and thus are not as hard to solve as the already existing ones.
• DOCS/: Here you can find all sorts of additional information for the project like presentation slides or blueprints of the NN architecture.
• solution/: All solutions and byproducts (e.g. weights, stats,...) generated by a solver will be stored here.
• src/: Folder containing all the relevant source code.

Source Code:

• /neural_networks/ Here you can find many network architectures as well as helpful submodules.

  • encode_process_decode.py: The combined actor-critic network for the new message passing approach. It is not yet used by any solver. See comments or https://arxiv.org/abs/1806.01261 for more information
  • feature_collection.py: A helper class that wrapps together different sized tensors and symplifies the handling.
  • message_passing_core.py: A submodule that implements the MP layer, aka message passing on a graph network.
  • network.py: the network from the "Learning to Evolve" paper
  • pool_conv_sum_nonlin_pool.py: A submodule implementing a memory efficient + permutation equivariant convolution layer
  • static_dynamic_network.py: an improved version for the WalkSAT approach that tries to infer deep problem features while also deciding for an action each time step.
  • utils.py: Collection of various utility functions

• /reinforcement.py/ Code for reinforcement learning. Taken from Jan Schuchardt's code based and left unchanged, except for allowing irregular sized training data batches and an additional progressbar for the optimization process.

• /sat/ Code for representing and validating SAT problems. Note that it may need future adaption to work with the new solver type.

  • cnf3.py: Code for reading CNF3 problems and evaluating them.
  • population.py: Code for representing and modifying a population of CNF3 solutions.
  • problem loader.py: Loads SAT3 problems from text files.
  • solution: Represent a single CNF3 solution.

• /solvers/ Code for encoding populations and problems for neural networks and running the genetic algorithm. Implementation of new classes based on Jan Schuchardt's code base.

  • encoding.py: This class encodes the current state and all relevant input features to be then fed to the neural network.
  • solvers.py: Test file implementing different WalkSAT solvers that all rely on genetic strategies. Note that for the new approach one has to implement a completly new solver.

• /strategies/ Implementation for different genetic algorithms strategies that are used by WalkSAT solvers.

• /utils/ Folder containing additional utility functions and test implementations for neural networks.

  • memory.py: Class comparing different custom RNN implementations. Not relevant for the code base.
  • NeuroSAT.py: A simplified version of the NeuroSAT architecture https://arxiv.org/abs/1802.03685. Not relevant for the code base.
  • plot_fitness_factors.py, plot_mutation_rates.py: Legacy code by Yoav Schneider. Not relevant for the code base.
  • SAT_problem_generator.py: Class to create new random SAT problem instances with arbitrary number of variables / clauses
  • solve.py: Implementation for the training and validation process

• train.py: File to start training

• validate.py: File to start validation

How to Use

As mentioned in the introduction, the new approach presented in the slides is not fully implemented yet. That means, there is no entry file that you can call to solve SAT problems end to end with the new approach. However, you can run the old WalkSAT approach to get an idea what the final outcome should look like. The following paragraphs describe how to train and validate the old WalkSAT approach.

Be sure to install all the necessary requirements!

pip install -r requirements.txt

Five different solvers are available:

• Individual Mutation
• Gene Mutation
• Crossover
• Selection
• Vanilla

They can be trained using train.py with the following syntax

python3 train.py [solver] [output directory] [weights directory]? [start index]? 

• solver: Use either gene/individual/crossover/selection to call one of the above mentioned solvers
• output directory: folder you want store the statistics in. Folder must already exist!
• weights directory: (Optional) Path to the baseline file that can be used to initialize the the network with previously trained weights.
• start index: (Optional) Integer that specifies to start at a specific round of training. Default is 0.

They can be validated using validation.py with the following syntax (network weights are expected in the output dir as "baseline")

python3 validate.py [solver] [output directory] [weights directory]? [start index]? 

• solver: Use either gene/individual/crossover/selection/vanilla to use The validation outputs the average maximum fitness at each generation to a text files at the output direction.
• output directory: folder you want store the statistics in. Folder must already exist!
• weights directory: (Optional) Path to the baseline file that can be used to initialize the the network with previously trained weights.
• start index: (Optional) Integer that specifies to start at a specific round of training. Default is 0.

Note for the implementation:

When you check the code in /neural_networks/ you will find that instead of a single input tensor we often use a so called Feature_Collection. This is a wrapper class to manage multiple different sized tensors. The need for such a class originated in the implementation process of a the memory efficient conv layer (pool_conv_sum_nonlin_pool.py). Instead of concatenating all input features with broadcasting and then use convolution, we only concatenate feature streams of the same dimensionality. Then we appy convolution to each input stream seperately. Only after this we sum them together with broadcasting. This is a more efficent way of extracting features than having a single big tensor. To simplify the handling with these multiple features we introduce a new system, which will be discribed in the following.

Let an input_stream be the Tensor itself. A Feature_Collection manages a dictionary mapping so called input_codes to their respective input_stream. Let us imagine the following scenario: For our input we need a population dimension P, an equation dim E and a genome dim G. That means that if we were to combine our features along the channels dimension in a single tensor, it would be of size BxCxPxExG, where B and C are the Batch and the Channels dimension, respectively. But now consider that we have 3 input streams:

• stream_1: 2xPxG
• stream_2: 5xP
• stream_3: 1xExG

where the letters behind each name stand for their respective size. Let's normalize them to the above mentioned form of BxCxPxExG:

• stream_1: 1x2xPx1xG
• stream_2: 1x5xPx1x1
• stream_3: 1x1x1xExG

(Note that we could now easily concatenate them together to a 1x8xPxExG tensor.) We now can assign to each stream a unique code that is derived from its size:

• stream_1: (1,0,1)
• stream_2: (1,0,0)
• stream_3: (0,1,1)

Leaving out the Batch and Channels dimension, there is a 1 for each dimension that is bigger than 1 and a 0 otherwise. So from looking at (0,1,1) we know it does not have the P dim, but does have the E and G dim. If we have another feature of the same size we can add it to our Feature_Collection and it will automatically be concatenated with the existing stream of this size. The encoding scheme can be set in src/solvers/encoding.py.

Future Work

See future work section of the slides for the discussion and theoretical background. Here is a list of things that have to be implemented while working towards the new approach:

• Implement CDCL sat solver such as MiniSAT
• Create a new evolution strategy that creates new individuals given the network output
• Adapt the algorithm to allow queries to the NN to guide the algorithm
• Train and tune hyperparamters
• Optimize code for runtime