[Enhancement ask] Display correct LRAT resolvents for each ID

[msoos]

I am having trouble figuring out what the resolvents and their order should be after the l in the FRAT file. It would be immensely helpful if frat-rs could print out the correct order or resolutions it did that I should have put after l for it to be correct. My understanding is that frat-rs recovers this in non-strict mode (searching close to the hints given). So frat-rs knows this information already. It would be of great help if it could print it, so I would know what I should have put. I can then debug on my side to fix to have correct l after my a clauses.

No rush or anything, just an ask. Thanks and sorry for bothering you with so much of this. I am trying to move my machine-learning based system, CrystalBall to frat-rs instead of DRAT. So I will start hacking frat-rs soon enough :)

BTW, I understand that frat-rs doesn't compute this for all IDs, etc. but for the ones it does compute it, it'd be really great. Thanks!

[digama0]

FRAT has no restrictions on the order of resolvents in an l proof. For RAT steps (not RUP or PR steps), the procedure is as follows:

• Suppose the input line has the form a (c_i)* 0 l (p_i)* (-r_i (s_ij)*)* 0.
• let lit := c_0, the first literal in the input clause, which must exist.
• There is an optional list of steps p_i which apply to all resolvent proofs. These are a unit propagation proof in a context where all literals c_i except for lit are false.
• The r_i are negated clause ID references. There must be one for each clause in the context that contains -lit.
  • The s_ij are a unit propagation proof picking up where p_i left off, with a context additionally extended to add all literals in the r_i clause except for -lit.

You are asking what the requirements are for the r_i, and the answer is that if you have a clause in the context with -lit in it then it must be in the list. If there are no such clauses then it should be an empty list. (In that case a valid proof is l 0, introducing a clause whose pivot literal has no negative occurrences.) You of course need to know what the context is at that point in the proof, but I would assume that you know this from the solver context.

[msoos]

Hi,

Thanks for the explanation, this will come handy when I want to implement BVA (bounded variable addition, a form of extended resolution) to work with FRAT!

Regarding my question: sorry I was ambiguous. Let me explain. I am still just trying to create a regular RUP proof. This is normally done by frat-rs if I don't supply an l, and if I supply an l that is incomplete, it takes what I gave afterl as a hint, and fixes it up. However, in -s, i.e. strict mode, it rejects an l proof that's wrong/incomplete (in my case, missing some IDs). What I would like to have is for frat-rs to give me the l proof that it generated given my hint of l when I don't pass the -s flag. I am likely missing a few IDs from the l and when I don't pass -s, it recovers these and is happy. However, I'd like to have this list of IDs printed, so I can check what I missed, fix up my l, and have my proof be accepted in -s mode.

Say, here is a proof fragment:

a 10 1 2 0
a 11 1 -2 0
a 12 1 0 l 10 0

Here, a 12 1 0 l 10 0 is incorrect, it should be a 12 1 0 l 10 11 0. I gave a hint of l 10 0 but that's not enough, it should have been l 10 11 0. I would like for frat-rs to print

[...]
line X should have been: "a 12 1 0 l 10 11 0"
VALIDATED

Would this be possible? It would help me get -s to work and accept my proofs :) Thanks a lot in advance,

Mate

[digama0]

Oh I see. I think you can use the refrat utility to do this. Here's an example of use:

$ cat test.frat
o 1 1 2 0
o 2 1 -2 0
o 3 -1 0
a 10 1 2 0
a 11 1 -2 0
a 12 1 0 l 10 0
a 13 0
f 13 0
f 12 1 0
f 11 1 -2 0
f 10 1 2 0
f 3 -1 0
f 2 1 -2 0
f 1 1 2 0
$ target/release/frat-rs elab - test.frat 
elaborating...
parsing DIMACS...
Error: Os { code: 2, kind: NotFound, message: "No such file or directory" }
$ target/release/frat-rs refrat test.frat.temp test2.frat
$ cat test2.frat
o 1  2 1 0
o 2  -2 1 0
o 3  -1 0
a 10  2 1 0  l 3 1 2 0
d 1  2 1 0
a 11  1 -2 0  l 3 2 10 0
d 2  -2 1 0
a 13  0  l 3 10 11 3 0
d 11  1 -2 0
d 10  2 1 0
d 3  -1 0
f 13  0

(The Os error is because I gave a bogus cnf file. The elaborator pass runs to completion on the FRAT file before it attempts to open the CNF file.) This is running elab for its side effect of producing a .frat.temp file, which is then fed back to refrat to turn it into a FRAT file again, but this time with elaborated hints.

