How to convert DRAT/DRUP to LRAT? #29
Comments
|
On Sun, Feb 06, 2022 at 10:47:21PM -0800, DennisYurichev wrote:
I'm trying to convert DRAT proof produced by Kissat to LRAT to see if it can be verified in ACL2.
Am I doing this right?
unsat1.cnf:
p cnf 1 2
1 0
-1 0
Running:
% kissat unsat1.cnf unsat1.drat
% xxd -g 1 unsat1.drat
00000000: 61 00 61 00 64 03 00 a.a.d..
Attempting to generate LRAT proof from DRAT proof.
Am I doing this right?
% ./drat-trim unsat1.cnf unsat1.drat -l unsat1.lrat
You want -L instead of -l
Both write an optimized/trimmed proof with only core lemmas but -l uses DRAT
whereas -L uses LRAT (which adds clause numbering and hints how to derive
each lemma).
c turning on binary mode checking
c parsing input formula with 1 variables and 2 clauses
c WARNING: backward mode ignores deletion of (pseudo) unit clause [0] -1 0
c finished parsing, read 7 bytes from proof file
c found complementary unit clauses: -1
s VERIFIED
c verification time: 0.143 seconds
unsat1.lrat:
0
Right, it should be something like
3 0 1 2 0
|
|
Thanks a lot. But still can't run ACL2... unsat1.cnf: unsat1.lrat: /home/i/Downloads/acl2/books/projects/sat/lrat/stobj-based unsat1.out: |
|
On Mon, Feb 07, 2022 at 12:27:35AM -0800, DennisYurichev wrote:
% ./run.sh ~/Downloads/drat-trim/unsat1.cnf ~/Downloads/drat-trim/unsat1.lrat
s FAILED
(see /home/i/Downloads/drat-trim/unsat1.out)
unsat1.out:
"HARD ACL2 ERROR in VALID-PROOFP$-TOP: Invalid proof!"
This is really strange, it works fine for me.
Here is what I did starting from a clean checkout of acl2 ("git clean -dxf"
works nicely, obviously use with caution).
#!/bin/sh
set -e
git describe # just in case, should also work with 7.0
# 8.3-9034-g2296010cb1
make LISP=$(command -v sbcl)
acl2=$PWD/saved_acl2
cert=$PWD/books/build/cert.pl
cd books/projects/sat/lrat
"$cert" -j`nproc` --acl2 "$acl2" */*.lisp
cd stobj-based
"$acl2" <<EOF
(include-book "run")
:q
(save-exec
"lrat-check"
"Large executable including run.lisp, saved with --dynamic-space-size 240000"
:host-lisp-args "--dynamic-space-size 240000"
)
EOF
cat > unsat1.cnf <<EOF
p cnf 1 2
1 0
-1 0
EOF
cat > unsat1.lrat <<EOF
3 0 1 2 0
EOF
./run.sh unsat1.cnf unsat1.lrat
# s VERIFIED
# (see unsat1.out)
|
|
Something utterly wrong. I did like you wrote. I even made unsat1.cnf/lrat files using command line, as you did. Weird, but at the same moment, tests that comes with acl2, passed: |
|
Ohhhhh! *.cnf and *.lrat files MUST NOT contain trailing empty line. Probably, this ACL2 module author's should be notified... Thanks for your help. |
|
Follow-up: probably another bug? acl2/acl2#1355 |
|
Filed an issue: acl2/acl2#1359 |
|
@krobelus Know something about that? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
I'm trying to convert DRAT proof produced by Kissat to LRAT to see if it can be verified in ACL2.
Am I doing this right?
unsat1.cnf:
Running:
Attempting to generate LRAT proof from DRAT proof.
Am I doing this right?
unsat1.lrat:
Running:
Trying to verify LRAT proof in ACL2:
Stdout:
unsat1.out:
The text was updated successfully, but these errors were encountered: