Solving SAT takes forever about perin HOT 2 OPEN

Hi, thanks for using PERIN! Generally, solving the SAT problem can take a couple of hours and it’s quite possible that the algorithm will not be able to find any solution in a reasonable time for a custom dataset. The SAT heuristics can be very unpredictable. Are you using the official AMR dataset from MRP2020 or some other one?

You can also use a greedy search for a suboptimal solution, for this exact reason. Just call the function get_smallest_rule_set with approximate=True and it will run a faster algorithm. The solution will not be as good, but it shouldn't lead to any significant performance drop.

from perin.

Thanks for your prompt rely. I'm using MRP2020_Train_Dev-2020CoNLL_CFMRP_LDC2020E05.tgz from LDC, which might not be exactly the same with the one used in MRP2020 competion. Maybe split_dataset.sh creates random split too?

I'll try approximate=True and other solvers.

from perin.