satexplorer

This tool can be used to visualize the process of solving SAT instances. It can layout the clause variable incidence graph and be used to step through a trace of a solution process, highlighting the variables which the solver set. The default solver is Minisat, but we a provide a header file, that hopefully makes it easy to integrate tracing into other SAT solvers using CDCL.

Build

We tested installation on Linux (Ubuntu and Archlinux), but Mac OS and Windows might also work.

Install the dependencies:

• qt5-base (libqt5 on Ubuntu)
• OGDF (We highly recommend our patches for more performance, but standard OGDF will also work, find detailed instructions in ogdf_installation/README.md)
• python-networkx
• python-louvain
• zlib
• bison
• flex

Remember to init and update git submodules

Inside the repository create a build folder and cd into it, execute cmake .. and make.

Using your own SAT solver

Our fork of Minisat provides a header file which contains functions, that can be used for writing the tracefile, that is rendered in satexplorer. Call these functions at the relevant spots in the solver and than change the solver command in the initialize function in satviewer/Stepper.cpp with your own solver.

Related Tools

The following tools convert circuits to SAT instances for hardware verification:

• bmc
• bcsat

Usage

Run ./satviewer-bin [sat-instance] [options] in build folder. The sat instance must be in cnf format. If none is specified, a file dialog will open to select one.

Functionality:

• Step, Branch, Next Conflict, Next Restart: Skip forward and display to the next entry in the tracefile matching the clicked type.
• Last restart: Skip forward to the last restart entry in the tracefile
• Relayout: re-run the layouting algorithm
• Zoom in/out: does what it says
• Cluster: run the clustering script and apply the resulting clustering (via colors)
• Show all: resets node culling - all nodes and edges will be visible. also relayouts the graph.
• Exports the underlying .svg as .png - will be saved in ${working_directory}/data/exported_image.png
• Textbox: insert a number here to cull nodes with degree larger than the entered value.
• Draw a rectangle with the mouse (click&drag) to color all nodes in the rectangle. Rightclicking and drawing will reset the color to white.

Color coding:

When stepping through the tracefile, (variable-)nodes are assigned a color based on their state within Minisat at that time.

• Red/Green: It was inferred that the variable has to be set to false/true
• Orange/Blue: Minisat branched on this Node (It tries out different 'paths') and set it to false/true
• Black: A conflict was detected in this variable. That means it was inferred that this variable has to be set to both true and false to satisfy the formula.

Options

Flag	Description
-f	force recomputation of the solution instead of reusing a previous tracefile
-s	visualize the graph simplified by Minisat instead of the original graph
-i	display an implication graph, i.e., only edges for clauses with two variables

Importing Layouts

Using the button Import Layout you can import files with the ending .layout in the following format:

The first line contains the word size followed by a space and then the number of graph nodes n to be shown. After that follow n lines, with the name of the node and then the coordinates separated by spaces. The name is either c<index of clause in cnf file> (starting from 0) or l<name of variable in cnf file>.

Example:

size 5
c0 30 50
c1 40 60
l0 0 0
l1 0 50
l2 50 0

This means, that two clauses and three variables are shown (five graph nodes in total).

VSCODE launch configuration

{
    "name": "debug",
    "type": "cppdbg",
    "request": "launch",
    "program": "${workspaceFolder}/build/satviewer-bin",
    "args": ["path/to/file.cnf"],
    "stopAtEntry": false,
    "cwd": "${workspaceFolder}/build/",
    "environment": [],
    "externalConsole": true,
    "MIMode": "gdb",
    "setupCommands": [
        {
            "description": "Enable pretty-printing for gdb",
            "text": "-enable-pretty-printing",
            "ignoreFailures": true
        }
    ]
}

How satviewer works

The program takes files in DIMACS (.cnf) format. For detailed information refer to http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html The input file is converted to the GML format via a python script. The .gml file can then be read by the OGDF library.

The .cnf file is also used as input for the SAT solver Minisat. This generates a tracefile (.trace), documenting the steps the solver took during the solving process. Additionally, Minisat generates a .solution file containing a solution of the SAT Instance, if there is any.

The tracefile

The tracefile encodes the steps taken by Minisat in binary. The format is char followed by int32. This combination is called a block. For information how each step is encoded as a char refer to the stepFromCharacter map in satviewer/Stepper.cpp.

For the Step Types that set a variable to true or false the sign of the integer corresponds to true for positive and false for negative (e.g '+' and 1000 would set variable 1000 to true, while '+' and -1000 would set it to false).

Clauses are handled a bit differently. The start of a clause is indicated by 'L' or 'U'. Its followed by the ID of the new clause (Minisat makes sure it does not conflict with existing clauses). The next block has to have the flag 'S', indicating the start of the variable sequence. The integer denotes the amount of variables in the clause. The following blocks represent the variables that are part of the clause. The char will be 'x' and the integer contains the ID of the variable.

Clustering

Clustering is done via a python script using the python-louvain implementation of the Louvain algorithm.

Interface and Drawing

We are using Qt5 for the GUI. The graph image is rendered as an .svg by the OGDF Library.

Custom Libraries and tools

ogdfWrapper

As the name tells, this is a wrapper around the OGDF library. It simplifies access to OGDF's functions. Its purpose is to hold and manage a graph instance. It can

• read a graph from a .gml file
• write/render the graph to .gml and .svg
• layout the graph using different layout algorithms
• set color, shape and size of nodes
• add and remove nodes/edges
• set height of nodes, useful for rendering order

scripts

• cligToCNF converts a clause-literal-incidence-graph in .csv format to .cnf format.
• cnfToGML converts a SAT instance in .cnf (DIMACS) format to .gml
• vigToGML converts a variable-incidence-graph in .csv format to .gml format.
• louvain_clustering calculates a clustering on a graph in .gml format using the louvain community detection algorithm. The output format is a text file with [node id] [cluster number] in each line.