OKlibrary  0.2.1.6
PdVanderWaerdenCNF.cpp File Reference

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

#include <string>
#include <iostream>
#include <fstream>
#include <boost/lexical_cast.hpp>
#include <OKlib/Satisfiability/Interfaces/InputOutput/Colouring.hpp>
#include <OKlib/Satisfiability/Interfaces/InputOutput/ClauseSetAdaptors.hpp>
#include <OKlib/Combinatorics/Hypergraphs/Generators/VanderWaerden.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 2-coloured palindromised van der Waerden problems.

  • Only 2-coloured vdW-problems can be generated; more than two colours have to be yet established.
  • The three command-line parameters are the two progression size and the number of vertices.
  • The output by default is put into file "VanDerWaerden_pd_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_pd_vanderwaerden2nd_stdname(k1,k2,n) in ComputerAlgebra/Satisfiability/Lisp/Generators/RamseyTheory/VanderWaerdenProblems.mac.

Definition in file PdVanderWaerdenCNF.cpp.


Enumeration Type Documentation

anonymous enum

Definition at line 48 of file PdVanderWaerdenCNF.cpp.


Function Documentation

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

Definition at line 66 of file PdVanderWaerdenCNF.cpp.