This repository contains the source code to find and exploit clause dependencies for MUS enumeration.
This is not the most elegant or the most efficient code, and the output is a mess -- you've been warned.
We are submitting a paper to SAT'2020. So we also include benchmarks and experimental results here.
Update (NEW): we have run additional experiments on random MUS benchmarks by Luo, ref. https://github.com/luojie-sklsde/MUS_Random_Benchmarks. The time for each MARCO was set to 300 seconds (= 5 minutes). The folder results_NEW contains these experimental results.
A Group-CNF input format is described in http://www.satcompetition.org/2011/rules.pdf.
We have extended the above format to specify "restriction clauses" using lines such as: c restrict -847 760 0
That is, any regular tool that reads GCNFS will treat the above line as a comment and simply ignore it. On the other hand, marco_with_restrictions will treat such lines differently from comments.
Here is a longer example:
p gcnf 3 6 6
{1} 1 0
{2} -1 0
{3} 2 0
{4} -2 0
{5} 3 0
{6} -3 0
c restrict -2 1 0
c restrict -1 2 0
c restrict -4 3 0
c restrict -3 4 0
c restrict -6 5 0
c restrict -5 6 0
The first 7 lines are in the usual GCNF format. Each "c restrict" line specifies restriction between groups.
Please refer to MARCO algorithm at https://sun.iwu.edu/~mliffito/marco.
marco_with_restrictions is a minor modification of the above, which allows: - parsing GCNFs with restriction clauses and passing restriction clauses to msolver - disabling the check if seed is explored (not valid with restrictions) - minor output tweaks
On the above example, marco_with_restriction will add the clauses (-2, 1), (-1, 2), (-4, 3), (4, -3), (-6, 5) and (6, -5) to the map-solver in MARCO.
to compile: marco_with_restrictions should be compiled in exactly the same way as marco.
to run [example]: python3 -u marco_with_restrictions/marco.py --print-mcses -T 3600 -s -a -v -v ssa2670-129.cnf
lve_restrict reads a CNF or a GCNF formula and discovers dependencies between clauses (or groups) in the sense of the submitted SAT'2020 paper. With -output=..., it writes the GCNF with discovered restrictions (which can be used as an input to marco_with_restrictions)
It is a rather small hack on top of minisat/simp.
lve_restrict/minisat_* - reads a CNF, GCNF, or GCNF with restrictions (however, ignores all restrictions) - finds restrictions - writes a GCNF with restrictions
- options:
-grow, -cl-lim: controls the effort spent on VE
(ex. -grow=40 -cl-lim=200)
-verb: verbosity
-time: specifies the time for VE
-output: name of the output file
-max: allows to restrict the number of binary implications
-reduce: reduce binary implications
-redundant: handling redundant groups (0 - nothing, 1 - remove, 2 - relabel as group-0)
-eq-only: only equivalences
-lve-only: does not analyze restrictions (only necessary and redudant groups)
-outputs: name of the simplified output file
- __To compile__:
./build.sh
- __To run__:
lve_restrict/lverestrict <input>.cnf -output=<output>.gcnf -param=<value>
__Example__:
*lve_restrict/lverestrict tests/ssa2670-129.cnf -lve-only -redundant=1 -output=aaa2*
bce_restrict reads a CNF or a GCNF formula and discovers dependencies between clauses (or groups) in the sense of the submitted SAT'2020 paper. With -output ..., it writes the GCNF with discovered restrictions (which can be used as an input to marco_with_restrictions)
bce_restrict: - reads a CNF, GCNF, or GCNF with restrictions (however, for now only positive unit restrictions are used) - finds restrictions - writes a GCNF with restrictions
- options:
-bce-only: does only top-level BCE
-bce-skip: skips top-level BCE
-verb: verbosity
-time: specifies the time for VE
-output: name of the output file
-max: allows to restrict the number of binary implications
-reduce: reduce binary implications
-redundant: handling redundant groups (0 - nothing, 1 - remove, 2 - relabel as group-0)
-eq-only: only equivalences
- __to compile__:
*./build.sh*
- __to run__:
*bce_restrict/bcerestrict <input>.cnf -output <output>.gcnf -param <value>*
__Example__:
*bce_restrict/bcerestrict tests/ssa2670-129.cnf -bce-only 1 -redundant 1 -output aaa1*
Located in benchmarks/
cnf: the original 11 benchmarks from the MUS track of the 2011 SAT competition
bce: the original 11 benchmrks together with restriction clauses found by bce_restrict
lve: the original 11 benchmrks together with restriction clauses found by lve_restrict
Located in results/
bce_output: output of bce_restrict on benchmarks from cnf (i.e. this is how bce benchmarks are produced)
lve_output: output of lve_restrict on benchmarks from cnf (i.e. this is how lve benchmarks are produced)
marco_on_cnf_output: output of marco_with_restrictions when running on benchmarks from cnf
marco_on_bce_output: output of marco_with_restrictions when running on benchmarks from bce
marco_on_lve_output: output of marco_with_restrictions when running on benchmarks from lve
Update (NEW): we have run additional experiments on the MUS_Random_Benchmarks suite by Luo, ref. https://github.com/luojie-sklsde/MUS_Random_Benchmarks. The time for each MARCO was set to 300 seconds (= 5 minutes). We would like to thank an (anonymous) reviewer for pointing us to these benchmarks. These new results are located in results_NEW / marco_variations_on_random_formulas.xlsx.