diff --git a/src/internal/id.rs b/src/internal/id.rs
index 47fe226..07dfd89 100644
--- a/src/internal/id.rs
+++ b/src/internal/id.rs
@@ -114,6 +114,7 @@ impl ArenaId for ClauseId {
         Self(unsafe { NonZeroU32::new_unchecked((x + 1).try_into().expect("clause id too big")) })
     }
 
+    #[inline]
     fn to_usize(self) -> usize {
         (self.0.get() - 1) as usize
     }
diff --git a/src/solver/clause.rs b/src/solver/clause.rs
index 4d53307..47ed74b 100644
--- a/src/solver/clause.rs
+++ b/src/solver/clause.rs
@@ -425,30 +425,6 @@ impl ClauseWatches {
         clause
     }
 
-    pub fn unlink_clause(
-        &mut self,
-        linked_clause: &ClauseWatches,
-        watched_literal: Literal,
-        linked_clause_watch_index: usize,
-    ) {
-        if self.watched_literals[0] == Some(watched_literal) {
-            self.next_watches[0] = linked_clause.next_watches[linked_clause_watch_index];
-        } else {
-            debug_assert_eq!(self.watched_literals[1], Some(watched_literal));
-            self.next_watches[1] = linked_clause.next_watches[linked_clause_watch_index];
-        }
-    }
-
-    #[inline]
-    pub fn next_watched_clause(&self, watched_literal: Literal) -> Option<ClauseId> {
-        if Some(watched_literal) == self.watched_literals[0] {
-            self.next_watches[0]
-        } else {
-            debug_assert_eq!(self.watched_literals[1], Some(watched_literal));
-            self.next_watches[1]
-        }
-    }
-
     pub fn has_watches(&self) -> bool {
         // If the first watch is not null, the second won't be either
         self.watched_literals[0].is_some()
@@ -642,18 +618,6 @@ mod test {
     use super::*;
     use crate::{internal::arena::ArenaId, solver::decision::Decision};
 
-    fn clause(
-        next_clauses: [Option<ClauseId>; 2],
-        watch_literals: Option<[Literal; 2]>,
-    ) -> ClauseWatches {
-        ClauseWatches {
-            watched_literals: watch_literals.map_or([None, None], |literals| {
-                [Some(literals[0]), Some(literals[1])]
-            }),
-            next_watches: next_clauses,
-        }
-    }
-
     #[test]
     #[allow(clippy::bool_assert_comparison)]
     fn test_literal_satisfying_value() {
@@ -685,111 +649,6 @@ mod test {
         assert_eq!(negated_literal.eval(&decision_map), Some(true));
     }
 
-    #[test]
-    fn test_unlink_clause_different() {
-        let clause1 = clause(
-            [
-                ClauseId::from_usize(2).into(),
-                ClauseId::from_usize(3).into(),
-            ],
-            Some([
-                VariableId::from_usize(1596).negative(),
-                VariableId::from_usize(1211).negative(),
-            ]),
-        );
-        let clause2 = clause(
-            [None, ClauseId::from_usize(3).into()],
-            Some([
-                VariableId::from_usize(1596).negative(),
-                VariableId::from_usize(1208).negative(),
-            ]),
-        );
-        let clause3 = clause(
-            [None, None],
-            Some([
-                VariableId::from_usize(1211).negative(),
-                VariableId::from_usize(42).negative(),
-            ]),
-        );
-
-        // Unlink 0
-        {
-            let mut clause1 = clause1.clone();
-            clause1.unlink_clause(&clause2, VariableId::from_usize(1596).negative(), 0);
-            assert_eq!(
-                clause1.watched_literals,
-                [
-                    Some(VariableId::from_usize(1596).negative()),
-                    Some(VariableId::from_usize(1211).negative())
-                ]
-            );
-            assert_eq!(clause1.next_watches, [None, ClauseId::from_usize(3).into()])
-        }
-
-        // Unlink 1
-        {
-            let mut clause1 = clause1;
-            clause1.unlink_clause(&clause3, VariableId::from_usize(1211).negative(), 0);
-            assert_eq!(
-                clause1.watched_literals,
-                [
-                    Some(VariableId::from_usize(1596).negative()),
-                    Some(VariableId::from_usize(1211).negative())
-                ]
-            );
-            assert_eq!(clause1.next_watches, [ClauseId::from_usize(2).into(), None])
-        }
-    }
-
-    #[test]
-    fn test_unlink_clause_same() {
-        let clause1 = clause(
-            [
-                ClauseId::from_usize(2).into(),
-                ClauseId::from_usize(2).into(),
-            ],
-            Some([
-                VariableId::from_usize(1596).negative(),
-                VariableId::from_usize(1211).negative(),
-            ]),
-        );
-        let clause2 = clause(
-            [None, None],
-            Some([
-                VariableId::from_usize(1596).negative(),
-                VariableId::from_usize(1211).negative(),
-            ]),
-        );
-
-        // Unlink 0
-        {
-            let mut clause1 = clause1.clone();
-            clause1.unlink_clause(&clause2, VariableId::from_usize(1596).negative(), 0);
-            assert_eq!(
-                clause1.watched_literals,
-                [
-                    Some(VariableId::from_usize(1596).negative()),
-                    Some(VariableId::from_usize(1211).negative())
-                ]
-            );
-            assert_eq!(clause1.next_watches, [None, ClauseId::from_usize(2).into()])
-        }
-
-        // Unlink 1
-        {
-            let mut clause1 = clause1;
-            clause1.unlink_clause(&clause2, VariableId::from_usize(1211).negative(), 1);
-            assert_eq!(
-                clause1.watched_literals,
-                [
-                    Some(VariableId::from_usize(1596).negative()),
-                    Some(VariableId::from_usize(1211).negative())
-                ]
-            );
-            assert_eq!(clause1.next_watches, [ClauseId::from_usize(2).into(), None])
-        }
-    }
-
     #[test]
     fn test_requires_with_and_without_conflict() {
         let mut decisions = DecisionTracker::new();
diff --git a/src/solver/mod.rs b/src/solver/mod.rs
index efa2bb6..3faf6ad 100644
--- a/src/solver/mod.rs
+++ b/src/solver/mod.rs
@@ -1093,65 +1093,26 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
             return Err(PropagationError::Cancelled(value));
         };
 
-        // Negative assertions derived from other rules (assertions are clauses that
-        // consist of a single literal, and therefore do not have watches)
-        for &(solvable_id, clause_id) in &self.negative_assertions {
-            let value = false;
-            let decided = self
-                .decision_tracker
-                .try_add_decision(Decision::new(solvable_id, value, clause_id), level)
-                .map_err(|_| PropagationError::Conflict(solvable_id, value, clause_id))?;
-
-            if decided {
-                tracing::trace!(
-                    "Negative assertions derived from other rules: Propagate assertion {} = {}",
-                    solvable_id.display(&self.variable_map, self.provider()),
-                    value
-                );
-            }
-        }
-
-        // Assertions derived from learnt rules
-        for learn_clause_idx in 0..self.learnt_clause_ids.len() {
-            let clause_id = self.learnt_clause_ids[learn_clause_idx];
-            let clause = self.clauses.kinds[clause_id.to_usize()];
-            let Clause::Learnt(learnt_index) = clause else {
-                unreachable!();
-            };
-
-            let literals = &self.learnt_clauses[learnt_index];
-            if literals.len() > 1 {
-                continue;
-            }
-
-            debug_assert!(!literals.is_empty());
-
-            let literal = literals[0];
-            let decision = literal.satisfying_value();
-
-            let decided = self
-                .decision_tracker
-                .try_add_decision(
-                    Decision::new(literal.variable(), decision, clause_id),
-                    level,
-                )
-                .map_err(|_| PropagationError::Conflict(literal.variable(), decision, clause_id))?;
-
-            if decided {
-                tracing::trace!(
-                    "├─ Propagate assertion {} = {}",
-                    literal
-                        .variable()
-                        .display(&self.variable_map, self.provider()),
-                    decision
-                );
-            }
-        }
+        // Add decisions from assertions and learned clauses. If any of these cause a
+        // conflict, we will return an error.
+        self.decide_assertions(level)?;
+        self.decide_learned(level)?;
+
+        // For each decision that has not been propagated yet, we propagate the
+        // decision.
+        //
+        // Propagation entails iterating through the linked list of clauses that watch
+        // the literal that the decision caused to turn false. If a clause can only be
+        // satisfied if one of the literals involved is assigned a value, we also make a
+        // decision on that literal to ensure that the clause is satisfied.
+        //
+        // Any new decision is also propagated. If by making a decision on one of the
+        // remaining literals of a clause we cause a conflict, propagation is halted and
+        // an error is returned.
 
-        // Watched solvables
-        let clauses = &self.clauses.kinds;
-        let clause_states = &mut self.clauses.states;
         let interner = self.cache.provider();
+        let clause_kinds = &self.clauses.kinds;
+
         while let Some(decision) = self.decision_tracker.next_unpropagated() {
             let watched_literal = Literal::new(decision.variable, decision.value);
 
@@ -1162,77 +1123,32 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
 
             // Propagate, iterating through the linked list of clauses that watch this
             // solvable
-            let mut old_predecessor_clause_id: Option<ClauseId>;
-            let mut predecessor_clause_id: Option<ClauseId> = None;
-            let mut next_clause_id = self.watches.first_clause_watching_literal(watched_literal);
-            while let Some(clause_id) = next_clause_id {
-                debug_assert!(
-                    predecessor_clause_id != Some(clause_id),
-                    "Linked list is circular!"
-                );
-
-                // Get mutable access to both clauses.
-                let (predecessor_clause_state, clause_state) =
-                    if let Some(prev_clause_id) = predecessor_clause_id {
-                        let prev_idx = prev_clause_id.to_usize();
-                        let current_idx = clause_id.to_usize();
-                        if prev_idx < current_idx {
-                            let (left, right) = clause_states.split_at_mut(current_idx);
-                            (Some(&mut left[prev_idx]), &mut right[0])
-                        } else {
-                            let (left, right) = clause_states.split_at_mut(prev_idx);
-                            (Some(&mut right[0]), &mut left[current_idx])
-                        }
-                    } else {
-                        (None, &mut clause_states[clause_id.to_usize()])
-                    };
-
-                // Update the prev_clause_id for the next run
-                old_predecessor_clause_id = predecessor_clause_id;
-                predecessor_clause_id = Some(clause_id);
-
-                // Configure the next clause to visit
-                next_clause_id = clause_state.next_watched_clause(watched_literal);
-
-                // Determine which of the two literals that the clause is watching turned false.
-                let (watch_index, other_watch_index) =
-                    if clause_state.watched_literals[0] == Some(watched_literal) {
-                        (0, 1)
-                    } else {
-                        debug_assert_eq!(clause_state.watched_literals[1], Some(watched_literal));
-                        (1, 0)
-                    };
-
-                // Find another literal to watch. If we can't find one, the other literal must
-                // be set to true for the clause to still hold.
-                let other_watched_literal = clause_state.watched_literals[other_watch_index]
-                    .expect("clauses are always watching two literals");
+            let mut next_cursor = self
+                .watches
+                .cursor(&mut self.clauses.states, watched_literal);
+            while let Some(mut cursor) = next_cursor.take() {
+                let clause_id = cursor.clause_id();
+                let clause = &clause_kinds[clause_id.to_usize()];
+                let watch_index = cursor.watch_index();
+
+                // If the other literal the current clause is watching is already true, we can
+                // skip this clause. Its is already satisfied.
+                let other_watched_literal = cursor.other_literal();
                 if other_watched_literal.eval(self.decision_tracker.map()) == Some(true) {
-                    // If the other watch is already true, we can simply skip
-                    // this clause.
-                } else if let Some(variable) = clause_state.next_unwatched_literal(
-                    &clauses[clause_id.to_usize()],
+                    // Continue with the next clause in the linked list.
+                    next_cursor = cursor.next();
+                } else if let Some(literal) = cursor.watches().next_unwatched_literal(
+                    clause,
                     &self.learnt_clauses,
                     &self.requirement_to_sorted_candidates,
                     self.decision_tracker.map(),
                     watch_index,
                 ) {
-                    self.watches.update_watched(
-                        predecessor_clause_state,
-                        clause_state,
-                        clause_id,
-                        watch_index,
-                        watched_literal,
-                        variable,
-                    );
-
-                    // Make sure the right predecessor is kept for the next iteration (i.e. the
-                    // current clause is no longer a predecessor of the next one; the current
-                    // clause's predecessor is)
-                    predecessor_clause_id = old_predecessor_clause_id;
+                    // Update the watch to point to the new literal
+                    next_cursor = cursor.update(literal);
                 } else {
                     // We could not find another literal to watch, which means the remaining
-                    // watched literal can be set to true
+                    // watched literal must be set to true.
                     let decided = self
                         .decision_tracker
                         .try_add_decision(
@@ -1252,7 +1168,6 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                         })?;
 
                     if decided {
-                        let clause = &clauses[clause_id.to_usize()];
                         match clause {
                             // Skip logging for ForbidMultipleInstances, which is so noisy
                             Clause::ForbidMultipleInstances(..) => {}
@@ -1268,6 +1183,9 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
                             }
                         }
                     }
+
+                    // Skip to the next clause in the linked list.
+                    next_cursor = cursor.next();
                 }
             }
         }
@@ -1275,6 +1193,69 @@ impl<D: DependencyProvider, RT: AsyncRuntime> Solver<D, RT> {
         Ok(())
     }
 
+    /// Add decisions for negative assertions derived from other rules
+    /// (assertions are clauses that consist of a single literal, and
+    /// therefore do not have watches).
+    fn decide_assertions(&mut self, level: u32) -> Result<(), PropagationError> {
+        for &(solvable_id, clause_id) in &self.negative_assertions {
+            let value = false;
+            let decided = self
+                .decision_tracker
+                .try_add_decision(Decision::new(solvable_id, value, clause_id), level)
+                .map_err(|_| PropagationError::Conflict(solvable_id, value, clause_id))?;
+
+            if decided {
+                tracing::trace!(
+                    "Negative assertions derived from other rules: Propagate assertion {} = {}",
+                    solvable_id.display(&self.variable_map, self.provider()),
+                    value
+                );
+            }
+        }
+        Ok(())
+    }
+
+    /// Add decisions derived from learnt clauses.
+    fn decide_learned(&mut self, level: u32) -> Result<(), PropagationError> {
+        // Assertions derived from learnt rules
+        for learn_clause_idx in 0..self.learnt_clause_ids.len() {
+            let clause_id = self.learnt_clause_ids[learn_clause_idx];
+            let clause = self.clauses.kinds[clause_id.to_usize()];
+            let Clause::Learnt(learnt_index) = clause else {
+                unreachable!();
+            };
+
+            let literals = &self.learnt_clauses[learnt_index];
+            if literals.len() > 1 {
+                continue;
+            }
+
+            debug_assert!(!literals.is_empty());
+
+            let literal = literals[0];
+            let decision = literal.satisfying_value();
+
+            let decided = self
+                .decision_tracker
+                .try_add_decision(
+                    Decision::new(literal.variable(), decision, clause_id),
+                    level,
+                )
+                .map_err(|_| PropagationError::Conflict(literal.variable(), decision, clause_id))?;
+
+            if decided {
+                tracing::trace!(
+                    "├─ Propagate assertion {} = {}",
+                    literal
+                        .variable()
+                        .display(&self.variable_map, self.provider()),
+                    decision
+                );
+            }
+        }
+        Ok(())
+    }
+
     /// Adds the clause with `clause_id` to the current [`Conflict`]
     ///
     /// Because learnt clauses are not relevant for the user, they are not added
diff --git a/src/solver/watch_map.rs b/src/solver/watch_map.rs
index bb9d8f4..c506cdf 100644
--- a/src/solver/watch_map.rs
+++ b/src/solver/watch_map.rs
@@ -1,5 +1,5 @@
 use crate::{
-    internal::{id::ClauseId, mapping::Mapping},
+    internal::{arena::ArenaId, id::ClauseId, mapping::Mapping},
     solver::clause::{ClauseWatches, Literal},
 };
 
@@ -33,39 +33,165 @@ impl WatchMap {
         }
     }
 
-    pub(crate) fn update_watched(
-        &mut self,
-        predecessor_clause: Option<&mut ClauseWatches>,
-        clause: &mut ClauseWatches,
-        clause_id: ClauseId,
-        watch_index: usize,
-        previous_watch: Literal,
-        new_watch: Literal,
-    ) {
-        // Remove this clause from its current place in the linked list, because we
-        // are no longer watching what brought us here
-        if let Some(predecessor_clause) = predecessor_clause {
-            // Unlink the clause
-            predecessor_clause.unlink_clause(clause, previous_watch, watch_index);
-        } else if let Some(next_watch) = clause.next_watches[watch_index] {
-            // This was the first clause in the chain
-            self.map.insert(previous_watch, next_watch);
+    /// Returns a [`WatchMapCursor`] that can be used to navigate and manipulate
+    /// the linked list of the clauses that are watching the specified
+    /// literal.
+    pub fn cursor<'a>(
+        &'a mut self,
+        watches: &'a mut [ClauseWatches],
+        literal: Literal,
+    ) -> Option<WatchMapCursor<'a>> {
+        let clause_id = *self.map.get(literal)?;
+        let watch_index = if watches[clause_id.to_usize()].watched_literals[0] == Some(literal) {
+            0
         } else {
-            self.map.unset(previous_watch);
-        }
+            debug_assert_eq!(
+                watches[clause_id.to_usize()].watched_literals[1],
+                Some(literal),
+                "the clause is not actually watching the literal"
+            );
+            1
+        };
 
-        // Set the new watch
-        clause.watched_literals[watch_index] = Some(new_watch);
-        let previous_clause_id = self.map.insert(new_watch, clause_id);
-        clause.next_watches[watch_index] = previous_clause_id;
+        Some(WatchMapCursor {
+            watch_map: self,
+            watches,
+            literal,
+            previous: None,
+            current: WatchNode {
+                clause_id,
+                watch_index,
+            },
+        })
     }
