Adding VSIDS variable picking, restarts, and polarity caching

libsolutil/CDCL.cpp

@@ -35,7 +35,8 @@ CDCL::CDCL(
 	std::function<std::optional<Clause>(std::map<size_t, bool> 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::Model> CDCL::solve()
 {
-//	cout << "====" << endl;
+	CDCL::Model model;
-//	for (unique_ptr<Clause> const& c: m_clauses)
+	int solution;
-//		cout << toString(*c) << endl;
+	uint32_t max_conflicts = 100;
-//	cout << "====" << endl;
+	bool solved = false;
-	while (true)
+	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<Clause> conflictClause = propagate();
 		if (!conflictClause && m_theorySolver)
@@ -60,10 +75,12 @@ optional<CDCL::Model> 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::Model> 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<Clause, size_t> 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<Clause, size_t> 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<uint64_t>(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<Clause>(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<size_t> CDCL::nextDecisionVariable() const
+optional<size_t> CDCL::nextDecisionVariable()
 {
-	for (size_t i = 0; i < m_variables.size(); i++)
+	while(true) {
-		if (!m_assignments.count(i))
+		if (order.empty()) return nullopt;
-			return i;
+		size_t i = (size_t)order.removeMin();
+		if (!m_assignments.count(i)) return i;
+	}
 	return nullopt;
 }
 

libsolutil/CDCL.h

@@ -24,6 +24,7 @@
 #include <functional>
 #include <memory>
 #include <optional>
+#include "heap.h"
 
 namespace solidity::util
 {
@@ -64,6 +65,20 @@ public:
 	std::optional<Model> solve();
 
 private:
+	struct VarOrderLt { ///Order variables according to their activities
+        const std::vector<double>&  activities;
+        bool operator () (const int x, const int y) const
+        {
+            return activities[(size_t)x] > activities[(size_t)y];
+        }
+
+        explicit VarOrderLt(const std::vector<double>& _activities) :
+            activities(_activities)
+        {}
+    };
+
+
+	bool solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& solution);
 	void setupWatches(Clause& _clause);
 	std::optional<Clause> propagate();
 	std::pair<Clause, size_t> analyze(Clause _conflictClause);
@@ -75,7 +90,7 @@ private:
 
 	void cancelUntil(size_t _backtrackLevel);
 
-	std::optional<size_t> nextDecisionVariable() const;
+	std::optional<size_t> nextDecisionVariable();
 
 	bool isAssigned(Literal const& _literal) const;
 	bool isAssignedTrue(Literal const& _literal) const;
@@ -103,10 +118,38 @@ private:
 
 	/// Current assignments.
 	std::map<size_t, bool> m_assignments;
+	std::map<size_t, bool> m_assignments_cache; // Polarity caching. All propagated values end up here
 	std::map<size_t, size_t> m_levelForVariable;
 	/// TODO wolud be good to not have to copy the clauses
 	std::map<Literal, Clause const*> m_reason;
 
+	// Var activity
+	Heap<VarOrderLt> order;
+	std::vector<double> 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<Literal> m_assignmentTrail;

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 <vector>
+#include <cassert>
+#include <iostream>
+
+//=================================================================================================
+// A heap implementation with support for decrease/increase key.
+
+
+template<class Comp>
+class Heap {
+    Comp     lt;       // The heap is a minimum-heap with respect to this comparator
+    std::vector<int> heap;     // Heap of integers
+    std::vector<int> 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<typename T>
+    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