Asymmetric branching skips clauses

[mishun]

Lets look at asymmetric branching code:

bool SimpSolver::asymmVar(Var v)
{
    assert(use_simplification);

    const vec<CRef>& cls = occurs.lookup(v);

    if (value(v) != l_Undef || cls.size() == 0)
        return true;

    for (int i = 0; i < cls.size(); i++)
        if (!asymm(v, cls[i]))
            return false;

    return backwardSubsumptionCheck();
}

Note that it calls asymm, wich in turn may call strengthenClause. strengthenClause removes clause from occurs, so in code above clause being at cls[i + 1] ends up at cls[i] and we skip it. It can be tested by taking a copy of occurs.lookup(v) instead of reference --- there is a good chance of changing solver's output for almost any relatively complex sat problem (don't forget to enable asymetric branching).

[mishun]

Actually there is workaround against the similar problem in backwardSubsumptionCheck:

if (!strengthenClause(cs[j], ~l))
    return false;

// Did current candidate get deleted from cs? Then check candidate at index j again:
if (var(l) == best)
    j--;

that works incorrectly if clause contains 2 literals (in that case strengthenClause deletes from occurs lazily).