Let's recycle!

I gave it up.

2021-10-01T00:00 🌀

できるにはできたけど、かなりの割合で再利用されるようになったけど、性能があがらん。というかやや遅くなってベンチマークをかける気にならない。うーむ。まあ論文で示された結果はそれほど劇的な改善というわけではなかったのでこれでも想定内と考えるべきなのか。

バリエーションとして

repropagateはするけども矛盾は再利用しない（もっと大事な矛盾を見つけるかもしれない）。これはConflict qualityのバリエーション。
propagateの最初で挿入するのはやめる。新規含意リテラルで走査してから、再利用を始める。これももっと重要なリテラルの影響を優先する試み。

を評価中。

2021-09-30T08:00

できた。つまり、binary clauseが矛盾を起こしたときのliteral flipを嫌ったのが原因。その場合の手当を追加すれば論文通りに実装できる。

    if let Err(mut cc) = self.append_saved_literals() {
        if cc.link != NULL_LIT && self.locked(cdb[cc.cid], cc.cid) {
            cc.link = cdb[cc.cid].lit0();
        }
        return Some(cc);
    }

2021-09-30

いったいこれは何を意味しているんだ？

    if let Err(mut cc) = self.append_saved_literals() {
        let c = &cdb[cc.cid];
        let ret = if self.locked(c, cc.cid) {
            Some(cc)
        } else if cc.link != NULL_LIT {
            cc.link = cdb[cc.cid].lit0();
            Some(cc)
        } else {
            None
        };
        if ret.is_some() {
            return ret;
        }
    }

conflictを全て無視すると動く
lockされている節によるconflictは利用しても問題ない
binary clauseは正規化してやれば問題ない

では、それ以外の節は「正規化」できないのか？

2021-09-28

このように短いコードなので、1日で実装終わるはずだったのに3日ほどデバッグで苦しんでしまった。

一体何が問題だったかというと、reason_savedに入れた節がいつの間にかreasonでなくっていたせい。確かに他の伝播（つまり別リテラルのreasonに使われる）場合、節内リテラル順序は変更されるのでそういう場合を想定しなければならない。少なくともSplrでは（論文ではどういう実装を考えているのだ？）。

そして観測を続けると、reason_savedに保存された節の全てのリテラルが否定されることがあるようだ。これは矛盾状態なので、どのリテラルで考えるかによらず（先頭がどのリテラルなのかを気にすることなく）矛盾解析に回してよさそうだが、矛盾扱いすると、UNSAT certificateがおかしくなってしまう。

一体何が起きているのだろう。 q_headの更新し忘れなのだろうか。

Trail Saving on Back Jump

ChronoBTがちゃんと動かない！いくら考えてもなぜUNSAT certificateがおかしくなるのか見当もつかないので、諦めてもっと新しいアプローチに乗り換えることにした！ Splr-0.13にランディングの予定。

[1] Randy Hickey and Fahiem Bacchus, Trail Saving on Backtrack, SAT 2020, LNCS 12178, pp.46-61, 2020.

preparation

先頭部が削除、追加されるので使用するデータ型はスタックにした。

sturct AssignStack {
    /// Partial record of unassigned assignments as stack
    trail_saved: Vec<Lit>,
    reason_saved: Vec<AssignReason>,
}

fn backtrack

fn backtrack(&mut self, bt_level: DecisionLevel) {
  let current_level = self.decision_level();
  let head = self.len_upto(bt_level + 1);
  for lit in self.trail[head..self.len_upto(current_level - 1)].rev() {
    let vi = lit.vi();
    // copy the reason
    self.reason_saved[vi] = self.reason[vi];
    // save the assign
    self.trail_saved.push(lit);
  }
  self.trail.truncate(head);
}

fn propagate

返値の型をOptionからResultに変更した。

fn new_propagate(&mut self) -> Result<(), ConflictContext> {
    while self.remains() {
        self.use_saved_trail()?;
        // 以前のpropagateの処理を1リテラル分だけ走らせる。
        self.propagate_single()?;
    }
    Ok(())
}

fn use_saved_trail

以下の2つは等価だから条件式は O(1) なものに変換した。

self.trail.contains(&lit)
self.assigned(lit) == Some(true)

fn use_saved_trail(&mut) -> Result<(), ConflictContext> {
    for i in (0..self.trail_saved.len()).rev() {
        let lit = self.trail_saved[i];
        let vi = lit.vi();
        match self.reason_saved[vi] {
            AssignReason::Decision => {
                if self.assigned(lit) == Some(true) {
                    continue;
                }
                self.trail_saved.truncate(i + 1);
                return Ok(());
            }
            AssignReason::Implication(c, l) => {
                match self.assigned(lit) {
                    Some(true) => continue,
                    Some(false) => return Err(ConflictContext{ cid: c, link: l}),
                    None => { self.assign_by_implication(lit, _, c, l) }
                }
            }
            AssignReason::Asserted(_) => panic!("impossible path"),
            AssignReason::None => panic!("impossible path"),
        }
    }
}

Published at 2021-09-23 Last updated 2021-10-01