Skip to content

Commit

Permalink
add description for running without cadical/cake_lpr in path
Browse files Browse the repository at this point in the history
  • Loading branch information
bsubercaseaux committed Jun 9, 2024
1 parent d74e35b commit d3094c5
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,11 @@ If proof checking succeeds, you should see the following output:
s VERIFIED UNSAT
```

Moreover, if you do not have the `cadical` and `cake_lpr` executables on your path, you can pass them to the script as:
```
env CADICAL=<path to cadical> CAKELPR=<path to cake_lpr> ./verify_tautology.sh
```

Because verifying the **UNSAT proof** requires many thousands of CPU hours,
we provide a simple way to verify that any single cube is UNSAT.
To generate the formula + cube number $i$ (assuming the steps for the **tautology proof** have been followed), run `./solve_cube.sh` script in the `cube_checking/` directory, which essentially runs:
Expand Down

0 comments on commit d3094c5

Please sign in to comment.