Theory propegation requirements

[dewert99]

As I thinking about batsats non-chronological backtracking with theory propagation I started wondering what requirements the theory propagation had, eg. "a theories explanation of a propagated literal must contain a literal from the level the propagation happened ", or "a theory must not propagate a literal that was falsified at a level earlier than the current level". As an experiment I created OddTheory<Th> that wraps a theory causing to only propagate add odd decision levels (see below), and ran the sudoku tests using it. This gave

thread 'main' panicked at /home/dewert/Repos/batsat/src/batsat/src/core.rs:1406:21:
possible cycle in conflict graph between -43 and -43
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
16a17,542

Either this is a bug in the sudoku solver, or delaying propagation should not be allowed. I'm not sure how hard/costly (runtime) this would be to fix, but it would be nice to have the propagation requirements documented.

[dewert99]

OddTheory:

use std::ops::{Deref, DerefMut};
use batsat::{Lit, Theory, TheoryArg};

#[derive(Default)]
pub struct OddTheory<Th>(pub Th);

impl<Th: Theory> Theory for OddTheory<Th> {
    fn final_check(&mut self, acts: &mut TheoryArg) {
        self.0.final_check(acts)
    }

    fn create_level(&mut self) {
        self.0.create_level()
    }

    fn pop_levels(&mut self, n: usize) {
        self.0.pop_levels(n)
    }

    fn n_levels(&self) -> usize {
        self.0.n_levels()
    }

    fn partial_check(&mut self, acts: &mut TheoryArg) {
        if self.0.n_levels() % 2 == 1 {
            self.0.partial_check(acts)
        }
    }

    fn explain_propagation(&mut self, p: Lit) -> &[Lit] {
        self.0.explain_propagation(p)
    }
}

impl<Th> Deref for OddTheory<Th> {
    type Target = Th;

    fn deref(&self) -> &Self::Target {
        &self.0
    }
}

impl<Th> DerefMut for OddTheory<Th> {
    fn deref_mut(&mut self) -> &mut Self::Target {
        &mut self.0
    }
}

[c-cube]

Sorry I've been slow to answer your questions/PRs! Indeed, a requirement is that theories that propagate do propagate eagerly, ie a propagation must be done at the earliest level where it holds. In other words, as you point out, a propagation must contain one literal that's true at the current level (and obv all the literals in the explanation must be true; and the conclusion must be true or undecided iirc). These invariants could be checked with reasonably low overhead using debug_assert!.