cdcl

libsolutil/CDCL.cpp

@@ -0,0 +1,322 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolutil/CDCL.h>
+
+#include <liblangutil/Exceptions.h>
+
+// TODO remove before merge
+#include <iostream>
+#include <libsolutil/StringUtils.h>
+
+using namespace std;
+using namespace solidity;
+using namespace solidity::util;
+
+
+CDCL::CDCL(
+	vector<string> _variables,
+	vector<Clause> const& _clauses,
+	std::function<std::optional<Clause>(std::map<size_t, bool> const&)> _theorySolver
+):
+	m_theorySolver(_theorySolver),
+	m_variables(move(_variables))
+{
+	for (Clause const& clause: _clauses)
+		addClause(clause);
+
+	// TODO some sanity checks like no empty clauses, no duplicate literals?
+}
+
+optional<CDCL::Model> CDCL::solve()
+{
+	cout << "====" << endl;
+	for (unique_ptr<Clause> const& c: m_clauses)
+		cout << toString(*c) << endl;
+	cout << "====" << endl;
+	while (true)
+	{
+		optional<Clause> conflictClause = propagate();
+		if (!conflictClause && m_theorySolver)
+		{
+			conflictClause = m_theorySolver(m_assignments);
+			if (conflictClause)
+				cout << "Theory gave us conflict: " << toString(*conflictClause) << endl;
+		}
+		if (conflictClause)
+		{
+			if (currentDecisionLevel() == 0)
+			{
+				cout << "Unsatisfiable" << endl;
+				return nullopt;
+			}
+			auto&& [learntClause, backtrackLevel] = analyze(move(*conflictClause));
+			cancelUntil(backtrackLevel);
+			solAssert(!learntClause.empty());
+			solAssert(!isAssigned(learntClause.front()));
+			for (size_t i = 1; i < learntClause.size(); i++)
+				solAssert(isAssignedFalse(learntClause.at(i)));
+
+			addClause(move(learntClause));
+			enqueue(m_clauses.back()->front(), &(*m_clauses.back()));
+		}
+		else
+		{
+			if (auto variable = nextDecisionVariable())
+			{
+				m_decisionPoints.emplace_back(m_assignmentTrail.size());
+				cout << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl;
+				enqueue(Literal{false, *variable}, nullptr);
+			}
+			else
+			{
+				cout << "satisfiable." << endl;
+				for (auto&& [var, value]: m_assignments)
+					cout << " " << m_variables.at(var) << ": " << (value ? "true" : "false") << endl;
+				return m_assignments;
+			}
+		}
+	}
+}
+
+void CDCL::setupWatches(Clause& _clause)
+{
+	for (size_t i = 0; i < min<size_t>(2, _clause.size()); i++)
+		m_watches[_clause.at(i)].push_back(&_clause);
+}
+
+optional<Clause> CDCL::propagate()
+{
+	cout << "Propagating." << endl;
+	for (; m_assignmentQueuePointer < m_assignmentTrail.size(); m_assignmentQueuePointer++)
+	{
+		Literal toPropagate = m_assignmentTrail.at(m_assignmentQueuePointer);
+		Literal falseLiteral = ~toPropagate;
+		cout << "Propagating " << toString(toPropagate) << endl;
+		// Go through all watched clauses where this assignment makes the literal false.
+		vector<Clause*> watchReplacement;
+		auto it = m_watches[falseLiteral].begin();
+		auto end = m_watches[falseLiteral].end();
+		for (; it != end; ++it)
+		{
+			Clause& clause = **it;
+			cout << " watch clause: " << toString(clause) << endl;
+
+			solAssert(!clause.empty());
+			if (clause.front() != falseLiteral)
+				swap(clause[0], clause[1]);
+			solAssert(clause.front() == falseLiteral);
+			if (clause.size() >= 2 && isAssignedTrue(clause[1]))
+			{
+				// Clause is already satisfied, keezp the watch.
+				cout << " -> already satisfied by " << toString(clause[1]) << endl;
+				watchReplacement.emplace_back(&clause);
+				continue;
+			}
+
+			// find a new watch to swap
+			for (size_t i = 2; i < clause.size(); i++)
+				if (isUnknownOrAssignedTrue(clause[i]))
+				{
+					cout << " -> swapping " << toString(clause.front()) << " with " << toString(clause[i]) << endl;
+					swap(clause.front(), clause[i]);
+					m_watches[clause.front()].emplace_back(&clause);
+					break;
+				}
+			if (clause.front() != falseLiteral)
+				continue; // we found a new watch
+
+			// We did not find a new watch, i.e. all literals starting from index 2
+			// are false, thus clause[1] has to be true (if it exists)
+			if (clause.size() == 1 || isAssignedFalse(clause[1]))
+			{
+				if (clause.size() >= 2)
+					cout << " - Propagate resulted in conflict because " << toString(clause[1]) << " is also false." << endl;
+				else
+					cout << " - Propagate resulted in conflict since clause is single-literal." << endl;
+				// Copy over the remaining watches and replace.
+				while (it != end) watchReplacement.emplace_back(move(*it++));
+				m_watches[falseLiteral] = move(watchReplacement);
+				// Mark the queue as finished.
+				m_assignmentQueuePointer = m_assignmentTrail.size();
+				return clause;
+			}
+			else
+			{
+				cout << " - resulted in new assignment: " << toString(clause[1]) << endl;
+				watchReplacement.emplace_back(&clause);
+				enqueue(clause[1], &clause);
+			}
+		}
+		m_watches[falseLiteral] = move(watchReplacement);
+	}
+	return nullopt;
+}
+
+
+std::pair<Clause, size_t> CDCL::analyze(Clause _conflictClause)
+{
+	solAssert(!_conflictClause.empty());
+	cout << "Analyzing conflict." << endl;
+	Clause learntClause;
+	size_t backtrackLevel = 0;
+
+	set<size_t> seenVariables;
+
+	int pathCount = 0;
+	size_t trailIndex = m_assignmentTrail.size() - 1;
+	optional<Literal> resolvingLiteral;
+	do
+	{
+		cout << " conflict clause: " << toString(_conflictClause) << endl;
+		for (Literal literal: _conflictClause)
+			if ((!resolvingLiteral || literal != *resolvingLiteral) && !seenVariables.count(literal.variable))
+			{
+				seenVariables.insert(literal.variable);
+				size_t variableLevel = m_levelForVariable.at(literal.variable);
+				if (variableLevel == currentDecisionLevel())
+				{
+					cout << "    ignoring " << toString(literal) << " at current decision level." << endl;
+					// ignore variable, we will apply resolution with its reason.
+					pathCount++;
+				}
+				else
+				{
+					cout << "    adding " << toString(literal) << " @" << variableLevel << " to learnt clause." << endl;
+					learntClause.push_back(literal);
+					backtrackLevel = max(backtrackLevel, variableLevel);
+				}
+			}
+			else
+				cout << "    already seen " << toString(literal) << endl;
+
+		solAssert(pathCount > 0);
+		pathCount--;
+		while (!seenVariables.count(m_assignmentTrail[trailIndex--].variable));
+		resolvingLiteral = m_assignmentTrail[trailIndex + 1];
+		cout << "  resolving literal: " << toString(*resolvingLiteral) << endl;
+		seenVariables.erase(resolvingLiteral->variable);
+		// TODO Is there always a reason? Not if it's a decision variable.
+		if (pathCount > 0)
+		{
+			_conflictClause = *m_reason.at(*resolvingLiteral);
+			cout << "  reason: " << toString(_conflictClause) << endl;
+		}
+	}
+	while (pathCount > 0);
+	solAssert(resolvingLiteral);
+	learntClause.push_back(~(*resolvingLiteral));
+	// Move to front so we can directly propagate.
+	swap(learntClause.front(), learntClause.back());
+
+	cout << "-> learnt clause: " << toString(learntClause) << " backtrack to " << backtrackLevel << endl;
+
+
+	return {move(learntClause), backtrackLevel};
+}
+
+void CDCL::addClause(Clause _clause)
+{
+	m_clauses.push_back(make_unique<Clause>(move(_clause)));
+	setupWatches(*m_clauses.back());
+}
+
+void CDCL::enqueue(Literal const& _literal, Clause const* _reason)
+{
+	cout << "Enqueueing " << toString(_literal) << " @" << currentDecisionLevel() << endl;
+	if (_reason)
+		cout << "  because of " << toString(*_reason) << endl;
+	// TODO assert that assignmnets was unknown
+	m_assignments[_literal.variable] = _literal.positive;
+	m_levelForVariable[_literal.variable] = currentDecisionLevel();
+	if (_reason)
+		m_reason[_literal] = _reason;
+	m_assignmentTrail.push_back(_literal);
+}
+
+void CDCL::cancelUntil(size_t _backtrackLevel)
+{
+	// TODO what if we backtrack to zero?
+	cout << "Canceling until " << _backtrackLevel << endl;
+	solAssert(m_assignmentQueuePointer == m_assignmentTrail.size());
+	size_t assignmentsToUndo = m_assignmentTrail.size() - m_decisionPoints.at(_backtrackLevel);
+	for (size_t i = 0; i < assignmentsToUndo; i++)
+	{
+		Literal l = m_assignmentTrail.back();
+		cout << "  undoing " << toString(l) << endl;
+		m_assignmentTrail.pop_back();
+		m_assignments.erase(l.variable);
+		m_reason.erase(l);
+		// TODO maybe could do without.
+		m_levelForVariable.erase(l.variable);
+	}
+	m_decisionPoints.resize(_backtrackLevel);
+	m_assignmentQueuePointer = m_assignmentTrail.size();
+	solAssert(currentDecisionLevel() == _backtrackLevel);
+}
+
+optional<size_t> CDCL::nextDecisionVariable() const
+{
+	for (size_t i = 0; i < m_variables.size(); i++)
+		if (!m_assignments.count(i))
+			return i;
+	return nullopt;
+}
+
+bool CDCL::isAssigned(Literal const& _literal) const
+{
+	return m_assignments.count(_literal.variable);
+}
+
+bool CDCL::isAssignedTrue(Literal const& _literal) const
+{
+	return (
+		m_assignments.count(_literal.variable) &&
+		m_assignments.at(_literal.variable) == _literal.positive
+	);
+}
+
+bool CDCL::isAssignedFalse(Literal const& _literal) const
+{
+	return (
+		m_assignments.count(_literal.variable) &&
+		!m_assignments.at(_literal.variable) == _literal.positive
+	);
+}
+
+bool CDCL::isUnknownOrAssignedTrue(Literal const& _literal) const
+{
+	return (
+		!m_assignments.count(_literal.variable) ||
+		m_assignments.at(_literal.variable) == _literal.positive
+	);
+}
+
+string CDCL::toString(Literal const& _literal) const
+{
+	return (_literal.positive ? "" : "~") + m_variables.at(_literal.variable);
+}
+
+string CDCL::toString(Clause const& _clause) const
+{
+	vector<string> literals;
+	for (Literal const& l: _clause)
+		literals.emplace_back(toString(l));
+	return "(" + joinHumanReadable(literals) + ")";
+}
+

