258 lines
7.0 KiB
C++
258 lines
7.0 KiB
C++
/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
|
|
/*
|
|
* Main authors:
|
|
* Raphael Reischuk <reischuk@cs.uni-sb.de>
|
|
* Guido Tack <tack@gecode.org>
|
|
*
|
|
* Copyright:
|
|
* Raphael Reischuk, 2008
|
|
* Guido Tack, 2008
|
|
*
|
|
* This file is part of Gecode, the generic constraint
|
|
* development environment:
|
|
* http://www.gecode.org
|
|
*
|
|
* Permission is hereby granted, free of charge, to any person obtaining
|
|
* a copy of this software and associated documentation files (the
|
|
* "Software"), to deal in the Software without restriction, including
|
|
* without limitation the rights to use, copy, modify, merge, publish,
|
|
* distribute, sublicense, and/or sell copies of the Software, and to
|
|
* permit persons to whom the Software is furnished to do so, subject to
|
|
* the following conditions:
|
|
*
|
|
* The above copyright notice and this permission notice shall be
|
|
* included in all copies or substantial portions of the Software.
|
|
*
|
|
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
|
|
* EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
|
|
* MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
|
|
* NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
|
|
* LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
|
|
* OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
|
|
* WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
|
|
*
|
|
*/
|
|
|
|
#include <gecode/driver.hh>
|
|
#include <gecode/int.hh>
|
|
|
|
#include <fstream>
|
|
#include <string>
|
|
#include <vector>
|
|
|
|
using namespace Gecode;
|
|
|
|
/** \brief Options for %SAT problems
|
|
*
|
|
* \relates SAT
|
|
*/
|
|
class SatOptions : public Options {
|
|
public:
|
|
/// Name of the DIMACS file to parse
|
|
std::string filename;
|
|
/// Initialize options with file name \a s
|
|
SatOptions(const char* s)
|
|
: Options(s) {}
|
|
/// Parse options from arguments \a argv (number is \a argc)
|
|
void parse(int& argc, char* argv[]) {
|
|
// Parse regular options
|
|
Options::parse(argc,argv);
|
|
// Filename, should be at position 1
|
|
if (argc == 1) {
|
|
help();
|
|
exit(1);
|
|
}
|
|
filename = argv[1];
|
|
argc--;
|
|
}
|
|
/// Print help message
|
|
virtual void help(void) {
|
|
Options::help();
|
|
std::cerr << "\t(string) " << std::endl
|
|
<< "\t\tdimacs file to parse (.cnf)" << std::endl;
|
|
}
|
|
};
|
|
|
|
/**
|
|
* \brief %Example: CNF SAT solver
|
|
*
|
|
* SAT finds assignments of Boolean variables such
|
|
* that a set of clauses is satisfied or shows that
|
|
* no such assignment exists.
|
|
*
|
|
* This example parses a dimacs CNF file in which
|
|
* the constraints are specified. For each line of
|
|
* the file a clause propagator is posted.
|
|
*
|
|
* Format of dimacs CNF files:
|
|
*
|
|
* A dimacs file starts with comments (each line
|
|
* starts with c). The number of variables and the
|
|
* number of clauses is defined by the line
|
|
*
|
|
* p cnf \<variables\> \<clauses\>
|
|
*
|
|
* Each of the subsequent lines specifies a clause.
|
|
* A positive literal is denoted by a positive
|
|
* integer, a negative literal is denoted by the
|
|
* corresponding negative integer. Each line is
|
|
* terminated by 0.
|
|
*
|
|
* c sample CNF file
|
|
* p cnf 3 2
|
|
* 3 -1 0
|
|
* 1 2 -1 0
|
|
*
|
|
* Benchmarks on satlib.org, for instance,
|
|
* are in the dimacs CNF format.
|
|
*
|
|
* \ingroup Example
|
|
*/
|
|
class Sat : public Script {
|
|
private:
|
|
/// The Boolean variables
|
|
BoolVarArray x;
|
|
public:
|
|
/// The actual problem
|
|
Sat(const SatOptions& opt)
|
|
: Script(opt) {
|
|
parseDIMACS(opt.filename.c_str());
|
|
branch(*this, x, BOOL_VAR_AFC_MAX(), BOOL_VAL_MIN());
|
|
}
|
|
|
|
/// Constructor for cloning
|
|
Sat(Sat& s) : Script(s) {
|
|
x.update(*this, s.x);
|
|
}
|
|
|
|
/// Perform copying during cloning
|
|
virtual Space*
|
|
copy(void) {
|
|
return new Sat(*this);
|
|
}
|
|
|
|
/// Print solution
|
|
virtual void
|
|
print(std::ostream& os) const {
|
|
os << "solution:\n" << x << std::endl;
|
|
}
|
|
|
|
/// Post constraints according to DIMACS file \a f
|
|
void parseDIMACS(const char* f) {
|
|
int variables = 0;
|
|
int clauses = 0;
|
|
std::ifstream dimacs(f);
|
|
if (!dimacs) {
|
|
std::cerr << "error: file '" << f << "' not found" << std::endl;
|
|
exit(1);
|
|
}
|
|
std::cout << "Solving problem from DIMACS file '" << f << "'"
|
|
<< std::endl;
|
|
std::string line;
|
|
int c = 0;
|
|
while (dimacs.good()) {
|
|
std::getline(dimacs,line);
|
|
// Comments (ignore them)
|
|
if (line[0] == 'c' || line == "") {
|
|
}
|
|
// Line has format "p cnf <variables> <clauses>"
|
|
else if (variables == 0 && clauses == 0 &&
|
|
line[0] == 'p' && line[1] == ' ' &&
|
|
line[2] == 'c' && line[3] == 'n' &&
|
|
line[4] == 'f' && line[5] == ' ') {
|
|
int i = 6;
|
|
while (line[i] >= '0' && line[i] <= '9') {
|
|
variables = 10*variables + line[i] - '0';
|
|
i++;
|
|
}
|
|
i++;
|
|
while (line[i] >= '0' && line[i] <= '9') {
|
|
clauses = 10*clauses + line[i] - '0';
|
|
i++;
|
|
}
|
|
std::cout << "(" << variables << " variables, "
|
|
<< clauses << " clauses)" << std::endl << std::endl;
|
|
// Add variables to array
|
|
x = BoolVarArray(*this, variables, 0, 1);
|
|
}
|
|
// Parse regular clause
|
|
else if (variables > 0 &&
|
|
((line[0] >= '0' && line[0] <= '9') || line[0] == '-' || line[0] == ' ')) {
|
|
c++;
|
|
std::vector<int> pos;
|
|
std::vector<int> neg;
|
|
int i = 0;
|
|
while (line[i] != 0) {
|
|
if (line[i] == ' ') {
|
|
i++;
|
|
continue;
|
|
}
|
|
bool positive = true;
|
|
if (line[i] == '-') {
|
|
positive = false;
|
|
i++;
|
|
}
|
|
int value = 0;
|
|
while (line[i] >= '0' && line[i] <= '9') {
|
|
value = 10 * value + line[i] - '0';
|
|
i++;
|
|
}
|
|
if (value != 0) {
|
|
if (positive)
|
|
pos.push_back(value-1);
|
|
else
|
|
neg.push_back(value-1);
|
|
i++;
|
|
}
|
|
}
|
|
|
|
// Create positive BoolVarArgs
|
|
BoolVarArgs positives(pos.size());
|
|
for (int i=pos.size(); i--;)
|
|
positives[i] = x[pos[i]];
|
|
|
|
BoolVarArgs negatives(neg.size());
|
|
for (int i=neg.size(); i--;)
|
|
negatives[i] = x[neg[i]];
|
|
|
|
// Post propagators
|
|
clause(*this, BOT_OR, positives, negatives, 1);
|
|
}
|
|
else {
|
|
std::cerr << "format error in dimacs file" << std::endl;
|
|
std::cerr << "context: '" << line << "'" << std::endl;
|
|
std::exit(EXIT_FAILURE);
|
|
}
|
|
}
|
|
dimacs.close();
|
|
if (clauses != c) {
|
|
std::cerr << "error: number of specified clauses seems to be wrong."
|
|
<< std::endl;
|
|
std::exit(EXIT_FAILURE);
|
|
}
|
|
}
|
|
};
|
|
|
|
|
|
/** \brief Main-function
|
|
* \relates SAT
|
|
*/
|
|
int main(int argc, char* argv[]) {
|
|
|
|
SatOptions opt("SAT");
|
|
opt.parse(argc,argv);
|
|
|
|
// Check whether all arguments are successfully parsed
|
|
if (argc > 1) {
|
|
std::cerr << "Could not parse all arguments." << std::endl;
|
|
opt.help();
|
|
std::exit(EXIT_FAILURE);
|
|
}
|
|
|
|
// Run SAT solver
|
|
Script::run<Sat,DFS,SatOptions>(opt);
|
|
return 0;
|
|
}
|
|
|
|
// STATISTICS: example-any
|