Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: add GSAT implementation #7

Merged
merged 7 commits into from
Jan 8, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 2 additions & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,8 @@ sat-rs <CNF_FILE> <SOLVER>
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 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.
* `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

Expand Down
1 change: 1 addition & 0 deletions src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@
//! * [`crate::solvers::interactive`] - A purely syntactic solver based on user provided input.
//! * [`crate::solvers::chaos`] - A solver based on the CHAOS algorithm.
//! * [`crate::solvers::wsat`] - A solver based on the WSAT algorithm.
//! * [`crate::solvers::gsat`] - A solver based on the GSAT algorithm.
//!
//! This crate also contains some useful structs for working with propositional variables and formulas, viz:
//! * [`crate::notation::Formula`] - A struct for working with propositional formulas
Expand Down
2 changes: 2 additions & 0 deletions src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ mod solvers;
mod utils;

use solvers::chaos::chaos_algorithm;
use solvers::gsat::gsat_algorithm;
use solvers::interactive::interactive_algorithm;
use solvers::wsat::wsat_algorithm;
use utils::read_file;
Expand Down Expand Up @@ -51,6 +52,7 @@ fn main() {
"interactive" => interactive_algorithm(&mut formula.unwrap()),
"chaos" => chaos_algorithm(&mut formula.unwrap(), 100),
"wsat" => wsat_algorithm(&mut formula.unwrap(), 100, 100),
"gsat" => gsat_algorithm(&mut formula.unwrap(), 100, 100, None),
&_ => panic!("Unknown solver: {}", args.solver),
};

Expand Down
37 changes: 37 additions & 0 deletions src/notation.rs
Original file line number Diff line number Diff line change
Expand Up @@ -269,4 +269,41 @@ impl Formula {
}
return value;
}

/// Returns a vector of unsatisfied clauses
///
/// This is intended to be used after the formula has been evaluated
///
/// # Returns
/// * [`Vec<Clause>`] - A vector of unsatisfied clauses
pub fn get_unsatisfied_clauses(&mut self) -> Vec<Clause> {
let mut unsatisfied_clauses: Vec<Clause> = Vec::new();
for clause in &self.clauses {
if !clause.is_satisfied {
unsatisfied_clauses.push(clause.clone());
}
}
return unsatisfied_clauses;
}

/// Returns a vector of variables in a clause
///
/// # Arguments
/// * `clause` - A [`Clause`] struct
///
/// # Returns
/// * [`Vec<i32>`] - A vector of variables in the clause
pub fn get_clausal_variables(&mut self, clause: &Clause) -> Vec<i32> {
let mut clausal_variables: Vec<i32> = Vec::new();

for var in &self.vars {
for literal in &clause.literals {
if literal.value == *var {
clausal_variables.push(*var);
}
}
}

return clausal_variables;
}
}
163 changes: 163 additions & 0 deletions src/solvers/gsat.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,163 @@
use rand::seq::SliceRandom;

use crate::notation::{Clause, Formula};
use crate::solvers::utils::flip;
use std::collections::HashMap;

/// GSAT Algorithm for evaluation of propostional formulas
///
/// This algorithm generates random interpretations and checks if the formula is satisfied by the
/// interpretation. If the formula is satisfied, the algorithm returns true. If the formula is not
/// statisfied, the algorithm selects a variable which upon flipping satisfies the maximum number
/// of clauses. The algorithm then flips the value of the variable in the interpretation. The
/// algorithm then checks if the formula is satisfied by the new interpretation. If the formula is
/// satisfied, the algorithm returns true. If the formula is not satisfied, the algorithm repeats
/// the process until the formula is satisfied or the maximum number of flips is reached.
///
/// # Pseudocode
/// ```text
/// procedure GSAT(Set of Clauses S)
///
/// input: A set of clauses S
/// output: true if S is satisfiable, false otherwise
/// parameters: max_tries, max_flips
///
/// begin
/// repeat max_tries times
/// create a random interpretation I
/// if I satisfies S
/// then return true
/// else
/// repeat max_flips times
/// p := variable which upon flipping satisfies the maximum number of clauses
/// I = flip(I, p)
/// if I satisfies S
/// then return true
/// else
/// continue
/// end
/// ```
///
/// # Arguments
/// * `formula` - A [`Formula`] struct
/// * `max_tries` - The number of times to try to find a satisfying interpretation
/// * `max_flips` - The number of times to flip the value of a variable in an interpretation
///
/// # Returns
/// * `bool` - The value of the formula
///
/// # Examples
/// ```rust
/// use sat_rs::notation::{Literal, Clause, Formula};
/// use sat_rs::solvers::gsat;
///
/// let mut clause = Clause::new(); // Clause: p v q
/// let p = Literal{ value: 1, negated: false};
/// let q = Literal{ value: 2, negated: false};
/// clause.literals.push(p);
/// clause.literals.push(q);
///
/// let mut formula = Formula {
/// clauses: vec![clause],
/// literals: vec![Literal{ value: 1, negated: false}, Literal{ value: 2, negated: false}],
/// vars: vec![1, 2],
/// num_clauses: 1,
/// num_vars: 2,
/// };
///
/// let result = gsat::gsat_algorithm(&mut formula, 10, 10, None);
/// assert_eq!(result, true);
/// ```
pub fn gsat_algorithm(
formula: &mut Formula,
max_tries: u32,
max_flips: u32,
walk_probability: Option<f32>,
) -> bool {
let mut value: bool = false;

for _ in 0..max_tries {
// Create a random interpretation
let mut interpretation: HashMap<i32, bool> = HashMap::new();

for var in &formula.vars {
interpretation.insert(*var, rand::random::<bool>());
}

// Check if the interpretation satisfies the formula
if formula.evaluate(&interpretation) {
value = true;
println!(
"Formula is satisfied by the interpretation: {:?}",
interpretation
);
return value;
} else {
for _ in 0..max_flips {
// Collect unsatisfied clauses
let unsatisfied_clauses: Vec<Clause> = formula.get_unsatisfied_clauses();

// Loop over all the unsatisfied clauses, and find the variable
// which upon flipping satisfies the maximum number of clauses
let mut var_to_flip: i32 = 0;
for clause in &unsatisfied_clauses {
let mut max_satisfied_clauses: u32 = 0;
for literal in &clause.literals {
let mut interpretation_copy = interpretation.clone();
interpretation_copy = flip(&mut interpretation_copy, literal.value).clone();

let mut num_satisfied_clauses: u32 = 0;
// Clone the formual per iteration
let mut temp_formula = formula.clone();

for clause in &mut temp_formula.clauses {
clause.is_satisfied = clause.evaluate(&interpretation_copy);
if clause.is_satisfied {
num_satisfied_clauses += 1;
}
}

if num_satisfied_clauses > max_satisfied_clauses {
max_satisfied_clauses = num_satisfied_clauses;
var_to_flip = literal.value;
}
}
}

// Flip the value of the variable
if walk_probability == None {
interpretation = flip(&mut interpretation, var_to_flip).clone();
} else {
// flip the value of the variable with a probability walk_probability
// and flip a random variable with probability 1 - walk_probabilityN
let random_number: f32 = rand::random::<f32>();
if random_number < walk_probability.unwrap() {
interpretation = flip(&mut interpretation, var_to_flip).clone();
} else {
// Randomly select a clause that is not satisfied by the interpretation
let clause = unsatisfied_clauses.choose(&mut rand::thread_rng());
let clausal_variables: Vec<i32> =
formula.get_clausal_variables(&clause.unwrap());
let random_var =
clausal_variables[rand::random::<usize>() % clausal_variables.len()];
interpretation = flip(&mut interpretation, random_var).clone();
}
}

// Check if the interpretation satisfies the formula
if formula.evaluate(&interpretation) {
value = true;
println!(
"Formula is satisfied by the interpretation: {:?}",
interpretation
);
return value;
} else {
continue;
}
}
}
}

return value;
}
6 changes: 4 additions & 2 deletions src/solvers/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,11 @@
//! ## Available solvers
//!
//! * [`interactive`] - A purely syntactic solver based on user provided input.
//! * [`chaos`] - A solver based on the chaos algorithm.
//! * [`wsat`] - A solver based on the wsat algorithm.
//! * [`chaos`] - A solver based on the CHAOS algorithm.
//! * [`wsat`] - A solver based on the WSAT algorithm.
//! * [`gsat`] - A solver based on the GSAT algorithm.
pub mod chaos;
pub mod gsat;
pub mod interactive;
pub mod utils;
pub mod wsat;
22 changes: 3 additions & 19 deletions src/solvers/wsat.rs
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ use std::collections::HashMap;
/// assert_eq!(result, true);
/// ```
pub fn wsat_algorithm(formula: &mut Formula, max_tries: u32, max_flips: u32) -> bool {
let mut value: bool = true;
let mut value: bool = false;

for _ in 0..max_tries {
// Create a random interpretation
Expand All @@ -90,28 +90,12 @@ pub fn wsat_algorithm(formula: &mut Formula, max_tries: u32, max_flips: u32) ->
return value;
} else {
for _ in 0..max_flips {
// Collect unsatisfied clauses
let mut unsatisfied_clauses: Vec<Clause> = Vec::new();
for clause in &formula.clauses {
if !clause.is_satisfied {
unsatisfied_clauses.push(clause.clone());
}
}

// Randomly select a clause that is not satisfied by the interpretation
let unsatisfied_clauses: Vec<Clause> = formula.get_unsatisfied_clauses();
let clause = unsatisfied_clauses.choose(&mut rand::thread_rng());

// Randomly select a variable from the clause
let mut clausal_variables: Vec<i32> = Vec::new();

for var in &formula.vars {
for literal in &clause.unwrap().literals {
if literal.value == *var {
clausal_variables.push(*var);
}
}
}

let clausal_variables: Vec<i32> = formula.get_clausal_variables(&clause.unwrap());
let variable = clausal_variables[rand::random::<usize>() % clausal_variables.len()];

interpretation = flip(&mut interpretation, variable).clone();
Expand Down
2 changes: 1 addition & 1 deletion tests/chaos_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@ use sat_rs::cnfparser;
use sat_rs::solvers::chaos;

#[test]
fn test_parse_cnf() {
fn test_chaos() {
// Create a buffer of type &str using file at bin/unsatisfiable.cnf
let buffer = include_str!("../bin/unsatisfiable.cnf");

Expand Down
2 changes: 1 addition & 1 deletion tests/evaluate_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use std::collections::HashMap;
use sat_rs::cnfparser;

#[test]
fn test_parse_cnf() {
fn test_evaluate() {
// Create a buffer of type &str using file at bin/problem.cnf
let buffer = include_str!("../bin/problem.cnf");

Expand Down
19 changes: 19 additions & 0 deletions tests/gsat_test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
use sat_rs::cnfparser;
use sat_rs::solvers::gsat;

#[test]
fn test_gsat() {
// Create a buffer of type &str using file at bin/unsatisfiable.cnf
let buffer = include_str!("../bin/unsatisfiable.cnf");

// Parse the CNF file
let formula = cnfparser::parse_cnf(&buffer);

// Check that the formula is unsatisfiable
let result: bool = gsat::gsat_algorithm(&mut formula.clone().unwrap(), 10, 10, None);
let result_with_walk_probability: bool =
gsat::gsat_algorithm(&mut formula.clone().unwrap(), 10, 10, Some(0.5));

assert_eq!(result, false);
assert_eq!(result_with_walk_probability, false);
}
16 changes: 16 additions & 0 deletions tests/wsat_test.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
use sat_rs::cnfparser;
use sat_rs::solvers::wsat;

#[test]
fn test_wsat() {
// Create a buffer of type &str using file at bin/unsatisfiable.cnf
let buffer = include_str!("../bin/unsatisfiable.cnf");

// Parse the CNF file
let formula = cnfparser::parse_cnf(&buffer);

// Check that the formula is unsatisfiable
let result: bool = wsat::wsat_algorithm(&mut formula.unwrap(), 10, 10);

assert_eq!(result, false);
}