libsolutil/CDCL.h

@@ -0,0 +1,119 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+#pragma once
+
+#include <vector>
+#include <tuple>
+#include <map>
+#include <string>
+#include <functional>
+#include <memory>
+#include <optional>
+
+namespace solidity::util
+{
+
+/**
+ * A literal of a (potentially negated) boolean variable or an inactive constraint.
+ */
+struct Literal
+{
+	bool positive;
+	// Either points to a boolean variable or to a constraint.
+	size_t variable{0};
+
+	Literal operator~() const { return Literal{!positive, variable}; }
+	bool operator==(Literal const& _other) const
+	{
+			return std::make_tuple(positive, variable) == std::make_tuple(_other.positive, _other.variable);
+	}
+	bool operator!=(Literal const& _other) const { return !(*this == _other); }
+	bool operator<(Literal const& _other) const
+	{
+		return std::make_tuple(positive, variable) < std::make_tuple(_other.positive, _other.variable);
+	}
+};
+using Clause = std::vector<Literal>;
+
+class CDCL
+{
+public:
+	using Model = std::map<size_t, bool>;
+	CDCL(
+		std::vector<std::string> _variables,
+		std::vector<Clause> const& _clauses,
+		std::function<std::optional<Clause>(std::map<size_t, bool> const&)> _theoryPropagator = {}
+	);
+
+	std::optional<Model> solve();
+
+private:
+	void setupWatches(Clause& _clause);
+	std::optional<Clause> propagate();
+	std::pair<Clause, size_t> analyze(Clause _conflictClause);
+	size_t currentDecisionLevel() const { return m_decisionPoints.size(); }
+
+	void addClause(Clause _clause);
+
+	void enqueue(Literal const& _literal, Clause const* _reason);
+
+	void cancelUntil(size_t _backtrackLevel);
+
+	std::optional<size_t> nextDecisionVariable() const;
+
+	bool isAssigned(Literal const& _literal) const;
+	bool isAssignedTrue(Literal const& _literal) const;
+	bool isAssignedFalse(Literal const& _literal) const;
+	bool isUnknownOrAssignedTrue(Literal const& _literal) const;
+
+	std::string toString(Literal const& _literal) const;
+	std::string toString(Clause const& _clause) const;
+
+	/// Callback that receives an assignment and uses the theory to either returns nullopt ("satisfiable")
+	/// or a conflict clause, i.e. a clauses that is false in the theory with the given assignments.
+	std::function<std::optional<Clause>(std::map<size_t, bool>)> m_theorySolver;
+
+	std::vector<std::string> m_variables;
+	/// includes the learnt clauses
+	std::vector<std::unique_ptr<Clause>> m_clauses;
+
+	/// During the execution of the algorithm, the clauses are madified to ensure that:
+	/// The first two literals are either true or unknown.
+	/// Those two literals are called "watched literals".
+	/// This map contains the reverse pointers from the literals.
+	/// The idea is that these two literals suffice to know if a clause is unsatisfied
+	/// (it might be satisfied without us knowing, but that is not bad).
+	std::map<Literal, std::vector<Clause*>> m_watches;
+
+	/// Current assignments.
+	std::map<size_t, bool> m_assignments;
+	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;
+
+	// TODO group those into a class
+
+	std::vector<Literal> m_assignmentTrail;
+	/// Indices into assignmentTrail where decisions were taken.
+	std::vector<size_t> m_decisionPoints;
+	/// Index into assignmentTrail: All assignments starting there have not yet been propagated.
+	size_t m_assignmentQueuePointer = 0;
+};
+
+
+}

