From 3e0f4cd7bb0fd4565aa38a495b8a59d7cd3b145f Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Mon, 21 Mar 2022 17:52:47 +0100 Subject: [PATCH] Adding example SAT solver --- tools/CMakeLists.txt | 4 + tools/satsolver-main.cpp | 188 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 192 insertions(+) create mode 100644 tools/satsolver-main.cpp diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt index b442ba96a..83a869579 100644 --- a/tools/CMakeLists.txt +++ b/tools/CMakeLists.txt @@ -49,3 +49,7 @@ add_executable(yul-phaser yulPhaser/main.cpp) target_link_libraries(yul-phaser PRIVATE phaser) install(TARGETS yul-phaser DESTINATION "${CMAKE_INSTALL_BINDIR}") + + +add_executable(satsolver satsolver-main.cpp) +target_link_libraries(satsolver PUBLIC solidity range-v3 Boost::boost Boost::program_options) diff --git a/tools/satsolver-main.cpp b/tools/satsolver-main.cpp new file mode 100644 index 000000000..8e09b0eec --- /dev/null +++ b/tools/satsolver-main.cpp @@ -0,0 +1,188 @@ +/* + 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 +#include +#include +#include +#include +#include +#include + +using namespace solidity::util; +using std::vector; +using std::string; +using std::cout; +using std::endl; +using std::optional; +using std::nullopt; +using std::stringstream; +using std::make_pair; + +const int verbose = 0; +vector cutStringBySpace(string& input); +optional> parseLine(std::string& line); +std::pair>, size_t> readCNFFile(const string& fname); +size_t getNumVars(const vector>& cls); + + +vector cutStringBySpace(string& input) +{ + return input | ranges::views::split(' ') | ranges::to>(); +} + +optional> parseLine(std::string& line) +{ + vector cl; + bool end_of_clause = false; + for (auto const& part: line | ranges::views::split(' ')) + { + if (end_of_clause) + { + cout << "ERROR: trailing elements after finishing `0` at the end of a clause in CNF file" << endl; + exit(-1); + } + const long lit = std::stol(ranges::to(part)); + const long var = std::abs(lit); + if (var == 0) + { + //end of clause + end_of_clause = true; + continue; + } + assert(var > 0); + const Literal l {lit > 0, (size_t)var-1}; + cl.push_back(l); + } + + if (verbose) + { + cout << "cl: "; + for (auto const& l: cl) + cout << (l.positive ? "" : "-") << (l.variable+1) << " "; + cout << " end: " << (int)end_of_clause << endl; + } + + if (end_of_clause) + return cl; + else + return nullopt; +} + +std::pair>, size_t> readCNFFile(const string& fname) +{ + long vars_by_header = -1; + long cls_by_header = -1; + vector> cls; + std::ifstream infile(fname.c_str()); + + std::string line; + while (std::getline(infile, line)) + { + if (line.empty()) + continue; + if (line[0] == 'p') { + assert(line.substr(0,6) == string("p cnf ")); + line = line.substr(6); + vector parts = cutStringBySpace(line); + vars_by_header = std::stol(parts[0]); + assert(vars_by_header >= 0); + cls_by_header = std::stol(parts[1]); + assert(cls_by_header >= 0); + + continue; + } + const auto cl = parseLine(line); + if (cl) + cls.push_back(cl.value()); + } + if (vars_by_header == -1) + { + cout << "ERROR: CNF did not have a header" << endl; + exit(-1); + } + + assert(cls_by_header >= 0); + if (cls.size() != (size_t)cls_by_header) + { + cout << "ERROR: header said number of clauses will be " << cls_by_header << " but we read " << cls.size() << endl; + exit(-1); + } + + return make_pair(cls, (size_t)vars_by_header); +} + +size_t getNumVars(const vector>& cls) +{ + size_t largestVar = 0; + for (auto const& cl: cls) + for (auto const& l: cl) + largestVar = std::max(largestVar, l.variable+1); + + return largestVar; +} + +int main(int argc, char** argv) +{ + if (argc != 2) + { + cout << "ERROR: you must give CNF a parameters" << endl; + exit(-1); + } + + const string cnf_file_name = argv[1]; + auto&& [cls, max_vars_by_header] = readCNFFile(cnf_file_name); + const size_t num_vars_by_cls = getNumVars(cls); + vector m_variables; + + if (max_vars_by_header < num_vars_by_cls) + { + cout << "ERROR: header promises less variables than what clauses say" << endl; + exit(-1); + } + assert(max_vars_by_header >= num_vars_by_cls); + + for (size_t i = 0; i < max_vars_by_header; i ++) + m_variables.push_back(string("x") + std::to_string(i)); + + auto model = CDCL{m_variables, move(cls)}.solve(); + + if (model) { + const size_t line_break_after = 80; + stringstream ss; + ss << "v"; + for (size_t i = 0; i < model->size(); i++) { + if (ss.str().size() > line_break_after) { + cout << ss.str() << endl; + ss.clear(); + ss << "v"; + } +// if (model->at(i) != TriState::t_unset()) { +// ss << " " << (model->at(i) == TriState::t_true() ? "" : "-") << i+1; +// } + + } + cout << ss.str() << " 0" << endl; + cout << "s SATISFIABLE" << endl; + } else + cout << "s UNSATISFIABLE" << endl; + + return 0; +}