1 ConflictData data = FindConflictLevel(confl); 2 3 if (data.nHighestLevel == 0) return l_False; 4 5 if (data.bOnlyOneLitFromHighest) 6 { 7 cancelUntil(data.nHighestLevel - 1); 8 continue; 9 }
|
|
1 inline Solver::ConflictData Solver::FindConflictLevel(CRef cind) 2 { 3 ConflictData data; 4 Clause& conflCls = ca[cind]; 5 data.nHighestLevel = level(var(conflCls[0])); 6 if (data.nHighestLevel == decisionLevel() && level(var(conflCls[1])) == decisionLevel()) 7 { 8 return data; 9 } 10 11 int highestId = 0; 12 data.bOnlyOneLitFromHighest = true; 13 // find the largest decision level in the clause 14 for (int nLitId = 1; nLitId < conflCls.size(); ++nLitId) 15 { 16 int nLevel = level(var(conflCls[nLitId])); 17 if (nLevel > data.nHighestLevel) 18 { 19 highestId = nLitId; 20 data.nHighestLevel = nLevel; 21 data.bOnlyOneLitFromHighest = true; 22 } 23 else if (nLevel == data.nHighestLevel && data.bOnlyOneLitFromHighest == true) 24 { 25 data.bOnlyOneLitFromHighest = false; 26 } 27 } 28 29 if (highestId != 0) 30 { 31 std::swap(conflCls[0], conflCls[highestId]); 32 if (highestId > 1) 33 { 34 OccLists<Lit, vec<Watcher>, WatcherDeleted>& ws
|
|