libsolutil/CMakeLists.txt

@@ -2,6 +2,8 @@ set(sources
 	Algorithms.h
 	AnsiColorized.h
 	Assertions.h
+	CDCL.h
+	CDCL.cpp
 	Common.h
 	CommonData.cpp
 	CommonData.h

test/CMakeLists.txt

@@ -31,6 +31,7 @@ set(contracts_sources
 detect_stray_source_files("${contracts_sources}" "contracts/")
 
 set(libsolutil_sources
+    libsolutil/CDCL.cpp
     libsolutil/Checksum.cpp
     libsolutil/CommonData.cpp
     libsolutil/CommonIO.cpp

test/libsolutil/CDCL.cpp

@@ -0,0 +1,121 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolutil/CDCL.h>
+#include <test/Common.h>
+
+#include <boost/test/unit_test.hpp>
+
+using namespace std;
+using namespace solidity::util;
+
+
+namespace solidity::util::test
+{
+
+class CDCLTestFramework
+{
+public:
+	Literal variable(string const& _name)
+	{
+		m_variables.emplace_back(_name);
+		return Literal{true, m_variables.size() - 1};
+	}
+
+	void satisfiable(vector<Clause> _clauses)
+	{
+		auto model = CDCL{m_variables, move(_clauses)}.solve();
+		BOOST_REQUIRE(!!model);
+	}
+
+	void unsatisfiable(vector<Clause> _clauses)
+	{
+		auto model = CDCL{m_variables, move(_clauses)}.solve();
+		BOOST_REQUIRE(!model);
+	}
+
+protected:
+
+	vector<string> m_variables;
+};
+
+
+BOOST_FIXTURE_TEST_SUITE(CDCL, CDCLTestFramework, *boost::unit_test::label("nooptions"))
+
+BOOST_AUTO_TEST_CASE(basic)
+{
+	auto x = variable("x");
+	Clause c1{x, ~x};
+	satisfiable({c1});
+}
+
+BOOST_AUTO_TEST_CASE(basic_unsat1)
+{
+	auto x = variable("x");
+	unsatisfiable({{x}, {~x}});
+}
+
+BOOST_AUTO_TEST_CASE(basic_unsat2)
+{
+	auto x1 = variable("x1");
+	auto x2 = variable("x2");
+	Clause c1{x1, ~x2};
+	Clause c2{~x1, x2};
+	Clause c3{x1, x2};
+	Clause c4{~x1, ~x2};
+	unsatisfiable({c1, c2, c3, c4});
+}
+
+BOOST_AUTO_TEST_CASE(basic_sat)
+{
+	auto x1 = variable("x1");
+	auto x2 = variable("x2");
+	Clause c1{x1, ~x2};
+	Clause c2{~x1, x2};
+	Clause c3{x1, x2};
+	Clause c4{~x1, ~x2};
+	unsatisfiable({c1, c2, c3, c4});
+}
+
+BOOST_AUTO_TEST_CASE(learning)
+{
+	auto x1 = variable("x1");
+	auto x2 = variable("x2");
+	auto x3 = variable("x3");
+	auto x4 = variable("x4");
+	auto x7 = variable("x7");
+	auto x8 = variable("x8");
+	auto x9 = variable("x9");
+	auto x10 = variable("x10");
+	auto x11 = variable("x11");
+	auto x12 = variable("x12");
+	Clause c1{x1, x4};
+	Clause c2{x1, ~x3, ~x8};
+	Clause c3{x1, x8, x12};
+	Clause c4{x2, x11};
+	Clause c5{~x7, ~x3, x9};
+	Clause c6{~x7, x8, ~x9};
+	Clause c7{x7, x8, ~x10};
+	Clause c8{x7, x10, ~x12};
+	satisfiable({c1, c2, c3, c4, c5, c6, c7, c8});
+}
+
+
+BOOST_AUTO_TEST_SUITE_END()
+
+}