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
TopiGlobal.hpp
// Copyright(C) 2021-2022 Intel Corporation
// SPDX - License - Identifier: MIT
#pragma once
#include <bit>
// Defining likely/unlikely for helping branch prediction.
// Will replace by C++20's [[likely]]/[[unlikely]] attributes, once properly and consistently implemented in both GCC and VS
#ifdef _WIN32
#define likely(x) (x)
#define unlikely(x) (x)
#else
#define likely(x) __builtin_expect((x),1)
#define unlikely(x) __builtin_expect((x),0)
#endif
using namespace std;
namespace Topor
{
enum class TToporStatus : uint8_t
{
// Status unknown
STATUS_UNDECIDED,
// The latest invocation had returned SAT and no clauses contradicting the model were introduced since
STATUS_SAT,
// The latest invocation returned UNSAT, but this status might be temporary (under assumptions)
STATUS_UNSAT,
// The latest invocation returned USER_INTERRUPT
STATUS_USER_INTERRUPT,
/*
* Only unrecoverable status values below
*/
STATUS_FIRST_UNRECOVERABLE,
// The instance is forever contradictory.
STATUS_CONTRADICTORY = STATUS_FIRST_UNRECOVERABLE,
/*
* Only permanently erroneous values below
*/
STATUS_FIRST_PERMANENT_ERROR,
// The instance is in memory-out state, meaning that one of the allocations fails.
STATUS_ALLOC_FAILED = STATUS_FIRST_PERMANENT_ERROR,
// Data doesn't fit into the buffer
STATUS_INDEX_TOO_NARROW,
// Parameter-related error
STATUS_PARAM_ERROR,
// Error while processing assumption-required queries
STATUS_ASSUMPTION_REQUIRED_ERROR,
// Global timeout reached
STATUS_GLOBAL_TIMEOUT,
// Problem when trying to access/write the DRAT file
STATUS_DRAT_FILE_PROBLEM,
// So-far: cannot accommodate the last possible variable if sizeof(TLit) == sizeof(size_t), since the allocation will fail
STATUS_EXOTIC_ERROR
};
// The TLit type, representing the external literals, unsigned
// Will be used for storing internal literals, whose sign is determined by the LSB, rather than the MSB
using TULit = make_unsigned<TLit>::type;
static_assert(numeric_limits<TULit>::digits == numeric_limits<TLit>::digits + 1);
// Bad literal
TULit static constexpr BadULit = 0;
// TUL is used to hold unsigned integers, whose number is not greater than that of the literaks; used only for code clarity
using TUL = TULit;
// TUVar is used to hold variables; used only for code clarity
using TUVar = TULit;
// TUV is used to hold unsigned integers, whose number is not greater than that of the variables; used only for code clarity
using TUV = TUVar;
// Bad variable
TULit static constexpr BadUVar = 0;
TUVar static constexpr GetVar(TULit l) { return l >> 1; }
static_assert(GetVar(0b1001) == 0b100 && GetVar(0b1000) == 0b100);
TULit static constexpr GetLit(TUVar v, bool isNegative) { return (v << 1) + (TULit)isNegative; }
static_assert(GetLit(0b100, true) == 0b1001 && GetLit(0b100, false) == 0b1000);
TULit static constexpr GetFirstLit() { return GetLit(1, false); }
static_assert(GetFirstLit() == 2);
bool static constexpr IsPos(TULit l) { return (l & 1) == 0; }
static_assert(IsPos(0b1000));
bool static constexpr IsNeg(TULit l) { return (bool)(l & 1); }
static_assert(IsNeg(0b1001));
TULit static constexpr Negate(TULit l) { return l ^ 1; }
static_assert(Negate(0b1001) == 0b1000 && Negate(0b1000) == 0b1001);
TULit static constexpr GetMaxLit(TULit l) { return IsNeg(l) ? l : Negate(l); }
static_assert(GetMaxLit(0b1001) == 0b1001 && GetMaxLit(0b1000) == 0b1001);
// Initialization-related: the initial number of entries in the fused buffer: set the original size to 4Mb
static constexpr size_t InitEntriesInB = 0x400000 / sizeof(TULit);
// The assumed number of bytes in one page
static constexpr size_t BytesInPage = 64;
static_assert(has_single_bit(BytesInPage));
// The number of literals in one page; relevant for watch allocation
static constexpr size_t LitsInPage = BytesInPage / sizeof(TULit);
static_assert(has_single_bit(LitsInPage));
// Make sure that, initially, we allocate a sufficient number of entries in the buffer to accommodate LitsInPage literals
static_assert(LitsInPage <= InitEntriesInB);
// counter type for discovering duplicates, tautologies, contradictions etc., e.g., in incoming clauses and assumptions
// In the context of handling new clauses,
// we did some tests and found that int32_t for the counter works better than int64_t, int16_t (both are 2x slower) and int8_t (significantly slower)
// We also tested options using bit-arrays CBitArray<2> and CBitArrayAligned<2> with memset-0 after each clause,
// but the former is much slower than the current implementation, while the latter is impossibly slow.
typedef int32_t TCounterType;
static_assert(is_signed<TCounterType>::value);
// Bad parent clause index
TUInd static constexpr BadClsInd = 0;
template<class ForwardIt, class UnaryPredicate>
ForwardIt move_if(ForwardIt first, ForwardIt last, UnaryPredicate p)
{
first = std::find_if(first, last, p);
if (first != last)
for (ForwardIt i = first; ++i != last; )
if (!p(*i))
{
//*first++ = std::move(*i);
swap(*first, *i);
first++;
}
return first;
}
}