search

curtisbright / PhysicsCheck

Other
0 stars 2 forks source link

Improve code structure and modularization #19

Closed curtisbright closed 1 year ago

curtisbright commented 1 year ago

I enabled proof generation and checking into the pipeline but found that the code is not so well structured. For example, instead of having a single solving script there are many separate calls to MapleSAT most of which use similar parameters so that should be modularized. For now, I added the verification code into main.sh to show you how it is done. A partial proof produces "s DERIVATION" if it verifies correctly and a full proof will produce "s VERIFIED" if it verifies correctly. Proofs that might be partial proofs have to be checked forwards (pass -f to DRAT-trim), not backwards like normal.

Can the code be simplified perhaps? The new extend script looks quite involved and if we are planning on relying on the partial results of the previous run to ensure the correctness of the next run that means it's not enough to just trust the proof certificates; we also have to trust the extend script!

Also, again I fixed some obvious errors that arose due to changes in the code.

BrianLi009 commented 1 year ago

Note to myself:

  1. modularize solving script
  2. test running partial and full proof
  3. simplify new cubing pipeline, need to be trusted
  4. go over the commits and double check the changes
curtisbright commented 1 year ago

I updated MapleSAT to support writing learnt unit clauses, so during iterative cubing you'll want to use -unit-out=<unit-clause-file> and -noncanonical-out=<noncanonical-blocking-file> and then append the clauses in those files to the CNF instances in the next iteration that are children of the current cube (if the current cube was not solved in the given timeout).

You can also use -max-proof-size=7168 to stop solving once the proof has reached 7GiB. On my machine this takes about an hour and the resulting proof can be verified by DRAT-trim using under 4GiB of memory.

curtisbright commented 1 year ago

You can also add clauses to the child instances blocking any KS candidates found. The following sed command may be useful to convert the assumptions in the exhaust file into blocking clauses: sed -e 's/ / -/g' -e 's/-0/0/' -e 's/a //' -e 's/--//g'