SAT Solvers in Rust

This crate contains implementations of various satisfiability solvers for the boolean satisfiability problem (SAT).

Usage

The crate can be used as a library or as a binary. To use it as a binary, run the following command:

cargo run <CNF_FILE> <SOLVER>

OR

sat-rs <CNF_FILE> <SOLVER>

Algorithms

Available implementations:

• CHOAS: A purely random algorithm (appropriately named) which generates random interpretations and checks if the formula evaluates to true.
• WSAT: A pseudo-random algorithm which generates random interpretations and if the formula evaluates to false, flips a random variable from some unsatisfied clause and repeats this process until it finds a satisfying implementation.
• GSAT: A pseudo-random algorithm which generates random interpretations and if the formula evaluates to false, flips a variable which satisfies the maximum number of unsatisfied clauses and repeats this process until it finds a satisfying implementation.

References

• Initial work on the crate was based on the COMP21111: Logic and Modelling course taught by Konstantin Korovin.