use super::GroverSat;
use crate::{Result, Samples};
use burn::tensor::Device;
use rand::{Rng, SeedableRng};
use rand_chacha::ChaCha8Rng;
use serde::{Deserialize, Serialize};
#[derive(Clone, Copy, Debug, Serialize, Deserialize)]
pub struct SearchConfig {
pub max_trials: usize,
pub max_oracle_calls: usize,
pub seed: u64,
}
impl Default for SearchConfig {
fn default() -> Self {
Self {
max_trials: 64,
max_oracle_calls: 4096,
seed: 0,
}
}
}
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
#[serde(tag = "status", rename_all = "snake_case")]
pub enum SatOutcome {
Satisfiable {
assignment: Vec<bool>,
},
Unsatisfiable,
Inconclusive,
}
#[derive(Clone, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub struct SearchReport {
#[serde(flatten)]
pub outcome: SatOutcome,
pub trials: usize,
pub oracle_calls: usize,
pub seed: u64,
}
impl GroverSat {
pub fn search(&self, config: SearchConfig, device: &Device) -> Result<SearchReport> {
let mut report = SearchReport {
outcome: SatOutcome::Inconclusive,
trials: 0,
oracle_calls: 0,
seed: config.seed,
};
if self.formula().clauses().iter().any(Vec::is_empty) {
report.outcome = SatOutcome::Unsatisfiable;
return Ok(report);
}
if self.formula().clauses().is_empty() {
report.outcome = SatOutcome::Satisfiable {
assignment: vec![false; self.formula().num_variables()],
};
return Ok(report);
}
if config.max_trials == 0 {
return Ok(report);
}
let uniform = self.initial_state(device)?;
let mut rng = ChaCha8Rng::seed_from_u64(config.seed);
let mut window = 1.0f64;
let cap = (2.0f64).powf(self.formula().num_variables() as f64 / 2.0);
for _ in 0..config.max_trials {
let iterations = rng.random_range(0..window.ceil() as usize);
if iterations > config.max_oracle_calls - report.oracle_calls {
break;
}
let state = self.iterate(uniform.clone(), iterations)?;
report.oracle_calls += iterations;
let samples = Samples::from_state(&state, 1, rng.random(), 1)?;
report.trials += 1;
let digits = state.register().decode(samples.outcomes[0][0])?;
let assignment: Vec<bool> = digits[..self.formula().num_variables()]
.iter()
.map(|&x| x == 1)
.collect();
if self.formula().evaluate(&assignment)? {
report.outcome = SatOutcome::Satisfiable { assignment };
return Ok(report);
}
window = (window * 1.2).min(cap);
}
Ok(report)
}
}