meelgroup
Release ApproxMC7
Upgrade ApproxMC6 to ApproxMC7 following our recent work:
Towards Real-Time Approximate Counting Yash Pote ⓡ Kuldeep S. Meel ⓡ Jiong Yang Annual AAAI Conference on Artificial Intelligence (AAAI 2025) ⓡ random order
ApproxMC7 enables the use of a single SAT call to check the cell size under the current approximation scheme, significantly reducing the total number of SAT calls while maintaining the same guarantees as ApproxMC6 in the constant-factor regime.
This commit enables ApproMC7 when epsilon >= 5 and falls back to ApproxMC6 otherwise. While ApproxMC7 is theoretically sound for epsilon > 1, our current experiments indicate that it consistently outperforms ApproxMC6 when epsilon > 5. Hence, epsilon > 5 serves as a conservative threshold based on current empirical evidence. We plan to relax this threshold once more fine-grained experiments are conducted.
@kuldeepmeel Can you please help out? I don't have the time to keep in mind to check up on code all the time for people who fail to respond for weeks. Either this is done well, or it doesn't get merged in.
Notice that:
- README hasn't been updated for the new version, and the paper hasn't been linked in to README. You are not even advertising your changes.
- Version number hasn't been bumped, which is necessary for a new release. See CMakeLists.txt
- People don't care about improvements unless they are made easily accessible. The epsilon is not above 5 by default. This needs to be explained in the README: both what it means and how it helps. I strongly suggest to also explain, in a 1-liner, all the other improvements since AppMC2, in a single line, with a link to the paper, at the end of the README. This way there is a documentation of what happened and how it helps the users.
As noted above, that big if-then-else switch needs explanation. You wrote all these improvements, spent months working on them and getting their corresponding papers accepted. I think it would make sense to collect them into a list. It's actually unclear as-is what the improvements were, and how they helped. Yes, this means actual work on the README. However, you clearly spent the time on all these papers, which are many-many pages long. All I'm asking is a short sentence and link to each. I think it's very-very reasonable to do this. Yes, you need to actually sit down and think about how to do this well. However, this is the price to be paid in order to release code. It's real work, not some secondary afterthought.
Out in the real world, nobody cares about a paper, only how they can make use of it. And the README and a new released binary is mostly how people interact with it.
Clearly you are not interested in any of this -- this is just a paper mill for you. You don't seem to care about the users, as you fail to even mention you are releasing it in the README, or care to explain how to make use of it in the README. Also, I don't see even a trace of this having gone through fuzzing. I see this is a joke to you, but it's not to me.
Closing. When you are ready to actually care about the work you do, beyond the h-index, let me know.
Hi Mate,
I'm using SharpVelvet to fuzz ApproxMC7. Following these instructions, I could generate 200 instances for fuzzing, but the script failed to retrieve results from ApproxMC's output. I received the following message on each instance.
[SharpVelvet]: Counter approxmc reports count None
I added intermediate outputs inside the fuzzing script, and it turned out that ApproxMC7 runs normally, but the script src/fuzzer_utils.py seemingly could not parse ApproxMC's output properly.
Have you ever used SharpVelvet to fuzz ApproxMC (the main branch version)? Do you know whether the fuzzer can parse the ApproxMC's standard output format as below?
c o [appmc+arjun] Total time: 0.00
c [appmc] Number of solutions is: 1*2**13*1
s SATISFIABLE
s mc 8192
Here is the configuration file I used in SharpVelvet.
$ cat generator_config_mc.json
{
"biere-mc": {
"path":"/path/to/SharpVelvet/generators/biere-fuzz",
"config":"{seed} 0 > {out_file}"
},
"brummayer-mc": {
"path":"/path/to/SharpVelvet/generators/cnf-fuzz-brummayer.py",
"config":"-I 21 -s {seed} -T 0 > {out_file}"
}
}
$ cat counter_config_mc.json
{
"approxmc": {
"path":"/path/to/approxmc",
"config":"--epsilon 13",
"exact":"False"
}
}
Hi! Nice work! I think you'll need to adjust it to parse the output. Maybe you can write to Anna or maybe you can do it yourself? I use my own fork of SharpVelvet but it's a good idea to fix the mainline. Perhaps talk with Anna or have a go at fixing it yourself?
Mate
Can you please try again to fuzz this? I really wanna merge, but you used fibonacci again, and it's EXTREMELY prone to bugs, and hardly anyone understands it. @kuldeepmeel claimed to have proven it correct (which I believe), but we could find a bug in the implementation with Anna. Proving something on paper and implementing it in code are not the same things. So it needs to be fuzzed.
Fixing the parser of SharpVelvet is probably not too hard? Can you please have another go at this? Thanks!
OK, I'll do this. It's absolutely trivial to do, just see [email protected]:meelgroup/count_fuzzer.git and run that. An AI agent will make this work in under 10 minutes. No idea why 2 people with a PhD can't do it.
Towards Real-Time Approximate Counting Yash Pote ⓡ Kuldeep S. Meel ⓡ Jiong Yang Annual AAAI Conference on Artificial Intelligence (AAAI 2025) ⓡ random order
Glad you managed to self-promote. Just forgot to do the work. Classic.
Aaaaand I was right in asking for fuzz testing. Took less than 10 minutes, as promised: bug.cnf.gz
--> Executing: ../approxmc/build/approxmc --epsilon 6 --delta 0.2 -s 42 /home/soos/development/sat_solvers/count_fuzzer/out/fuzzTest_970.cnf in dir None
ERROR in output: Internal ERROR: Something is VERY fishy, the difference between each count must never be this large. Please report this bug to the maintainers
Setting resource limit in child (pid 366274)
c o CMS SHA1: b7c039ffb0451d366893cdbcd9e8e818ac1adff4
c o Arjun SHA1: 6c31a24f9e9d050a01fec2f6a5642c89b06bb5ea
c o Arjun SBVA SHA1: 4c165231a296bee923ae502fe868ad521b252a3c
c o ApproxMC SHA1: dafad35bc9da02f1404da220c6b9ed03cf67a576
c o Using VMTF, picosat, CaDiCaL, and CadiBack code by Armin Biere
c o CMS is MIT licensed
c o Using code from 'When Boolean Satisfiability Meets Gauss-E. in a Simplex Way'
c o by C.-S. Han and J.-H. Roland Jiang in CAV 2012. Fixes by M. Soos
c o Using CCAnr from 'CCAnr: A Conf. Checking Based Local Search Solver [...]'
c o by Shaowei Cai, Chuan Luo, and Kaile Su, SAT 2015
c o Using Oracle code from 'Integrating Tree Decompositions [...]'
c o by Tuukka Korhonen and Matti Jarvisalo, CP 2021
c o Using ideas by JM Lagniez, and Pierre Marquis
c o from paper 'Improving Model Counting [..] IJCAI 2016
c o executed with command line: ../approxmc/build/approxmc --epsilon 6 --delta 0.2 -s 42 /home/soos/development/sat_solvers/count_fuzzer/out/fuzzTest_970.cnf
c o --> Executing strategy token: clean-cls
c o --> Executing strategy token: must-scc-vrepl
c o [scc] new: 0 BP 0M T: 0.00
c o [vrep] vars 0 lits 0 rem-bin-cls 0 rem-long-cls 0 BP 0M T: 0.00
c o [consolidate] mini T: 0.00
c o global_timeout_multiplier: 2.5
c o [branch] rebuilding order heap for all branchings. Current branching: vsid
c o [arjun-simp] probing all sampling variables
c o --> Executing strategy token: must-scc-vrepl
c o [scc] new: 0 BP 0M T: 0.00
c o [vrep] vars 0 lits 0 rem-bin-cls 0 rem-long-cls 0 BP 0M T: 0.00
c o [consolidate] mini T: 0.00
c o global_timeout_multiplier: 2.5
c o [branch] rebuilding order heap for all branchings. Current branching: vsid
c o [arjun-simp] Removed set : 0 new size: 33
c o [arjun-simp] Removed eq lits: 0 new size: 33
c o [arjun-simp] probe removed: 0 perc: 0.00 T: 0.00
c o [arjun-simp] Removed eq lits: 0 new size: 33
c o [arjun-simp] Removed set : 0 new size: 33
c o [arjun-simp] get-empties removed: 0 perc: 0.00 total empties now: 0 T: 0.00
c o [arjun-simp] CMS::simplify() with no BVE, intree probe...
c o [arjun-simp] Removed set : 0 new size: 33
c o [arjun-simp] CMS::simplify() with no BVE finished. T: 0.00
c o WARNING: Turning off gates, because the sampling size is small, so we can just do it. Size: 33
c o [arjun-simp] Removed eq lits: 0 new size: 33
c o [arjun-simp] Removed set : 0 new size: 33
c o [arjun-simp] get-empties removed: 0 perc: 0.00 total empties now: 0 T: 0.00
c o [arjun-simp] probing all sampling variables
c o [arjun-simp] Removed set : 0 new size: 33
c o [arjun-simp] Removed eq lits: 0 new size: 33
c o [arjun-simp] probe removed: 0 perc: 0.00 T: 0.00
c o [arjun-simp] Removed eq lits: 0 new size: 33
c o [arjun-simp] Removed set : 0 new size: 33
c o [arjun-simp] get-empties removed: 0 perc: 0.00 total empties now: 0 T: 0.00
c o [arjun] simplification finished removed: 0 perc: 0.00 T: 0.00
c o [arjun] Duplicating CNF...
c o [arjun] Duplicated CNF. T: 0.00
c o [arjun] CMS::simplify() with *only* BVE...
c o [arjun] CMS::simplify() with *only* BVE finished. T: 0.00
c o [arjun] Adding fixed clauses time: 0.00
c o [arjun] Start unknown size: 33
c o [arjun] backward round finished. U: I: 33 T: 0.00
c o [arjun] run_minimize_indep finished T: 0.00
c o ind 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 0
c o [arjun] final set size: 33 percent of original: 100.0000 %
c o [arjun] Arjun finished. T: 0.0010
c o [appmc] Sampling set size: 33
c o [appmc] Sampling set: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 0
c o [appmc] threshold set to 25 sparse: 0
c o [appmc] Starting at hash count: 0
c o [appmc] [ 0.00 ] round: 0 hashes: 0
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 0
c o [appmc] repeat solutions: 0 checked: 0 out of: 0
c o [appmc] [ 0.00 ] round: 0 hashes: 1
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 1
c o [appmc] repeat solutions: 1 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 0 hashes: 2
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 2
c o [appmc] repeat solutions: 1 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 0 hashes: 4
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 4
c o [appmc] repeat solutions: 1 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 0 hashes: 8
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 8
c o [appmc] repeat solutions: 0 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 0 hashes: 16
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 16
c o [appmc] repeat solutions: 0 checked: 2 out of: 2
c o [appmc] [ 0.00 ] round: 0 hashes: 32
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 32
c o [appmc] repeat solutions: 0 checked: 3 out of: 3
c o [appmc] [ 0.00 ] round: 0 hashes: 24
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 24
c o [appmc] repeat solutions: 0 checked: 3 out of: 3
c o [appmc] [ 0.00 ] round: 0 hashes: 20
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 20
c o [appmc] repeat solutions: 0 checked: 3 out of: 3
c o [appmc] [ 0.00 ] round: 0 hashes: 18
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 18
c o [appmc] repeat solutions: 0 checked: 3 out of: 3
c o [appmc] [ 0.00 ] round: 0 hashes: 17
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 17
c o [appmc] repeat solutions: 0 checked: 3 out of: 3
c o [appmc] simplifying
c o [appmc] [ 0.00 ] round: 1 hashes: 16
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 16
c o [appmc] repeat solutions: 0 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 1 hashes: 17
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 17
c o [appmc] repeat solutions: 1 checked: 2 out of: 2
c o [appmc] [ 0.00 ] round: 1 hashes: 18
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 18
c o [appmc] repeat solutions: 1 checked: 2 out of: 2
c o [appmc] [ 0.00 ] round: 1 hashes: 19
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 19
c o [appmc] repeat solutions: 0 checked: 2 out of: 2
c o [appmc] [ 0.00 ] round: 1 hashes: 21
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 21
c o [appmc] repeat solutions: 1 checked: 3 out of: 3
c o [appmc] [ 0.00 ] round: 1 hashes: 25
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 25
c o [appmc] repeat solutions: 0 checked: 3 out of: 3
c o [appmc] [ 0.00 ] round: 1 hashes: 23
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 23
c o [appmc] repeat solutions: 1 checked: 3 out of: 3
c o [appmc] [ 0.00 ] round: 1 hashes: 24
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 24
c o [appmc] repeat solutions: 0 checked: 3 out of: 3
c o [appmc] simplifying
c o [appmc] [ 0.00 ] round: 2 hashes: 23
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 23
c o [appmc] repeat solutions: 0 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 2 hashes: 22
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 22
c o [appmc] repeat solutions: 0 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 2 hashes: 21
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 21
c o [appmc] repeat solutions: 0 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 2 hashes: 20
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 20
c o [appmc] repeat solutions: 0 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 2 hashes: 10
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 10
c o [appmc] repeat solutions: 0 checked: 1 out of: 1
c o [appmc] [ 0.00 ] round: 2 hashes: 15
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 15
c o [appmc] repeat solutions: 0 checked: 2 out of: 2
c o [appmc] [ 0.00 ] round: 2 hashes: 12
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 12
c o [appmc] repeat solutions: 0 checked: 2 out of: 2
c o [appmc] [ 0.00 ] round: 2 hashes: 13
c o [appmc] [ 0.00 ] bounded_sol_count looking for 1 solutions -- hashes active: 13
c o [appmc] repeat solutions: 0 checked: 3 out of: 3
Internal ERROR: Something is VERY fishy, the difference between each count must never be this large. Please report this bug to the maintainers
Error running Solver(exe='../approxmc/build/approxmc --epsilon 6 --delta 0.2 ', exact=False, dir=None)
Now get your stuff together and fix this. File attached. And just run the fuzzer, what's so hard in typing ./fuzz.py --unweighted ? Just need a compiled ganak, and a compiled approxmc. You can even get both from the GitHub Actions that I created.