From 09e3980b20fb8f1321611ccf941e3420dc36b08f Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 21 Mar 2022 17:46:40 +0100 Subject: [PATCH] Adding VSIDS variable picking, restarts, and polarity caching --- libsolutil/CDCL.cpp | 72 ++++++++++++--- libsolutil/CDCL.h | 45 ++++++++- libsolutil/heap.h | 220 ++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 322 insertions(+), 15 deletions(-) create mode 100644 libsolutil/heap.h diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp index d58224247..a4021b7a1 100644 --- a/libsolutil/CDCL.cpp +++ b/libsolutil/CDCL.cpp @@ -35,7 +35,8 @@ CDCL::CDCL( std::function(std::map const&)> _theorySolver ): m_theorySolver(_theorySolver), - m_variables(move(_variables)) + m_variables(move(_variables)), + order(VarOrderLt(activity)) { for (Clause const& clause: _clauses) addClause(clause); @@ -45,11 +46,25 @@ CDCL::CDCL( optional CDCL::solve() { -// cout << "====" << endl; -// for (unique_ptr const& c: m_clauses) -// cout << toString(*c) << endl; -// cout << "====" << endl; - while (true) + CDCL::Model model; + int solution; + uint32_t max_conflicts = 100; + bool solved = false; + while(!solved) { + solution = 3; + solved = solve_loop(max_conflicts, model, solution); + max_conflicts = uint32_t((double)max_conflicts * 1.2); + } + assert(solution != 3); + if (solution) return model; + else return nullopt; +} + +bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& solution) +{ + assert (max_conflicts > 0); + uint32_t conflicts = 0; + while (conflicts < max_conflicts) { optional conflictClause = propagate(); if (!conflictClause && m_theorySolver) @@ -60,10 +75,12 @@ optional CDCL::solve() } if (conflictClause) { + conflicts++; if (currentDecisionLevel() == 0) { // cout << "Unsatisfiable" << endl; - return nullopt; + solution = 0; + return true; } auto&& [learntClause, backtrackLevel] = analyze(move(*conflictClause)); cancelUntil(backtrackLevel); @@ -83,17 +100,25 @@ optional CDCL::solve() cout << ((m_assignments.size() * 100) / m_variables.size()) << "% of variables assigned." << endl; m_decisionPoints.emplace_back(m_assignmentTrail.size()); // cout << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl; - enqueue(Literal{false, *variable}, nullptr); + + // Polarity caching below + bool positive = false; + auto const& found = m_assignments_cache.find(*variable); + if (found != m_assignments_cache.end()) positive = found->second; + enqueue(Literal{positive, *variable}, nullptr); } else { //cout << "satisfiable." << endl; //for (auto&& [i, value]: m_assignments | ranges::view::enumerate()) // cout << " " << m_variables.at(i) << ": " << value.toString() << endl; - return m_assignments; + solution = 1; + model = m_assignments; + return true; } } } + return false; } void CDCL::setupWatches(Clause& _clause) @@ -200,6 +225,7 @@ std::pair CDCL::analyze(Clause _conflictClause) else { //cout << " adding " << toString(literal) << " @" << variableLevel << " to learnt clause." << endl; + vsids_bump_var_act((uint32_t)literal.variable); learntClause.push_back(literal); backtrackLevel = max(backtrackLevel, variableLevel); } @@ -234,6 +260,19 @@ std::pair CDCL::analyze(Clause _conflictClause) void CDCL::addClause(Clause _clause) { + uint64_t max_var = (uint32_t)activity.size(); + uint64_t new_max_var = 0; + for(auto const& l: _clause) { + new_max_var = std::max(l.variable+1, max_var); + } + int64_t to_add = (int64_t)new_max_var - (int64_t)max_var; + if (to_add > 0) { + activity.insert(activity.end(), (uint64_t)to_add, 0.0); + } + for(auto const& l: _clause) { + if (!order.inHeap((int)l.variable)) order.insert((int)l.variable); + } + m_clauses.push_back(make_unique(move(_clause))); setupWatches(*m_clauses.back()); } @@ -248,8 +287,10 @@ void CDCL::enqueue(Literal const& _literal, Clause const* _reason) // TODO assert that assignmnets was unknown m_assignments[_literal.variable] = _literal.positive; m_levelForVariable[_literal.variable] = currentDecisionLevel(); - if (_reason) + if (_reason) { m_reason[_literal] = _reason; + m_assignments_cache[_literal.variable] = _literal.positive; + } m_assignmentTrail.push_back(_literal); } @@ -268,17 +309,20 @@ void CDCL::cancelUntil(size_t _backtrackLevel) m_reason.erase(l); // TODO maybe could do without. m_levelForVariable.erase(l.variable); + order.insert((int)l.variable); } m_decisionPoints.resize(_backtrackLevel); m_assignmentQueuePointer = m_assignmentTrail.size(); solAssert(currentDecisionLevel() == _backtrackLevel); } -optional CDCL::nextDecisionVariable() const +optional CDCL::nextDecisionVariable() { - for (size_t i = 0; i < m_variables.size(); i++) - if (!m_assignments.count(i)) - return i; + while(true) { + if (order.empty()) return nullopt; + size_t i = (size_t)order.removeMin(); + if (!m_assignments.count(i)) return i; + } return nullopt; } diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h index bc0118c58..289bd51bc 100644 --- a/libsolutil/CDCL.h +++ b/libsolutil/CDCL.h @@ -24,6 +24,7 @@ #include #include #include +#include "heap.h" namespace solidity::util { @@ -64,6 +65,20 @@ public: std::optional solve(); private: + struct VarOrderLt { ///Order variables according to their activities + const std::vector& activities; + bool operator () (const int x, const int y) const + { + return activities[(size_t)x] > activities[(size_t)y]; + } + + explicit VarOrderLt(const std::vector& _activities) : + activities(_activities) + {} + }; + + + bool solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& solution); void setupWatches(Clause& _clause); std::optional propagate(); std::pair analyze(Clause _conflictClause); @@ -75,7 +90,7 @@ private: void cancelUntil(size_t _backtrackLevel); - std::optional nextDecisionVariable() const; + std::optional nextDecisionVariable(); bool isAssigned(Literal const& _literal) const; bool isAssignedTrue(Literal const& _literal) const; @@ -103,10 +118,38 @@ private: /// Current assignments. std::map m_assignments; + std::map m_assignments_cache; // Polarity caching. All propagated values end up here std::map m_levelForVariable; /// TODO wolud be good to not have to copy the clauses std::map m_reason; + // Var activity + Heap order; + std::vector activity; + double var_inc_vsids = 1; + double var_decay = 0.95; + void vsids_decay_var_act() + { + var_inc_vsids *= (1.0 / var_decay); + } + void vsids_bump_var_act(uint32_t var) + { + assert(activity.size() > var); + activity[var] += var_inc_vsids; + + bool rescaled = false; + if (activity[var] > 1e100) { + // Rescale + for (auto& a: activity) a *= 1e-100; + rescaled = true; + var_inc_vsids *= 1e-100; + } + + // Update order_heap with respect to new activity: + if (order.inHeap((int)var)) order.decrease((int)var); + if (rescaled) assert(order.heap_property()); + } + // TODO group those into a class std::vector m_assignmentTrail; diff --git a/libsolutil/heap.h b/libsolutil/heap.h new file mode 100644 index 000000000..000077ce0 --- /dev/null +++ b/libsolutil/heap.h @@ -0,0 +1,220 @@ +/******************************************************************************************[Heap.h] +Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Glucose_Heap_h +#define Glucose_Heap_h + +#include +#include +#include + +//================================================================================================= +// A heap implementation with support for decrease/increase key. + + +template +class Heap { + Comp lt; // The heap is a minimum-heap with respect to this comparator + std::vector heap; // Heap of integers + std::vector indices; // Each integers position (index) in the Heap + + // Index "traversal" functions + static inline int left (int i) + { + return i * 2 + 1; + } + static inline int right (int i) + { + return (i + 1) * 2; + } + static inline int parent(int i) + { + return (i - 1) >> 1; + } + + + void percolateUp(int i) + { + int x = heap[(size_t)i]; + int p = parent(i); + + while (i != 0 && lt(x, heap[(size_t)p])) { + heap[(size_t)i] = heap[(size_t)p]; + indices[(size_t)heap[(size_t)p]] = i; + i = p; + p = parent(p); + } + heap [(size_t)i] = x; + indices[(size_t)x] = i; + } + + + void percolateDown(int i) + { + int x = heap[(size_t)i]; + while (left(i) < (int)heap.size()) { + int child = right(i) < (int)heap.size() && lt(heap[(size_t)right(i)], heap[(size_t)left(i)]) ? right(i) : left(i); + if (!lt(heap[(size_t)child], x)) { + break; + } + heap[(size_t)i] = heap[(size_t)child]; + indices[(size_t)heap[(size_t)i]] = i; + i = child; + } + heap [(size_t)i] = x; + indices[(size_t)x] = i; + } + + +public: + Heap(const Comp& c) : lt(c) { } + + void print_heap() { + std::cout << "heap:"; + for(auto x: heap) { + std::cout << x << " "; + } + std::cout << std::endl; + + std::cout << "ind:"; + for(auto x: indices) { + std::cout << x << " "; + } + std::cout << std::endl; + } + + uint32_t size () const + { + return heap.size(); + } + bool empty () const + { + return heap.size() == 0; + } + bool inHeap (int n) const + { + return n < (int)indices.size() && indices[(size_t)n] >= 0; + } + int operator[](int index) const + { + assert(index < (int)heap.size()); + return heap[index]; + } + + void decrease (int n) + { + assert(inHeap(n)); + percolateUp (indices[(size_t)n]); + } + void increase (int n) + { + assert(inHeap(n)); + percolateDown(indices[n]); + } + + + // Safe variant of insert/decrease/increase: + void update(int n) + { + if (!inHeap(n)) { + insert(n); + } else { + percolateUp(indices[n]); + percolateDown(indices[n]); + } + } + + + void insert(int n) + { + indices.resize((size_t)n + 1, -1); + assert(!inHeap(n)); + + indices[(size_t)n] = (int)heap.size(); + heap.push_back(n); + percolateUp(indices[(size_t)n]); + } + + + int removeMin() + { + int x = heap[0]; + heap[0] = (int)heap.back(); + indices[(size_t)heap[0]] = 0; + indices[(size_t)x] = -1; + heap.pop_back(); + if (heap.size() > 1) { + percolateDown(0); + } + return x; + } + + + // Rebuild the heap from scratch, using the elements in 'ns': + template + void build(const T& ns) + { + for (int i = 0; i < (int)heap.size(); i++) { + indices[heap[i]] = -1; + } + heap.clear(); + + for (uint32_t i = 0; i < ns.size(); i++) { + indices[ns[i]] = i; + heap.push_back(ns[i]); + } + + for (int i = (int)heap.size() / 2 - 1; i >= 0; i--) { + percolateDown(i); + } + } + + void clear(bool dealloc = false) + { + for (int i = 0; i < (int)heap.size(); i++) { + indices[heap[i]] = -1; + } + heap.clear(); + } + + size_t mem_used() const + { + size_t mem = 0; + mem += heap.capacity()*sizeof(uint32_t); + mem += indices.capacity()*sizeof(uint32_t); + return mem; + } + + bool heap_property (uint32_t i) const { + return i >= heap.size() + || ( (i == 0 || !lt(heap[i], heap[(size_t)parent((int)i)])) + && heap_property( (uint32_t)left((int)i) ) + && heap_property( (uint32_t)right((int)i) ) + ); + } + + bool heap_property() const { + return heap_property(0); + } + +}; + + +#endif