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
TopiVarScores.hpp
// Copyright(C) 2021-2022 Intel Corporation
// SPDX - License - Identifier: MIT
#pragma once
#include "ToporVector.hpp"
// Variable scores handler, including a heap implementation
namespace Topor
{
template <typename TUVar, typename TUV>
class CVarScores
{
public:
// The heap's 0 index must always be occupied, so that position 0 would mean not-in-the-heap
CVarScores(double& varActivityInc) : m_VarActivityInc(varActivityInc), m_Heap(1, 0, 1)
{
static_assert(std::is_same<TUVar, TUV>::value);
}
void SetInitOrder(bool initOrder)
{
m_InitOrder = initOrder;
}
void reserve_exactly(size_t beyondMaxVar)
{
m_PosScore.reserve_exactly(beyondMaxVar, 0);
m_Heap.reserve_exactly(beyondMaxVar);
}
inline bool uninitialized_or_erroneous() const
{
return m_PosScore.uninitialized_or_erroneous() || m_Heap.uninitialized_or_erroneous();
}
inline size_t size() const { return m_Heap.size() - 1; }
inline bool empty() const { return size() == 0; }
inline bool in_heap(TUVar v) const { assert(v < m_PosScore.cap()); return m_PosScore[v].m_Pos > 0; }
bool increase_score(TUVar v, double mult = 1.0)
{
bool isRescaled = false;
if (unlikely((m_PosScore[v].m_Score += m_VarActivityInc * mult) > 1e100))
{
span<TPosScore> posScoreSpan = m_PosScore.get_span_cap();
// Rescale
for (auto& currPosScore : posScoreSpan)
{
currPosScore.m_Score *= 1e-100;
}
m_VarActivityInc *= 1e-100;
isRescaled = true;
}
if (in_heap(v))
{
percolate_up(m_PosScore[v].m_Pos);
}
return isRescaled;
}
void reinsert_if_not_in_heap(TUVar v)
{
assert(!uninitialized_or_erroneous());
assert(v < m_PosScore.cap());
if (!in_heap(v))
{
m_PosScore[v].m_Pos = (TUV)m_Heap.size();
m_Heap.push_back(v);
percolate_up(m_PosScore[v].m_Pos);
}
}
void rebuild()
{
m_Heap.reserve_exactly(m_PosScore.cap());
m_Heap.clear();
m_Heap.emplace_back(0);
for (TUVar v = 1; v < m_PosScore.cap(); ++v)
{
if (in_heap(v))
{
m_PosScore[v].m_Pos = 0;
assert(!in_heap(v));
insert(v, m_PosScore[v].m_Score);
assert(in_heap(v));
}
}
}
void insert(TUVar v, double score)
{
if (v >= m_PosScore.cap())
{
m_PosScore.reserve_atleast(v + 1, (size_t)0);
m_Heap.reserve_atleast(v + 1);
if (uninitialized_or_erroneous())
{
return;
}
}
assert(!in_heap(v));
m_PosScore[v] = TPosScore((TUV)m_Heap.size(), score);
m_Heap.push_back(v);
percolate_up(m_PosScore[v].m_Pos);
}
TUVar remove_min()
{
auto v = m_Heap[1];
swap(m_Heap[1], m_Heap.back());
m_PosScore[m_Heap[1]].m_Pos = 1;
m_PosScore[v].m_Pos = 0;
m_Heap.pop_back();
if (m_Heap.size() > 2)
{
percolate_down(1);
}
return v;
}
inline TUVar get_min() const
{
return m_Heap[1];
}
inline bool var_score_exists(TUVar v) const { return v < m_PosScore.cap(); }
inline double get_var_score(TUVar v) const { return m_PosScore[v].m_Score; }
// Use set_var_score only if rebuild is surely scheduled soon, otherwise it will botch the data structure!
inline void set_var_score(TUVar v, double newScore) { m_PosScore[v].m_Score = newScore; }
inline void var_inc_update(double varDecay) { m_VarActivityInc *= (1. / varDecay); }
inline void set_multiplier(double multiplier) { m_PosScore.SetMultiplier(multiplier); m_Heap.SetMultiplier(multiplier); }
inline void replace_pos_score_vars(TUVar vFrom, TUVar vTo) { m_PosScore[vTo] = move(m_PosScore[vFrom]); }
inline size_t memMb() const { return m_Activity.memMb() + m_Heap.memMb() + m_PosScore.memMb(); }
protected:
// The activity
CVector<double> m_Activity;
double& m_VarActivityInc;
// This variable allows one to simulate the two different insertion orders:
// false: bigger variable indices first; true: smaller variable indices first (default)
// We do the simulation by providing two implementations of the "better" predicate (see below)
// See the parameter m_ParamVsidsInitOrder for more details
bool m_InitOrder = false;
// Heap of variables
CVector<TUVar> m_Heap;
// TPosScore: 1) position in the heap (0 means not in the heap); 2) score
struct TPosScore
{
TPosScore(TUV pos, double score) : m_Pos(pos), m_Score(score) {}
TUV m_Pos;
double m_Score;
};
// Variable-indexed array: position & score per variable
CDynArray<TPosScore> m_PosScore;
// Index "traversal" functions
static constexpr TUV left(TUV i) { return i << 1; };
static constexpr TUV right(TUV i) { return (i << 1) + 1; };
static constexpr TUV parent(TUV i) { return i >> 1; };
// Cannot put the static asserts in the class itself, since it's forbidden by C++ standard
// as the functions are undefined inside the class
void static_assert_traversal()
{
static_assert(parent(2) == 1);
static_assert(parent(3) == 1);
static_assert(left(1) == 2);
static_assert(right(1) == 3);
static_assert(parent(4) == 2);
static_assert(parent(5) == 2);
static_assert(left(2) == 4);
static_assert(right(2) == 5);
static_assert(parent(6) == 3);
static_assert(parent(7) == 3);
static_assert(left(3) == 6);
static_assert(right(3) == 7);
}
void percolate_up(TUV i)
{
const TUVar v = m_Heap[i];
TUV p = parent(i);
while (i != 1 && better(v, m_Heap[p]))
{
m_Heap[i] = m_Heap[p];
m_PosScore[m_Heap[p]].m_Pos = i;
i = p;
p = parent(p);
}
m_Heap[i] = v;
m_PosScore[v].m_Pos = i;
}
void percolate_down(TUV i)
{
TUVar v = m_Heap[i];
while (left(i) < m_Heap.size())
{
auto child = right(i) < m_Heap.size() &&
better(m_Heap[right(i)], m_Heap[left(i)]) ? right(i) : left(i);
if (!better(m_Heap[child], v)) break;
m_Heap[i] = m_Heap[child];
m_PosScore[m_Heap[i]].m_Pos = i;
i = child;
}
m_Heap[i] = v;
m_PosScore[v].m_Pos = i;
}
inline bool better(TUVar v1, TUVar v2) const { return m_InitOrder ? m_PosScore[v1].m_Score > m_PosScore[v2].m_Score : m_PosScore[v1].m_Score >= m_PosScore[v2].m_Score; }
};
}