This is the same proof, but you can see that it has inserted d steps as early as possible, and the l steps are now correct. In this case the information you are looking for is the l proof associated to step 12, which is l 3 2 10 0 in this case (the unit orig step made it prefer a different proof in this case).

I had to modify frat-rs to produce this output, because by default all files it produces are in binary format and there is currently not a mechanism for changing this at run time. I will add a compile feature for this, so you can run cargo build --features=ascii to get a version that produces ascii files instead of binary.

[msoos]

Oh wow, thanks! This is amazing! I would go so far as to document this in the README, I think it's super-helpful. Thanks again, it's really great!

Mate

[msoos]

Hi! Today I wanted to use this to fix up my LRAT hints, but no luck. I seem to be getting a binary, not ascii version:

soos@vvv-dejavu:frat$ cargo clean
[[ this clears directory "target" completely ]]
soos@vvv-dejavu:frat$ cargo build --features=ascii
   Compiling libc v0.2.114
   Compiling cfg-if v1.0.0
   Compiling ppv-lite86 v0.2.16
   Compiling byteorder v1.4.3
   Compiling slab v0.4.5
   Compiling either v1.6.1
   Compiling arrayvec v0.5.2
   Compiling getrandom v0.2.4
   Compiling rand_core v0.6.3
   Compiling rand_chacha v0.3.1
   Compiling rand v0.8.4
   Compiling frat-rs v0.1.0 (/home/soos/development/sat_solvers/frat)
    Finished dev [unoptimized + debuginfo] target(s) in 5.29s

soos@vvv-dejavu:frat$ cp target/debug/frat-rs .

soos@vvv-dejavu:frat$ cat todo.sh 
#!/bin/bash
rm -f correct
./frat-rs elab a b -m -v
./frat-rs elab - b test.frat
./frat-rs refrat b.temp correct
echo "correct" created

soos@vvv-dejavu:frat$ ./todo.sh 
elaborating...
parsing DIMACS...
trimming...
verifying...
VERIFIED
elaborating...
parsing DIMACS...
Error: Os { code: 2, kind: NotFound, message: "No such file or directory" }
correct created

soos@vvv-dejavu:frat$ head correct 
o'30oWdQoYheoesuofuou�{oy��o����o����o���o���o�z�o��0o����o���o���o��to���o����o���o���o���o���o���o���ro���o����o���o����o���o���o�"��o���o���o�|��o����o��}�o����o����o����o����o����o����o����o����o���o���o���o�?�o���o���o���o���o���o���o��oo���o���o���o�P�o�3�o��"o���o���o���o���o���o���o���o���o���o����o���o���o����o���o����o����o��o���o���o�       ��o�
��o�
��o�
��o�
��o�
��o�
��oo�
��o�
��o�
���o�

soos@vvv-dejavu:frat$ hexdump correct 
0000000 276f 3033 6f00 6457 0051 596f 6568 6f00
0000010 7365 0075 666f 0275 6f00 8575 7b01 6f00
[...]

So the good news is that it does indeed create the correct proof, I think! However, it does not print it in ascii mode. I think I correctly compiled it with ascii enabled. Do you know what could be going on? Thanks in advance for checking,

Mate

[digama0]

fixed in 10784ae

[msoos]

Hi!

Thanks for the quick fix! Unfortunately, I must be doing something wrong, I think :( I am still getting a binary correct file. I am now attaching my script todo.sh along with a and b inputs. It cleans, recompiles and generates the correct file. Hopefully it reproduces the issue! I hope I am doing exactly as described, but something is off. Can you please have a look? The shell script (included) is:

#!/bin/bash
rm -f correct


cargo clean
cargo build --features=ascii

./frat-rs elab a b -m -v
./frat-rs elab - b test.frat
./frat-rs refrat b.temp correct

echo "correct" created

Thanks in advance for having a look! Again, I'm sorry. I really need to learn rust so I can fix these issues myself...

Mate

reproduce.zip

[digama0]

You are missing a cp target/debug/frat-rs . in there, or using target/debug/frat-rs instead of ./frat-rs. Most likely you are using an old version of frat-rs. You can also use cargo run -- in place of frat-rs; this will compile if necessary and call the correct binary.

After fixing that, I found another bug - the temp file has to be binary, because the temp->lrat conversion uses a binary-only parser. That shouldn't be a problem for you since you are using refrat afterward and the correct file should be a proper ascii frat file. The fix is in e66b9b6.

[msoos]

Ah, that worked, thank you so much! I knew I messed up something with using cargo. Sorry, last time I figured out I have to copy frat-rs but then I forgot :S Thanks again, this is a great help,

Mate