stalmarck_sat/solver/
variable_frequency.rs

1use crate::core::formula::TripletVar;
2use std::collections::HashMap;
3
4#[derive(Debug, Default)]
5pub struct VariableFrequency {
6    /// Count of how many triplets each variable appears in
7    frequency_map: HashMap<i32, usize>,
8
9    /// Sorted list of variables by frequency
10    sorted_variables: Vec<(i32, usize)>,
11}
12
13impl VariableFrequency {
14    pub fn new() -> Self {
15        Self::default()
16    }
17
18    /// Analyze triplets and build frequency map
19    pub fn analyze_triplets(&mut self, triplets: &[(TripletVar, TripletVar, TripletVar)]) {
20        self.frequency_map.clear();
21
22        for (a, b, c) in triplets {
23            for triplet_var in [a, b, c] {
24                if let TripletVar::Var(id) = triplet_var {
25                    *self.frequency_map.entry(*id).or_insert(0) += 1;
26                }
27            }
28        }
29
30        // Sort variables by frequency (descending)
31        self.sorted_variables = self
32            .frequency_map
33            .iter()
34            .map(|(&var, &freq)| (var, freq))
35            .collect();
36        self.sorted_variables.sort_by(|a, b| b.1.cmp(&a.1));
37    }
38
39    /// Get the most frequent unassigned variable
40    pub fn get_most_frequent_unassigned(
41        &self,
42        assignments: &HashMap<i32, bool>,
43        original_vars_only: bool,
44        max_original_var: i32,
45    ) -> Option<i32> {
46        for &(var_id, _freq) in &self.sorted_variables {
47            if !assignments.contains_key(&var_id) {
48                // If we want original variables only, filter by range
49                if original_vars_only && var_id > max_original_var {
50                    continue;
51                }
52                return Some(var_id);
53            }
54        }
55        None
56    }
57
58    /// Get the frequency score for a triplet
59    pub fn get_triplet_frequency(&self, triplet: &(TripletVar, TripletVar, TripletVar)) -> usize {
60        let (a, b, c) = triplet;
61        let mut score = 0;
62
63        for triplet_var in [a, b, c] {
64            if let TripletVar::Var(id) = triplet_var {
65                score += self.frequency_map.get(id).unwrap_or(&0);
66            }
67        }
68        score
69    }
70
71    /// Get the potential deduction score for a triplet
72    pub fn get_potential_deduction_score(
73        &self,
74        triplet: &(TripletVar, TripletVar, TripletVar),
75    ) -> usize {
76        let (a, b, c) = triplet;
77        let base_frequency_score = self.get_triplet_frequency(triplet);
78
79        // Score based on how many variables can be deduced from the triplet's structure
80        let mut potential_deductions = 0;
81        if a == b {
82            // Rule (x, x, z) => x=1, z=1 (deduces 2 vars)
83            potential_deductions = 2;
84        } else if b == c {
85            // Rule (x, y, y) => x=1 (deduces 1 var)
86            potential_deductions = 1;
87        }
88
89        // The final score is a combination of potential deductions and frequency
90        (1 + potential_deductions) * base_frequency_score
91    }
92}
stalmarck_sat/solver/variable_frequency.rs

stalmarck_sat/solver/
variable_frequency.rs
