Skip to content

A work in progress proof checker for LRAT files written in Lean.

Notifications You must be signed in to change notification settings

joehendrix/lean-sat-checker

Folders and files

NameName
Last commit message
Last commit date

Latest commit

81e297f · Apr 18, 2022

History

9 Commits
Apr 18, 2022
Mar 19, 2021
Apr 18, 2022
Apr 18, 2022
Apr 18, 2022
Apr 18, 2022
Apr 18, 2022
Apr 18, 2022
Mar 16, 2021

Repository files navigation

Lean SAT Proof Checker

This is an exploratory effort to build a proof checker for various formats used by the SAT community. Currently, we have focused on the LRAT SAT Proof format.

Building

To build the tool, you should follow the instructions in the Lean manual for installing Lean 4 including the lake build tool. The main binary can then be built by running:

% lake build

This will put the binary in ./build/bin/sat-checker.

Checking a DIMACS file

To check if a dimacs file is valid, you can use the dimacs command:

% ./build/bin/sat-checker dimacs <dimacsPath>

Checking a lrat proof

To check a proof, use the lrat command:

% ./build/bin/sat-checker lrat <dimacsFile> <lratFile>

As an example, this checks one of the handcrafted proofs:

% ./build/bin/sat-checker lrat examples/handcrafted/lrat-fig1.dimacs examples/handcrafted/lrat-fig1.lrat

About

A work in progress proof checker for LRAT files written in Lean.

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages