https://github.com/alexander-nadel/intel_sat_solver
Tip revision: 8a99f85649d80d06a6dddd61e1be5d38eac81997 authored by Alexander Nadel on 17 May 2023, 06:42:21 UTC
A major update, described in the SAT'23 paper Solving Huge Instances with Intel(R) SAT Solver
A major update, described in the SAT'23 paper Solving Huge Instances with Intel(R) SAT Solver
Tip revision: 8a99f85
TopiBacktrack.cc
// Copyright(C) 2021-2022 Intel Corporation
// SPDX - License - Identifier: MIT
#include "Topi.hpp"
using namespace Topor;
using namespace std;
template <typename TLit, typename TUInd, bool Compress>
void CTopi<TLit,TUInd,Compress>::BacktrackingInit()
{
m_CurrChronoBtIfHigher = m_QueryCurr == TQueryType::QUERY_INC_SHORT ? m_ParamChronoBtIfHigherS : m_QueryCurr == TQueryType::QUERY_INC_NORMAL ? m_ParamChronoBtIfHigherN : m_ParamChronoBtIfHigherInit;
m_CurrCustomBtStrat = m_QueryCurr == TQueryType::QUERY_INC_SHORT ? m_ParamCustomBtStratS : m_QueryCurr == TQueryType::QUERY_INC_NORMAL ? m_ParamCustomBtStratN : m_ParamCustomBtStratInit;
m_ConfsSinceNewInv = m_Stat.m_Conflicts;
}
template <typename TLit, typename TUInd, bool Compress>
void CTopi<TLit,TUInd,Compress>::Backtrack(TLit decLevelL, bool isBCPBacktrack, bool reuseTrail, bool isAPICall)
{
TUV decLevel = (TUV)decLevelL;
// cout << "\tc b <BacktrackLevel>" << endl;
if (m_DumpFile && isAPICall) (*m_DumpFile) << "b " << decLevel << endl;
if (decLevel >= m_DecLevel)
{
return;
}
if (m_ParamReuseTrail)
{
m_ReuseTrail.clear();
}
assert(NV(2) || P("***** Backtracking to " + to_string(decLevel) + "\n"));
++m_Stat.m_Backtracks;
if (isBCPBacktrack) ++m_Stat.m_BCPBacktracks;
m_Stat.m_ChronoBacktracks += (decLevel == m_DecLevel - 1);
// Cleaning up collapsed decision levels
while (decLevel != 0 && m_TrailLastVarPerDecLevel[decLevel] == BadClsInd)
{
if (decLevel == m_DecLevelOfLastAssignedAssumption)
{
--m_DecLevelOfLastAssignedAssumption;
}
--decLevel;
}
while (m_TrailEnd != m_TrailLastVarPerDecLevel[decLevel])
{
UnassignVar(m_TrailEnd, reuseTrail);
}
m_DecLevel = decLevel;
assert(NV(2) || P("***** Backtracked to " + to_string(m_DecLevel) + "\n"));
assert(NV(2) || !m_ParamReuseTrail || P(SReuseTrail()) + "\n");
}
template class CTopi<int32_t, uint32_t, false>;
template class CTopi<int32_t, uint64_t, false>;
template class CTopi<int32_t, uint64_t, true>;