microsat 0.0.1

A simple DPLL SAT solver
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128

use hashbrown::HashMap;

#[derive(Debug, Eq, PartialEq, Clone, Copy)]
pub enum Action {
    RemoveClause(ClauseId),
    RemoveLiteralFromClausesStart(),
    RemoveLiteralFromClause(ClauseId),
    RemoveLiteralFromClausesEnd(Literal),
    AssignVariable(Variable),
}

pub type Assignment = HashMap<Variable, bool>;
pub type ClauseId = u16;
pub type Literal = i16;
pub type Variable = u16;
pub type ActionState = usize;

#[derive(Debug, Default, Eq, PartialEq, Clone)]
pub struct Clause {
    variables: Vec<Literal>,
}

pub trait CNF {
    /// Adds a new clause to the CNF representation.
    fn add_clause(&mut self, clause: Clause);

    /// Removes a unit clause (if it exists) from the CNF and returns it.
    fn remove_unit_clause(&mut self) -> Option<ClauseId>;

    /// Removes a pure literal (if it exists) from the CNF and returns it.
    fn remove_pure_literal(&mut self) -> Option<Literal>;

    /// Constructs an assignment from the current state of the CNF.
    /// This is only valid if the CNF is satisfiable.
    fn construct_assignment(&mut self) -> Assignment;

    /// Returns true if the CNF is satisfiable.
    fn is_satisfied(&self) -> bool;

    fn is_unsatisfiable(&self) -> bool;

    fn get_action_state(&self) -> ActionState;

    fn restore_action_state(&mut self, state: ActionState);

    fn is_inference_possible(&self) -> bool;

    fn get_branch_variable(&self) -> (Variable, bool);

    fn branch_variable(&mut self, variable: Variable, value: bool);
}

impl Clause {
    pub fn new() -> Clause {
        Clause {
            variables: Vec::new(),
        }
    }

    #[inline]
    pub fn insert_checked(&mut self, variable: Literal) {
        if !self.variables.contains(&variable) {
            self.variables.push(variable);
        }
    }

    #[inline]
    pub fn insert(&mut self, variable: Literal) {
        self.variables.push(variable);
    }

    #[inline]
    pub fn len(&self) -> usize {
        self.variables.len()
    }

    #[inline]
    pub fn is_empty(&self) -> bool {
        self.variables.is_empty()
    }

    #[inline]
    pub fn contains(&self, variable: Literal) -> bool {
        self.variables.contains(&variable)
    }

    #[inline]
    pub fn literals(&self) -> &Vec<Literal> {
        &self.variables
    }

    #[inline]
    pub fn get(&self, index: usize) -> Literal {
        unsafe {
            return *self.variables.get_unchecked(index);
        }
    }

    /// Efficient remove for a clause set that uses constant time by swapping
    /// the last element with the removed one.
    pub fn remove(&mut self, variable: Literal) {
        for i in 0..self.variables.len() {
            if self.variables[i] == variable {
                self.variables.swap_remove(i);
                return;
            }
        }
    }
}

#[inline]
pub fn to_variable(literal: Literal) -> Variable {
    literal.unsigned_abs()
}

#[inline]
pub fn negate(variable: Literal) -> Literal {
    -variable
}

#[inline]
pub fn to_positive(variable: Literal) -> Literal {
    if variable > 0 {
        variable
    } else {
        -variable
    }
}