Thomas C. van Dijk, Fabian Lipp, Peter Markfelder, and Alexander Wolff
Lehrstuhl für Informatik I, Universitüt Würzburg, Germany
/sat
minisat executable for your system and put it in /sat. See below on how to build Minisat on Windows; in our experience, the Cygwin-based executable available at minisat.se does not work.
[your python] main.py [filename], for example pypy main.py example/star_wars.pcsv.
minisat-2.2.0.tar.gz from this location.
Under Visual Studio 2017 Community Edition, the above code does not compile as-is. Solve the following three problems.
core/Main.cc, either by hand or by applying our /minisat4win/Main.cc.patch.
"PRIu64" to " PRIu64 ", since Visual Studio chokes otherwise.
mem_lim != INT32_MAX and cpu_lim != INT32_MAX.
signal with signals that Windows does not have, such as signal(SIGXCPU,SIGINT_exit);. This does not influence our experiments, because of the previous point.
printStats, change to double mem_used = getPeakRSS();. Above printStats, add:
#include#include size_t getPeakRSS() { PROCESS_MEMORY_COUNTERS info; GetProcessMemoryInfo(GetCurrentProcess(), &info, sizeof(info)); return (size_t)info.PeakWorkingSetSize / (1024*1024); }
utils/ParseUtils.h, either by hand or by applying our /minisat4win/ParseUtils.h.patch.
static const int buffer_size = 1048576; to 4096 or some other small number. (Windows, by default, has a smaller stack size and will crash with minisat's default value. Using a smaller read buffer is the simplest fix.)
/exact
bcdp.cpp. You may need to include a compiler flag to compile as C++11, for example -std=c++11 in older versions of g++.
There is no commandline interface. As-is, the program runs some experiments on random graphs.
main (bottom of the file) and try to read
along.
run_FromFile for an example of how to
run the algorithms on a simple file format.
run_RandomInstances for an example of
how to automatically run measurements on random instances and
write the results to a CSV file. This also writes each
instance to a PCSV file so you can run Sat on the same
instances.
typedef
uint8_t CharName;
typedef set
Meeting;
typedef
vector Meetings;
k the number of characters
and meetings the instance, run the FPT algorithm
using dp( k, meetings ) . For more debug
output, use dp instead.
iterativeDeepening( k,
meetings ) or .
random_uniform and random_small to
generate random instances.
Timer objects to measure time: double
Timer::elapsed() gives seconds since the object was
constructed.
writePCSV to write .pcsv files.