OKlibrary  0.2.1.6
VanderWaerdenCNF.cpp File Reference

Application for creating SAT instances expressing van-der-Waerden problems. More...

#include <iostream>
#include <string>
#include <fstream>
#include <boost/lexical_cast.hpp>
#include <OKlib/General/ErrorHandling.hpp>
#include <OKlib/Combinatorics/Hypergraphs/Generators/VanderWaerden.hpp>
#include <OKlib/Satisfiability/Transformers/Generators/VanderWaerdenCNF.hpp>

Go to the source code of this file.

Enumerations

enum  

Functions

int main (const int argc, const char *const argv[])

Detailed Description

Application for creating SAT instances expressing van-der-Waerden problems.

Deprecated:
Needs update.
  • Three command-line parameters "k1 k2 n" are needed for the two progression sizes k1, k2 and for the number n of vertices.
  • The output by default is put into file "VanDerWaerden_2-k1-k2_n.cnf".
  • An optional fourth argument S is treated as follows:
    1. If S="-", then output is put to standard output.
    2. Otherwise the output is put into a file named S.
  • For the Maxima specification see output_vanderwaerden2nd_stdname(k1,k2,n) in ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/VanderWaerdenProblems.mac.
Todo:
Update needed

Definition in file VanderWaerdenCNF.cpp.


Enumeration Type Documentation

anonymous enum

Definition at line 52 of file VanderWaerdenCNF.cpp.


Function Documentation

int main ( const int  argc,
const char *const  argv[] 
)

Definition at line 66 of file VanderWaerdenCNF.cpp.

References ErrorHandling::Error2string().