otter_sat 0.1.0

A library for determining the satisfiability of boolean formulas written in conjunctive normal form, developed to support investigation into solvers by researchers, developers, or anyone curious.
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
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143

/*!
A structure to record which clauses are watching an atom.

# Theory

A core part of a solve is [Boolean Constraint Propagation](crate::procedures::bcp) (BCP).
In short, BCP is the observation that some literal in a clause must be true due to all other literals in the clause being false.

For example, given the clause p ∨ -q ∨ r and a valuation v such that p is false and q is true, the clause is true on the valution *only if* r is (made) true --- in other contexts, given the valuation and clause specified it is said the clause 'asserts' r.

Note, BCP only applies when:
- There is exactly one literal without a value.
- All other literals conflict with the background valuation.

This motivates the use of two watches:
- One watch on a literal without a value, to note the clause is a candidate for BCP to be applied at some point.
- One watch on any other literal which does not conflict with the background valuation, if possible.
  + For, if it is *only* possible to watch some other literal which conflicts with the current valuation, the other literal must be true.

The watch database records which clauses are watching an atoms, and for the implementation of watching literals see the way clauses are stored in a database [dbClause](crate::db::clause::db_clause) and in particular the associated methods [initialise_watches](crate::db::clause::db_clause::dbClause::initialise_watches) and [update_watch](crate::db::clause::db_clause::dbClause::initialise_watches).

# Literature

[The art of computer programming, Volume 4](https://www-cs-faculty.stanford.edu/~knuth/taocp.html) discusses watched literals in the *Lazy data structures* section of *Backtracking Algorithms*.
And, Knuth attributes the introduction of watched literals to [An Empirical Comparison of Backtracking Algorithms](https://doi.org/10.1109/TPAMI.1982.4767250).

It seems general use of watched literals followed from [Chaff](https://dl.acm.org/doi/10.1145/378239.379017).[^patent]
[^patent]: [US7418369B2](https://patents.google.com/patent/US7418369B2/en) is a patent covering Chaff, though at the time of writing the status of the patent is 'Expired'.

The given implentation of watch literals follows [Optimal implementation of watched literals and more general techniques](https://www.jair.org/index.php/jair/article/view/10839).

# Implementation

The clauses watching an atom are distinguished by type, with the relevant distinctions set in the [WatchTag] enum.

At present two distinctions are made:

1. Between binary clauses and other clauses.
   - This is made as in a binary clause the watched literals are never updated, and so the *other* literal can be recorded to avoid a trip to the clause itself.
2. Between the value being watched.
   - This is made as the primary use for watch lists is to identify when the value of an atom has been updated.
     In this case, the the purpose of a watch is to note that the literal in the clause is now false, and so either:
       - The watch must be updated.
       - The clause now asserts some literal.
       - The formula being solved cannot be satisfied on the current valuation.

So, in total each atom has four associated watch lists in it's watch database.

Note, a unit clause (a clause containing one literal) never watches any atoms.

The [WatchDB] structure does not have any associated mutating methods.
Instead, mutation of a [WatchDB] is through methods beloning to the [AtomDB](crate::db::atom::AtomDB).
Those methods are included in this file in order to access private members of the [WatchDB].

# Use

Watch lists are inspected and used during [boolean constraint propagation](crate::procedures::bcp).

# Safety
As the [AtomDB](crate::db::atom::AtomDB) methods do not perform a check for whether a [WatchDB] exists for a given atom, these are all marked unsafe.

At present, this is the only use of *unsafe* with respect to [WatchDB]s.
*/

use crate::{
    db::keys::ClauseKey,
    structures::{clause::ClauseKind, literal::CLiteral},
};

/// The watcher of an atom.
pub enum WatchTag {
    /// A binary clause together with the *other* literal in the clause.
    Binary(CLiteral, ClauseKey),

    /// A long clause.
    Long(ClauseKey),
}

/// The status of a watched literal, relative to some given valuation.
#[derive(Clone, Copy, PartialEq)]
pub enum WatchStatus {
    /// The polarity of the watched literal matches the valuation of the atom on the given valuation.\
    /// E.g. if the literal is -p, then p is valued 'false' on the given valuation.
    Witness,

    /// The watched literal has no value on the given valuation.
    None,

    /// The polarity of the watched literal does not match the valuation of the atom on the given valuation.\
    /// E.g. if the literal is -p and p has value 'true' on the given valuation.
    Conflict,
}

/// The watchers of an atom, distinguished by length of clause and which value of the atom is under watch.
pub struct WatchDB {
    /// A watch from a binary clause for a value of `true`.
    pub(super) positive_binary: Vec<WatchTag>,

    /// A watch from a long clause for a value of `true`.
    pub(super) positive_long: Vec<WatchTag>,

    /// A watch from a binary clause for a value of `false`.
    pub(super) negative_binary: Vec<WatchTag>,

    /// A watch from a long clause for a value of `false`.
    pub(super) negative_long: Vec<WatchTag>,
}

impl Default for WatchDB {
    fn default() -> Self {
        Self {
            positive_binary: Vec::default(),
            positive_long: Vec::default(),

            negative_binary: Vec::default(),
            negative_long: Vec::default(),
        }
    }
}

impl WatchDB {
    /// Returns the watchers of `kind` for `value`.
    pub fn watchers(&mut self, kind: ClauseKind, value: bool) -> &[WatchTag] {
        match kind {
            ClauseKind::Empty => panic!("! Attempt to retrieve watch list of empty clauses"),
            ClauseKind::Unit => panic!("! Attempt to retrieve watch list of unit clauses"),
            ClauseKind::Binary => {
                //
                match value {
                    true => &mut self.positive_binary,
                    false => &mut self.negative_binary,
                }
            }
            ClauseKind::Long => {
                //
                match value {
                    true => &mut self.positive_long,
                    false => &mut self.negative_long,
                }
            }
        }
    }
}