+}
 
-    /// Returns the id of the first clause that is watching the specified
-    /// literal.
-    pub(crate) fn first_clause_watching_literal(
-        &mut self,
-        watched_literal: Literal,
-    ) -> Option<ClauseId> {
-        self.map.get(watched_literal).copied()
+struct WatchNode {
+    /// The index of the [`ClauseWatches`]
+    clause_id: ClauseId,
+
+    /// A [`ClauseWatches`] contains the state for two linked lists. This index
+    /// indicates which of the two linked-list nodes is referenced.
+    watch_index: usize,
+}
+
+/// The watchmap contains a linked-list of clauses that are watching a certain
+/// literal. This linked-list is a singly linked list, which requires some
+/// administration when trying to modify the list. The [`WatchMapCursor`] is a
+/// utility that allows navigating the linked-list and manipulate it.
+///
+/// A cursor is created using [`WatchMap::cursor`]. The cursor can iterate
+/// through all the clauses using [`WatchMapCursor::next`] and a single watch
+/// can be updated using the [`WatchMapCursor::update`] method.
+pub struct WatchMapCursor<'a> {
+    /// The watchmap that is being navigated.
+    watch_map: &'a mut WatchMap,
+
+    /// The nodes of the linked list.
+    watches: &'a mut [ClauseWatches],
+
+    /// The literal who's linked list is being navigated.
+    literal: Literal,
+
+    /// The previous node we iterated or `None` if this is the head.
+    previous: Option<WatchNode>,
+
+    /// The current node.
+    current: WatchNode,
+}
+
+impl<'a> WatchMapCursor<'a> {
+    /// Skip to the next node in the linked list. Returns `None` if there is no
+    /// next node.
+    pub fn next(mut self) -> Option<Self> {
+        let next = self.next_node()?;
+
+        self.previous = Some(self.current);
+        self.current = next;
+
+        Some(self)
+    }
+
+    /// Returns the next node in the linked list or `None` if there is no next.
+    fn next_node(&self) -> Option<WatchNode> {
+        let next_clause_id =
+            self.watches[self.current.clause_id.to_usize()].next_watches[self.current.watch_index]?;
+        let next_clause_watch_index =
+            if self.watches[next_clause_id.to_usize()].watched_literals[0] == Some(self.literal) {
+                0
+            } else {
+                debug_assert_eq!(
+                    self.watches[next_clause_id.to_usize()].watched_literals[1],
+                    Some(self.literal),
+                    "the clause is not actually watching the literal"
+                );
+                1
+            };
+
+        Some(WatchNode {
+            clause_id: next_clause_id,
+            watch_index: next_clause_watch_index,
+        })
+    }
+
+    /// Returns the other literal that the current clause is watching.
+    pub fn other_literal(&self) -> Literal {
+        self.watches[self.current.clause_id.to_usize()].watched_literals
+            [1 - self.current.watch_index]
+            .expect("clauses never watch just one literal")
+    }
+
+    /// The current clause that is being navigated.
+    pub fn clause_id(&self) -> ClauseId {
+        self.current.clause_id
+    }
+
+    /// Returns the watches of the current clause.
+    pub fn watches(&mut self) -> &mut ClauseWatches {
+        &mut self.watches[self.current.clause_id.to_usize()]
+    }
+
+    /// Returns the index of the current watch in the current clause.
+    pub fn watch_index(&self) -> usize {
+        self.current.watch_index
+    }
+
+    /// Update the current watch to a new literal. This removes the current node
+    /// from the linked-list and sets up a watch on the new literal.
+    ///
+    /// Returns a cursor that points to the next node in the linked list or
+    /// `None` if there is no next.
+    pub fn update(mut self, new_watch: Literal) -> Option<Self> {
+        debug_assert_ne!(
+            new_watch, self.literal,
+            "cannot update watch to the same literal"
+        );
+
+        let clause_idx = self.current.clause_id.to_usize();
+        let next_node = self.next_node();
+
+        // Update the previous node to point to the next node in the linked list
+        // (effectively removing this one).
+        if let Some(previous) = &self.previous {
+            // If there is a previous node we update that node to point to the next.
+            self.watches[previous.clause_id.to_usize()].next_watches[previous.watch_index] =
+                next_node.as_ref().map(|node| node.clause_id);
+        } else if let Some(next_clause_id) = next_node.as_ref().map(|node| node.clause_id) {
+            // If there is no previous node, we are the head of the linked list.
+            self.watch_map.map.insert(self.literal, next_clause_id);
+        } else {
+            self.watch_map.map.unset(self.literal);
+        }
+
+        // Set the new watch for the current clause.
+        let watch = &mut self.watches[clause_idx];
+        watch.watched_literals[self.current.watch_index] = Some(new_watch);
+        let previous_clause_id = self.watch_map.map.insert(new_watch, self.current.clause_id);
+        watch.next_watches[self.current.watch_index] = previous_clause_id;
+
+        // Update the current
+        self.current = next_node?;
+
+        Some(self)
     }
 }