Satalyzer is a small, lightweight tool for the asynchronous visualization and analysis of event logs (JSON files) generated by supported logic and constraint solvers, such as SAT, CP, SMT and Answer Set solvers.
Satalyzer is written in Scala and runs on the Java VM (version 8 or higher).
It is not a general purpose logging or event analytics tool, it is mainly meant for SAT and similar solver development, debugging and preliminary benchmarking purposes.
java -jar satalyzer.jar <path to directory with event log files>
(A ready-to-run JAR file is available from Releases.)
On the dashboard, select one or more event log files in the upper left section. Events (singleton or grouped) appear in the upper middle pane. Select one or multiple entries there to see a graph depicting the event values.
Satalyzer reads JSON files consisting of event lists.
Generally, the entries in a Satalyzer log file are (event, value) pairs, where an event consists of a type and a timestamp, and possibly further information such as the solver thread which generated the event. An "event" can be any kind of message or measurement - it's entirely up to the solver what kinds of events it generates. For example, an event might be "number of conflicts at time 0:34:23, generated by thread $5" and its value might be 100637.
Events can also be used to write meta-information into the log file, e.g., the name, version and runtime settings of the solver.
Multiple events of the same kind can be grouped - this is useful for events which are all instances of the same type and are generated over the course of time of the same solver run, such as the number of conflicts or assignments (in DPLL/CDCL-style solvers), but also if multiple log files are selected and singleton events in those solver runs should be compared with each other, e.g., the overall run times of multiple solver runs (useful for preliminary benchmarking).
Event grouping happens automatically. If a group of events is selected in the upper middle pane, a graph visualization of the grouped event values is shown in the upper right pane. It is also possible to select multiple groups, to compare their graphs.
To let your solver generate Satalyzer log files, you currently need to include source code file SatalyzerUse.scala
into your solver project. (Currently, this very short file is available only in Scala code, but translating it
to, e.g., Java, Kotlin or Clojure shouldn't be difficult.)
Modify line import [...].stats as explained in file SatalyzerUse.scala (this is just
to bring into scope the main data structure (assumed to be in variable stats) for collecting Satalyzer log messages in your code).
In your own code, initialize the logger by assigning variable stats a value and calling initializeStatsFile().
E.g.,
var stats = new Stats(problemFile = "eventLog.json") // see Stats constructor for further parameters
initializeStatsFile()
To emit an event, use stats.writeEntry(). Examples:
stats.writeEntry(key = "numberUnassigned", value = noOfUnassignedVars, solverThreadNo = 5)
stats.writeEntry(key = "overallTimeMs", value = timeMs, solverThreadNo = 0)
To write the collected events to the JSON file, use
stats.writeToFile()
An existing solver for the Java VM which can generate Satalyzer logs is the Probabilistic Answer Set Programming and Probabilistic Satisfiability solver diff-SAT.
Author: Matthias Nickles
matthiasDOTnicklesATgmxDOTnet
Feedback and bug reports are welcome!
Copyright (c) 2020 by Matthias Nickles
Licensed under MIT license
jsoniter (https://jsoniter.com/)
Copyright (c) 2016 Tao Wen
License: https://github.com/json-iterator/java/blob/master/LICENSE
EvilPlot (https://cibotech.github.io/evilplot/)
Copyright (c) 2018 CiBO Technologies, Inc.
License: https://github.com/cibotech/evilplot/blob/master/LICENSE