search

conp-solutions / riss

Riss SAT Solver
GNU Lesser General Public License v2.1
8 stars 5 forks source link

coprocessor_for_modelcounting.sh changes model count #25

Open AntonReinhard opened 2 years ago

AntonReinhard commented 2 years ago

The script for the model count preserving version of Coprocessor does not actually always preserve the model count. For example, on the instances track1_004 and track1_005 from the 2020 model counting competition, the model count increases by some orders of magnitude. I verified the model counts using sharpsat-td and d4, which both agree. The log10 model count of 004 changes from roughly 411.8 to 427.3. As far as I can see, the model counts only ever increase through preprocessing.

AntonReinhard commented 2 years ago

Using the flags -no-dense -no-unhide -no-bve -no-bce instead of only -no-dense in the script seems to keep model count equivalence.

conp-solutions commented 2 years ago

I see, thanks for raising this.I take any command lines you tested. BCE is known to change the model, and should be turned off.BVE should not change the models in certain cases, namely when the eliminated variable is a definition of the eliminated clauses. I likely have no flag today to only eliminate those. However, the gate detection should be ther. Feel free to create an issue of this. Thanks!Am 04.08.2022 18:48 schrieb Anton Reinhard @.***>: Using the flags -no-dense -no-unhide -no-bve -no-bce instead of only -no-dense in the script seems to keep model count equivalence.

—Reply to this email directly, view it on GitHub, or unsubscribe.You are receiving this because you are subscribed to this thread.Message ID: @.***>

AntonReinhard commented 2 years ago

After more testing, it seems -no-xor and -no-ee are also necessary in a few cases for model count equivalence.