/* -*- C++ -*-
*
* This file is a part of LEMON, a generic C++ optimization library
*
* Copyright (C) 2003-2007
* 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-2 problems.
///
/// This demo progam solves the SAT-2 problem, i.e. the boolean
/// satisfiability problem where each disjuction consists at most 2
/// terms.
///
/// The program generates a graph from the boolean expression. Two
/// nodes are assigned to each boolean variable, an x and a
/// not x nodes. If there is an x or y disjunction
/// in the formula, then the not x => y and the not y =>
/// x edges are added to the graph. If there is a single
/// x term disjunction in the formula then the not x
/// =>x edge is added to the graph.
///
/// The boolean formula could be satified if and only if the
/// x and not x nodes are in different strongly connected
/// components. A feasible solution could be get from the current
/// component numbering.
///
/// \include sat-2.cc
#include
#include
#include
#include
#include