二值观察相关文献

Cadical 求解器propagate.cpp传播函数代码注释：

We are using the address of 'decision_reason' as pseudo reason for decisions to distinguish assignment decisions from other assignments.

Before we added chronological backtracking all learned units were assigned at decision level zero ('Solver.level == 0') and we just used a zero pointer as reason.

After allowing chronological backtracking units were also assigned at higher decision level (but with assignment level zero), and it was not possible anymore to just distinguish the case
'unit' versus 'decision' by just looking at the current level.

Both had a zero pointer as reason. Now only units have a zero reason and decisions need to use the pseudo reason 'decision_reason'.

This version of 'propagate' uses lazy watches and keeps two watched literals at the beginning of the clause.

We also use 'blocking literals' to reduce the number of times clauses have to be visited (2008 JSAT paper by Chu, Harwood and Stuckey).

——Cache Conscious Data Structures for Boolean Satisfiability Solvers
Chu, Geoffrey, Harwood, Aaron, and Stuckey, Peter J. ‘Cache Conscious Data Structures for Boolean Satisfiability Solvers’. 1 Jan. 2010 : 99 – 120.

The watches know if a watched clause is binary, in which case it never has to be visited. If a binary clause is falsified we continue propagating.

Finally, for long clauses we save the position of the last watch replacement in 'pos', which in turn reduces certain quadratic accumulated propagation costs (2013 JAIR article by Ian Gent) at the expense of four more bytes for each clause.