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