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
TopiRestart.cc
// Copyright(C) 2021-2022 Intel Corporation
// SPDX - License - Identifier: MIT
#include "Topi.hpp"
#include <climits>
using namespace Topor;
using namespace std;
template <typename TLit, typename TUInd, bool Compress>
bool CTopi<TLit,TUInd,Compress>::Restart()
{
bool restartNow = false;
switch (m_CurrRestartStrat)
{
case RESTART_STRAT_NUMERIC:
restartNow = m_DecLevel > 0 && m_ParamRestartNumericLocal ?
m_ConfsSinceRestart - m_RstNumericLocalConfsSinceRestartAtDecLevelCreation[m_DecLevel] >= m_RstNumericCurrConfThr :
m_ConfsSinceRestart >= m_RstNumericCurrConfThr;
if (restartNow)
{
if (m_ParamRestartNumericSubStrat == 1)
{
// Luby
m_RstNumericCurrConfThr = (uint64_t)(RestartLubySequence(m_ParamRestartLubyConfIncr, m_Stat.m_Restarts) * (double)m_ParamRestartNumericInitConfThr);
}
else
{
// Arithmetic
m_RstNumericCurrConfThr += m_ParamRestartArithmeticConfIncr;
}
}
break;
case RESTART_STRAT_LBD:
restartNow = m_RstGlueLbdWin.IsFullWindow() && m_RstGlueLbdWin.GetAverage() * m_ParamRestartLbdAvrgMult > m_RstGlueGlobalLbdSum / (double)m_RstGlueAssertingGluedClss;
if (restartNow)
{
m_RstGlueLbdWin.Clear();
}
break;
default:
break;
}
if (unlikely(restartNow))
{
m_ConfsSinceRestart = 0;
++m_Stat.m_Restarts;
++m_RestartsSinceInvStart;
UpdateAllUipInfoAfterRestart();
assert(m_QueryCurr != TQueryType::QUERY_NONE);
const auto currUnforceRestartsFraction = GetCurrUnforceRestartsFraction();
if (currUnforceRestartsFraction != 0. && currUnforceRestartsFraction != 1.)
{
const uint64_t restartInBlock = m_RestartsSinceInvStart % (uint64_t)m_ParamPhaseMngRestartsBlockSize;
const double currRestartFractionCompleted = (double)restartInBlock / (double)m_ParamPhaseMngRestartsBlockSize;
assert(currRestartFractionCompleted >= 0.);
const double currRestartFractionLeft = 1. - currRestartFractionCompleted;
assert(currRestartFractionLeft >= 0.);
if (m_PhaseStage == m_PhaseInitStage)
{
if (m_PhaseStage == TPhaseStage::PHASE_STAGE_STANDARD && currRestartFractionLeft <= currUnforceRestartsFraction)
{
m_PhaseStage = TPhaseStage::PHASE_STAGE_DONT_FORCE;
assert(m_PhaseInitStage != m_PhaseStage);
assert(NV(1) || P("Phase stage changed: " + GetPhaseStageStr() + "\n"));
}
else if (m_PhaseStage == TPhaseStage::PHASE_STAGE_DONT_FORCE && currRestartFractionCompleted >= currUnforceRestartsFraction)
{
m_PhaseStage = TPhaseStage::PHASE_STAGE_STANDARD;
assert(m_PhaseInitStage != m_PhaseStage);
assert(NV(1) || P("Phase stage changed: " + GetPhaseStageStr() + "\n"));
}
}
}
assert(NV(1) || P("Restart #" + to_string(m_Stat.m_Restarts) + "\n"));
}
return restartNow;
}
template <typename TLit, typename TUInd, bool Compress>
void CTopi<TLit,TUInd,Compress>::RstNewAssertingGluedCls(TUV glue)
{
assert(m_CurrRestartStrat == RESTART_STRAT_LBD);
if (m_ParamRestartLbdBlockingEnable)
{
m_RstGlueBlckAsgnWin.Enqueue(m_AssignedVarsNum);
if (m_RstGlueAssertingGluedClss > m_ParamRestartLbdBlockingConfsToConsider && m_RstGlueLbdWin.IsFullWindow() && (double)m_AssignedVarsNum > m_ParamRestartLbdBlockingAvrgMult * m_RstGlueBlckAsgnWin.GetAverage())
{
m_RstGlueLbdWin.Clear();
++m_Stat.m_RestartsBlocked;
}
}
const auto glueThr = glue > m_ParamRestartLbdThresholdGlueVal ? m_ParamRestartLbdThresholdGlueVal : glue;
m_RstGlueLbdWin.Enqueue(glueThr);
m_RstGlueGlobalLbdSum += (double)glueThr;
}
template <typename TLit, typename TUInd, bool Compress>
void CTopi<TLit,TUInd,Compress>::RestartInit()
{
assert(m_QueryCurr != TQueryType::QUERY_NONE);
auto InitGlue = [&]()
{
if (m_ParamRestartLbdBlockingEnable)
{
m_RstGlueBlckAsgnWin.Init(m_ParamRestartLbdBlockingWinSize);
if (unlikely(m_RstGlueBlckAsgnWin.IsError())) SetStatus(TToporStatus::STATUS_ALLOC_FAILED, "Couldn't reserve memory for m_RstGlueBlckAsgnWin");
}
m_RstGlueLbdWin.Init(m_ParamRestartLbdWinSize);
if (unlikely(m_RstGlueLbdWin.IsError())) SetStatus(TToporStatus::STATUS_ALLOC_FAILED, "Couldn't reserve memory for m_RstGlueLbdWin");
};
if (m_QueryCurr == TQueryType::QUERY_INIT)
{
m_CurrRestartStrat = m_ParamRestartStrategyInit;
if (m_CurrRestartStrat == RESTART_STRAT_NUMERIC)
{
m_RstNumericCurrConfThr = m_ParamRestartNumericInitConfThr;
assert(NV(1) || P("Restarts initialized to arithmetic\n"));
}
else if (m_CurrRestartStrat == RESTART_STRAT_LBD)
{
InitGlue();
assert(NV(1) || P("Restarts initialized to glue\n"));
}
}
else if (m_ParamRestartStrategyInit != m_ParamRestartStrategyS || m_ParamRestartStrategyInit != m_ParamRestartStrategyN)
{
const uint8_t prevRestartStrat = m_CurrRestartStrat;
assert(m_QueryCurr == TQueryType::QUERY_INC_SHORT || m_QueryCurr == TQueryType::QUERY_INC_NORMAL);
m_CurrRestartStrat = m_QueryCurr == TQueryType::QUERY_INC_SHORT ? m_ParamRestartStrategyS : m_ParamRestartStrategyN;
if (m_CurrRestartStrat != prevRestartStrat)
{
assert(prevRestartStrat == RESTART_STRAT_LBD || prevRestartStrat == RESTART_STRAT_NUMERIC);
assert(m_CurrRestartStrat == RESTART_STRAT_LBD || m_CurrRestartStrat == RESTART_STRAT_NUMERIC);
if (m_CurrRestartStrat == RESTART_STRAT_NUMERIC)
{
// LBD --> NUMERIC
assert(prevRestartStrat == RESTART_STRAT_LBD);
m_RstNumericCurrConfThr = m_Stat.m_Conflicts + m_ParamRestartNumericInitConfThr;
if (m_ParamRestartLbdBlockingEnable)
{
m_RstGlueBlckAsgnWin.Clear();
}
m_RstGlueLbdWin.Clear();
assert(NV(1) || P("Restarts switched to arithmetic\n"));
}
else
{
// NUMERIC --> LBD
assert(prevRestartStrat == RESTART_STRAT_NUMERIC);
InitGlue();
assert(NV(1) || P("Restarts switched to glue\n"));
}
}
}
const auto currUnforceRestartsFraction = GetCurrUnforceRestartsFraction();
m_PhaseInitStage = m_PhaseStage =
currUnforceRestartsFraction == 0. ? TPhaseStage::PHASE_STAGE_STANDARD :
currUnforceRestartsFraction == 1. ? TPhaseStage::PHASE_STAGE_DONT_FORCE :
m_ParamPhaseMngStartInvStrat == 0 ? TPhaseStage::PHASE_STAGE_STANDARD : m_ParamPhaseMngStartInvStrat == 1 ? TPhaseStage::PHASE_STAGE_DONT_FORCE :
((double)rand() / (double)INT_MAX <= currUnforceRestartsFraction ? TPhaseStage::PHASE_STAGE_DONT_FORCE : TPhaseStage::PHASE_STAGE_STANDARD);
m_RestartsSinceInvStart = 0;
assert(NV(1) || P("Phase stage set: " + GetPhaseStageStr() + "\n"));
}
template <typename TLit, typename TUInd, bool Compress>
double CTopi<TLit,TUInd,Compress>::RestartLubySequence(double y, uint64_t x)
{
// Finite subsequences of the Luby-sequence:
// 0: 1
// 1: 1 1 2
// 2: 1 1 2 1 1 2 4
// 3: 1 1 2 1 1 2 4 1 1 2 1 1 2 4 8
// ...
// Find the finite subsequence that contains index 'x' and the size of that subsequence:
uint64_t size = 1, seq = 0;
for (; size < x + 1; seq++, size = 2 * size + 1);
while (size - 1 != x)
{
size = (size - 1) >> 1;
seq--;
x = x % size;
}
return pow(y, seq);
}
template class CTopi<int32_t, uint32_t, false>;
template class CTopi<int32_t, uint64_t, false>;
template class CTopi<int32_t, uint64_t, true>;