Thomas C. van Dijk, Fabian Lipp, Peter Markfelder and Alexander Wolff
Lehrstuhl für Informatik I, Universität Würzburg, Germany
http://www1.informatik.uni-wuerzburg.de/en/staff
All implementations are written in C++, with the exception of some "driver" code in Python for Sat. Comparable effort has been put into optimizing each program. Memory usage was not optimized, but there are no flagrant memory inefficiencies.
Code is available in the src
directory.
We have compiled the C++11 code with Visual Studio 2017 Community Edition.
We have run the Python code with Pypy 5.7.1 Python 2.7.13.
The implementation uses Python to write CNF SAT instances in DIMACS format, to run Minisat on them, and to run the search.
Directory: src/sat
Get a 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
.Get the Minisat source code from minisat.se. We have used minisat-2.2.0.tar.gz from this location: http://minisat.se/downloads/minisat-2.2.0.tar.gz
Under Visual Studio 2017 Community Edition, the above code does not compile as-is. Solve the following three problems.
vcpkg
as package manager.core/Main.cc
, either by hand or by applying our patch src/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 <windows.h>
#include <psapi.h>
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 patch /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.)The implementation is in straight C++11 without libraries. See: Block Crossings in Storyline Visualizations. T. C. van Dijk, M. Fink, N. Fischer, F. Lipp, P. Markfelder, A. Ravsky, S. Suri, A. Wolff. Proceedings of the 24nd Internation Symposium on Graph Drawing. (2016).
Directory: src/exact
Compile 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 the SAT-based program on the same instances.typedef uint8_t CharName;
typedef set<CharName> Meeting;
. It could be interesting to use bitsets instead.typedef vector<Meeting> Meetings;
k
characters and the instance as meetings
, run the FPT algorithm using dp<Silent>( k, meetings )
. For more debug output, use dp<Verbose>
instead.iterativeDeepening<Silent>( k, meetings )
or <Verbose>
. (It is probably much slower than dp
.)random_uniform
and random_small
to generate random instances.Timer
objects to measure time: double Timer::elapsed()
gives seconds since the object was constructed.This program does not read the same input file format as Sat. (This program does not support concurrent meetings, which Sat does.) In order to compare to Sat, proceed as follows.
writePCSV
to write .pcsv files.