Proof-Stitch: Proof Combination for Divide-and-Conquer (D&C) SAT solvers

Description

This tool combines refutations of sub-problems generated by a D&C SAT solver into a single refutation for the original instance. It also optimizes the combined refutations to reduce their size and checking time.

Prerequisites

1. Python>=3.6.8
2. Linux-based system (Tested on CentOS)

Installation

Clone repository to any linux-based system

Usage

python3 proof_optimizer.py <CNF FILE> <DIRECTORY CONTAINING PROOFS> <OPTIMIZATION LEVEL>

CNF FILE: The file describing the SAT problem in dimacs format

DIRECTORY: The directory that contains the proof files generated by the Divide-and-Conquer solver

OPTIMIZATION LEVEL : 0 or 1 or 2
0: No Optimization
1: Intelligent Optimization
2: Full Optimization

Example

python3 proof_optimizer.py example/cnf/random_ksat.dimacs example/proof/ 0

Contributers

1. Abhishek Nair
2. Saranyu Chattopadhyay
3. Andrew Wu
4. Alex Ozdemir