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.