From 84c5c37c31aa66383629813cae605fbcbcb54ab7 Mon Sep 17 00:00:00 2001 From: chriseth Date: Mon, 21 Feb 2022 13:16:32 +0100 Subject: [PATCH] cdcl --- libsolutil/CDCL.cpp | 322 ++++++++++++++++++++++++++++++++++++++ libsolutil/CDCL.h | 119 ++++++++++++++ libsolutil/CMakeLists.txt | 2 + test/CMakeLists.txt | 1 + test/libsolutil/CDCL.cpp | 121 ++++++++++++++ 5 files changed, 565 insertions(+) create mode 100644 libsolutil/CDCL.cpp create mode 100644 libsolutil/CDCL.h create mode 100644 test/libsolutil/CDCL.cpp diff --git a/libsolutil/CDCL.cpp b/libsolutil/CDCL.cpp new file mode 100644 index 000000000..42aadda10 --- /dev/null +++ b/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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include + +#include + +// TODO remove before merge +#include +#include + +using namespace std; +using namespace solidity; +using namespace solidity::util; + + +CDCL::CDCL( + vector _variables, + vector const& _clauses, + std::function(std::map 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::solve() +{ + cout << "====" << endl; + for (unique_ptr const& c: m_clauses) + cout << toString(*c) << endl; + cout << "====" << endl; + while (true) + { + optional 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(2, _clause.size()); i++) + m_watches[_clause.at(i)].push_back(&_clause); +} + +optional 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 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 CDCL::analyze(Clause _conflictClause) +{ + solAssert(!_conflictClause.empty()); + cout << "Analyzing conflict." << endl; + Clause learntClause; + size_t backtrackLevel = 0; + + set seenVariables; + + int pathCount = 0; + size_t trailIndex = m_assignmentTrail.size() - 1; + optional 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(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 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 literals; + for (Literal const& l: _clause) + literals.emplace_back(toString(l)); + return "(" + joinHumanReadable(literals) + ")"; +} + diff --git a/libsolutil/CDCL.h b/libsolutil/CDCL.h new file mode 100644 index 000000000..0bbf2cde9 --- /dev/null +++ b/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 . +*/ +// SPDX-License-Identifier: GPL-3.0 +#pragma once + +#include +#include +#include +#include +#include +#include +#include + +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; + +class CDCL +{ +public: + using Model = std::map; + CDCL( + std::vector _variables, + std::vector const& _clauses, + std::function(std::map const&)> _theoryPropagator = {} + ); + + std::optional solve(); + +private: + void setupWatches(Clause& _clause); + std::optional propagate(); + std::pair 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 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::map)> m_theorySolver; + + std::vector m_variables; + /// includes the learnt clauses + std::vector> 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> m_watches; + + /// Current assignments. + std::map m_assignments; + std::map m_levelForVariable; + /// TODO wolud be good to not have to copy the clauses + std::map m_reason; + + // TODO group those into a class + + std::vector m_assignmentTrail; + /// Indices into assignmentTrail where decisions were taken. + std::vector m_decisionPoints; + /// Index into assignmentTrail: All assignments starting there have not yet been propagated. + size_t m_assignmentQueuePointer = 0; +}; + + +} diff --git a/libsolutil/CMakeLists.txt b/libsolutil/CMakeLists.txt index a1d915bb3..9a9d97c8c 100644 --- a/libsolutil/CMakeLists.txt +++ b/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 diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index c2332621a..a35cfb772 100644 --- a/test/CMakeLists.txt +++ b/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 diff --git a/test/libsolutil/CDCL.cpp b/test/libsolutil/CDCL.cpp new file mode 100644 index 000000000..5d4e2cfae --- /dev/null +++ b/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 . +*/ +// SPDX-License-Identifier: GPL-3.0 + +#include +#include + +#include + +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 _clauses) + { + auto model = CDCL{m_variables, move(_clauses)}.solve(); + BOOST_REQUIRE(!!model); + } + + void unsatisfiable(vector _clauses) + { + auto model = CDCL{m_variables, move(_clauses)}.solve(); + BOOST_REQUIRE(!model); + } + +protected: + + vector 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() + +}