/lidrup-visualiser

Python Script for visualisation of LIDRUP proofs.

Primary LanguagePythonMIT LicenseMIT

LIDRUP Visualizer

A Python script for visualizing LIDRUP proofs generated by incremental SAT solvers.

For more details on the proof format, see: [1] Katalin Fazekas, Florian Pollitt, Mathias Fleury, Armin Biere: Certifying Incremental SAT Solving. LPAR 2024: 321-340

Features

  • Visualizes LIDRUP proofs
  • Supports various graph types for comprehensive analysis
  • Option to save generated figures automatically
  • Customizable legend display

Installation

git clone https://github.com/kfazekas/lidrup-visualizer.git
cd lidrup-visualizer
pip install -r requirements.txt

Usage

python3 lidrup-visualizer.py [OPTIONS] PROOF-FILENAME

Options

  • --save: Automatically save the figure as a PNG file (filename derived from input)
  • --no-legend: Hide the legend for a less cluttered figure

Examples

  1. Generate and display a visualization:

    python3 lidrup-visualizer.py input_file.lidrup

  2. Generate, display, and save a visualization without legend:

    python3 lidrup-visualizer.py --save --no-legend input_file.lidrup

Graph Explanation

The visualizer generates up to four columns of graphs, each providing different insights:

  1. Clause Weakening and Restoration (leftmost column, if applicable)

    • Top: Number of weakened clauses
    • Bottom: Number of restored clauses
    • Color coding indicates the number of solve() queries between operations

  2. Clause Operation Frequency (second column)

    • Top: Frequency of clause weakening
    • Bottom: Frequency of clause restoration

  3. Clause Addition and Query Results (third column)

    • Top: Number of clauses added per solve() query (IPASIR-UP inputs vs. IPASIR inputs)
    • Bottom: Query results (SAT/UNSAT) and literal counts (assumed/core)

  4. Variable Usage in Assumptions (rightmost column)

    • Variables used in query assumptions
    • Color indicates polarity (red: positive, blue: negative)
    • Shade indicates presence in UNSAT core (darker: present)

Example Visualizations

BMC (Bounded Model Checking) Interaction

BMC example

MaxSAT Solver Interaction

MaxSAT example

Note: The MaxSAT example shows a different pattern in assumptions and query results compared to the BMC example, and does not include weakened or restored clauses.

License

This project is licensed under the MIT License - see the LICENSE file for details.

Acknowledgement

This work was funded by the Austrian Science Fund (FWF) under project No. T-1306.