The clavis project provides visualization for the solver ASP clasp. It consists of the following three parts.
All parts of the clavis project are free software and licensed under the General Public License (GPL).
There is a source package available with clavis, libclavis and insight.
You can also visit sourceforge for current development versions. There are currently no binaries or versions for Windows or OS X available.
To build clavis run the following commands in the clavis directory.
./configure.sh [HDF5_INSTALL_DIR=<path_to_hdf5>]
cd build/release
make
To install, you need a current version of the HDF5 library.
To install simply run make install. This will copy both the modified clasp binary called clavis-bin and
the python wrapper called simply clavis.
To use clavis you will also need the PyTables library for python.
To install libclavis run the following command in the libclavis directory.
python setup.py install
libclavis requires the following additional libraries to work.
To install the vizualization tool insight simply copy the insight directory from the source distribution.
To produce graph layouts you can either compile the recommended OGDF wrapper that comes with insight
(see “insight/ogdf/README” for instructions) or install PyGraphviz >= 1.1.
If you install both, you will be able to select the layout at runtime.
Additionally, insight requires the following libraries.
You can call clavis just like clasp with an additional argument for the log file.
clavis <logfile> <file> [<file2> ...] <clasp_options>
Note that the logfile has to be the first argument and is given without the file extension .h5 which will be added automatically.
To restrict the events that will be logged, you can specify a config file with the --config option.
The default config file can be generated with the --default-config.
Events that are not supposed to be logged can be commented out.
clavis is compatible with all single-threaded options of clasp.
The logfiles generated by clavis can be read directly using the HDF5 library, via libclavis, or our visualization tool insight.
For example, the following python script uses the PyTables library to extract all learned nogoods from a logfile called log.h5.
import tables
with tables.openFile('log.h5') as log:
literals = log.root.literals
learned = log.root.events.learned
for i, e in enumerate(learned):
if i == learned.attrs.num:
break
print ' '.join(map(str, literals[slice(*e['lits'])]))
Note that the IDs printed are neither the IDs of the input file nor the internal IDs used by clavis. For more information see the Log Format section.
The python library libclavis was created to simplify reading log files by providing a serialized interface.
To this end, the Player object in the logfile module takes a logfile and “plays” all events in the order they were recorded.
The following example shows how to extract the learned nogoods from a logfile called log.h5.
from libclavis.logfile import Player, Listener
class LearnedPrinter(Listener):
def event_learned(self, player):
print ' '.join(map(str, player.event().lits()))
LearnedPrinter(Player('toh.h5'))
To start insight run the following command.
insight <logfile>
The logfile can be given at the start or opened from the user interface.
The following example visualizations were created by running clavis with the following options and running insight with the generated logfile.
clavis toh tohI.lp tohE.lp --heuristic=vsids
The a Towers of Hanoi example given by the files tohE.lp and tohI.lp is uses three pegs and four disks and is solvable in 15 time steps which is also the maximum number of moves allowed.
In the first snapshot we can see the view list on the left giving all currently active (white on blue) and passive (black on white) views. They can be (de)activated by mouse selection. The most basic one is the problem view in the middle. At its top, it summarizes the key figures of the solving process at hand. Below, the actual visualization is configured and engaged, distinguishing structural (‘Graph’) and temporal views (‘Plot’). The displayed setting allows for generating the program interaction graph. The resulting view can be seen on the right.
The graph nicely reflects the temporal structure of the Towers of Hanoi problem by grouping variables in a state-wise fashion.
That is, variables with the same time stamp form clusters along the graph.
The structure can be explored with zooming and panning functionalities (including reset button) and
the visualization can be focused (while all other views are hidden).
Note that the orientation of the graph is subject to random factors within the force-directed
layout (eg. the graph might be mirrored for slightly varying data).
However, the layout algorithm is seeded to assure that the same input leads to the same layout.
Different layout engines can be used; currently,
insight offers the choice between the FMMMLayout from OGDF and sfdp from Graphviz.
The placements of variables can be inferred from the highlighting of the symbol table while
hovering with the mouse over the nodes in the graph,
or simply by searching for symbols via pattern matching (eg. for move(*,1)).
The variable coloring in the graph reflects the number of flipped truth assignments. Inspecting the graph in conjunction with the symbol table reveals that the “hot-spot” of the problem concerns action and fluent variables with time stamps 3-6, changing their truth values more than twenty times (as shown in the symbol table). While these variables are in deeper red, the ones in the upper left part of the graph are colored in deeper green indicating that their truth value was rarely changed. This tells us that the goal conditions are strong enough to fix the truth values of variables close to the final state.
For a complement, let us look at the development of the conflict level (that is, the decision levels at which conflicts occur) during the solving process in the left view in the second snapshot.
To support this, we show on the right the frequency distribution of the number of decisions per conflict (i.e. the number of decisions made since the previous conflict or restart); this provides an idea on the progress made during the 155 conflicts on the x-axis on the left. For instance, 52 times no decision was made among two conflicts; here, the learned nogoods caused an(other) immediate conflict. 36 conflicts were obtained after a single decision. Now, following the (green) central moving average in the left view, we observe two peaks dividing the solving process into three parts. Our hypothesis is that a part of the problem has been solved during the first solving phase. To explore this further, we take advantage of insight’s zooming and panning capacities. That is, via mouse control, we select the last two segments of the solving process and generate
In fact, the coloring on the left is further constraint by restricting the view to variables whose
truth values remain unchanged during the last two parts of the solving process.
This selection is accomplished via the simple query val:0.
The resulting cloud of green nodes supports our conjecture that the truth value of the obtained
variables has been fixed in the first part of the solving process.
More evidence for this is provided by conflict learning because nothing has been learned about
this program part during the considered span of events.
This can be visualized by the projection of the learned nogood interactions onto the program interaction graph
(i.e. by keeping the layout of the variable nodes in the program interaction graph)
on the right:
The green nodes in the left view do not appear in the right one.
Hence, they do not appear in any nogoods learned in the last two phases of the solving process.
The clavis logfile format was designed to store large amounts of data that can be read efficiently and to be easily extended by additional information. It is based on the HDF5 database format which consists of a hierarchical structure similar to a file system that holds tables that store sets of homogenous data and optional metadata.
Each logfile of the logfile format version 1.1 contains the following datasets.
In any dataset containing more than one column, the columns are identified by their names and not indexes. Thus, when reading a logfile you should not rely on the order of columns.
literals is a one-dimensional dataset that stores literals used in events.
Whenever an event contains a nogood the literals are stored in this dataset and
the index of the first and next to last literal stored in the event. Each literal
is stored as sign * (variable_id + 1). This means that a the negative literal
of variable 0 is stored as -1.
Entry format: int32
variables contains all information about variables. Currently this includes the following.
The index in the dataset corresponds to the index of the variable.
Important: the symbols are stored with fixed length as pytables currently does not support
variable-length strings.
Entry format: (type: uint8, symbol: c_string)
assignments is a two-dimensional dataset holding the assigned values for events like propagations. The second dimension is defined by the number of variables in the logfile. The value for each variable is one of 0 (unassigned), 1 (true), or 2 (false).
Entry format: uint8
info is a container for all metadata and contains only attributes (and an empty dummy table). The following attributes are included.
--outf=2 --stats=2)events is a group containing all event datasets.
all contains the global index including all events. Each event is stored as a type and an index.
All of the following event datasets have an attribute called id which defines their type.
On reading a logfile, an index should be created with all event types and their datasets in the log.
Do not rely on the indexes used by clavis as they may change.
index refers to the index of the event in the dataset corresponding to the type.
All following datasets contain and ‘index` that refers to this dataset.
This allows for reconstructring the order of events without searching the global index.
Entry format: (type: uint8, index: uint32)
program contains the constraints representing the problem. While they’re technically not
events that occur during the solving, they’re stored as events to read them using the same interface.
type is either 0 (nogood) or 1 (weight or cardinality constraint).
opt is 0 if the constraint was stored in special datastructure for fast propagation, else 1.
lits are the literals in the constraint and represented by a start index and end index
which is the index following the last element.
Entry format: (index: uint32, type: uint8, opt: uint8, lits: uint8)
learned contains the nogoods learned during the solving process either by conflict analysis
or by finding an unfounded set.
id is a unique identifier for the nogood to find out whether it gets deleted later on.
Nogoods stored in a special datastructur get the id 0.
lbd is the Literal(s) Block Distance.
lits are the literals in the nogood and represented by a start index and end index
Entry format: (index: uint32, id: size_t, lbd: uint16, lits: (start: uint, end: uint))
deleted contains all deletion events of learned nogoods.
id is the unique identifier of the deleted nogood.
Entry format: (index: uint32, id: size_t)
propagation contains all propagation events.
assignment is the index in the assignment dataset.
Entry format: (index: uint32, assignment: uint)
decision contains all decision events.
var is the variable and val its value which is either 1 (true) or 2 (false).
Entry format: (index: uint32, var: uint32, val: uint8, level: uint16)
conflict contains all conflict events.
lits is the conflict constraint (not the learned nogood).
Entry format: (index: uint32, lits: (start: uint, end: uint))
conflict_res contains all resolution steps of the conflict analysis.
They are logged after the conflict and before the learned nogood.
lit is the literal that is deleted and reason is the nogood that replaces it.
Entry format: (index: uint32, lit: int32, reason: (start: uint, end: uint))
backtrack contains all backtracks (not backjumps).
assignment is the index in the assignment dataset.
Entry format: (index: uint32, assignment: uint)
backjump contains all backjumps (not backtracks).
length is the number of reverted decisions and
assignment is the index in the assignment dataset.
Entry format: (index: uint32, length: uint16, assignment: uint)
solution contains all models of the problem.
assignment is the index in the assignment dataset.
Entry format: (index: uint32, assignment: uint)
restart contains all restart and currently no additional information. Entry format: (index: uint32)