sat.cpp
Go to the documentation of this file.
/* -*- 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;
class SatOptions : public Options {
public:
std::string filename;
SatOptions(const char* s)
: Options(s) {}
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--;
}
virtual void help(void) {
Options::help();
std::cerr << "\t(string) " << std::endl
<< "\t\tdimacs file to parse (.cnf)" << std::endl;
}
};
class Sat : public Script {
private:
BoolVarArray x;
public:
Sat(const SatOptions& opt)
: Script(opt) {
parseDIMACS(opt.filename.c_str());
branch(*this, x, BOOL_VAR_AFC_MAX(), BOOL_VAL_MIN());
}
Sat(Sat& s) : Script(s) {
x.update(*this, s.x);
}
virtual Space*
copy(void) {
return new Sat(*this);
}
virtual void
print(std::ostream& os) const {
os << "solution:\n" << x << std::endl;
}
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);
}
}
};
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
Gecode::BaseOptions::help
virtual void help(void)
Print help text.
Definition options.cpp:494
Gecode::BaseOptions::parse
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc).
Definition options.cpp:548
Gecode::BoolVarArgs
Passing Boolean variables.
Definition int.hh:712
Gecode::BoolVarArray
Boolean variable array.
Definition int.hh:808
Gecode::Driver::ScriptBase< Driver::IgnoreStepOption< Space > >::run
static void run(const Options &opt, Script *s=NULL)
Gecode::Options::Options
Options(const char *s)
Initialize options for script with name s.
Definition options.cpp:576
Gecode::Space
Computation spaces.
Definition core.hpp:1742
SatOptions
Options for SAT problems.
Definition sat.cpp:49
SatOptions::parse
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc).
Definition sat.cpp:57
SatOptions::help
virtual void help(void)
Print help message.
Definition sat.cpp:69
SatOptions::filename
std::string filename
Name of the DIMACS file to parse.
Definition sat.cpp:52
SatOptions::SatOptions
SatOptions(const char *s)
Initialize options with file name s.
Definition sat.cpp:54
Sat::copy
virtual Space * copy(void)
Perform copying during cloning.
Definition sat.cpp:130
Sat::Sat
Sat(const SatOptions &opt)
The actual problem.
Definition sat.cpp:117
Sat::parseDIMACS
void parseDIMACS(const char *f)
Post constraints according to DIMACS file f.
Definition sat.cpp:141
Sat::print
virtual void print(std::ostream &os) const
Print solution.
Definition sat.cpp:136
Sat::Sat
Sat(Sat &s)
Constructor for cloning.
Definition sat.cpp:124
Test::Options::parse
void parse(int argc, char *argv[])
Parse commandline arguments.
Definition test.cpp:120
driver.hh
int.hh
Gecode::Script
Driver::ScriptBase< Driver::IgnoreStepOption< Space > > Script
Base-class for scripts.
Definition driver.hh:801
Gecode::branch
void branch(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatValBranch vals, FloatBranchFilter bf=nullptr, FloatVarValPrint vvp=nullptr)
Branch over x with variable selection vars and value selection vals.
Definition branch.cpp:39
Gecode::clause
void clause(Home home, BoolOpType o, const BoolVarArgs &x, const BoolVarArgs &y, BoolVar z, IntPropLevel ipl=IPL_DEF)
Post domain consistent propagator for Boolean clause with positive variables x and negative variables...
Definition bool.cpp:955
Gecode::BOT_OR
@ BOT_OR
Disjunction.
Definition int.hh:952
Gecode
Gecode toplevel namespace
Gecode::BOOL_VAL_MIN
BoolValBranch BOOL_VAL_MIN(void)
Select smallest value.
Definition val.hpp:130
Gecode::neg
IntRelType neg(IntRelType irt)
Return negated relation type of irt.
Definition irt.hpp:52
Gecode::BOOL_VAR_AFC_MAX
BoolVarBranch BOOL_VAR_AFC_MAX(double d=1.0, BranchTbl tbl=nullptr)
Select variable with largest accumulated failure count with decay factor d.
Definition var.hpp:404
Test::opt
Options opt
The options.
Definition test.cpp:97
main
int main(int argc, char *argv[])
Definition test.cpp:208