/* -*- 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[1]);
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;
}