/* -*- C++ -*- * * This file is a part of LEMON, a generic C++ optimization library * * Copyright (C) 2003-2008 * Egervary Jeno Kombinatorikus Optimalizalasi Kutatocsoport * (Egervary Research Group on Combinatorial Optimization, EGRES). * * Permission to use, modify and distribute this software is granted * provided that this copyright notice appears in all copies. For * precise terms see the accompanying LICENSE file. * * This software is provided "AS IS" with no warranty of any kind, * express or implied, and with no claim as to its suitability for any * purpose. * */ /// \ingroup demos /// \file /// \brief Solver for SAT problems. /// /// This demo progam solves the SAT problem, i.e. the boolean /// satisfiability problem. The problem in general case is /// NP-complete. /// /// The program uses an integer linear program solver. A {0, /// 1} variable is assigned to each boolean variable. The /// disjunctions are converted to linear inequalities as each negation /// is replaced with a substraction from one and each disjunction is /// converted to addition. The generated linear expression should be /// at least one. /// /// \include sat.cc #include #include #include #include #include using namespace std; using namespace lemon; int main(int argc, const char *argv[]) { if (argc != 2) { std::cerr << "The SAT solver demo" << std::endl << std::endl; std::cerr << "The parameter should be a filename" << std::endl; std::cerr << "Each line of the file should contain a bool expression:" << std::endl; std::cerr << " [not] [or [not] ]..." << std::endl; std::cerr << "The program prints a feasible solution if it exists" << std::endl; return -1; } ifstream is(argv); Mip mip; mip.max(); mip.obj(0); string line; while (getline(is, line)) { istringstream ls(line); Mip::Expr expr; string op; do { string var; bool neg = false; ls >> var; if (var == "not") { neg = true; ls >> var; } Mip::Col col = mip.colByName(var); if (col == INVALID) { col = mip.addCol(); mip.colName(col, var); mip.colLowerBound(col, 0); mip.colUpperBound(col, 1); mip.integer(col, true); } expr += (neg ? 1 - col : col); } while (ls >> op && op == "or"); if (ls) { std::cerr << "Wrong bool expression" << std::endl; return -1; } mip.addRow(expr >= 1); } mip.solve(); if (mip.mipStatus() == Mip::OPTIMAL) { for (Mip::ColIt it(mip); it != INVALID; ++it) { std::cout << mip.colName(it) << " = " << (mip.primal(it) == 1 ? "true" : "false") << std::endl; } } else { std::cout << "There is no feasible solution." << std::endl; } return 0; }