ApproxMC original version

AUTHORS

@@ -0,0 +1,19 @@
+Kuldeep S. Meel (kuldeep@rice.edu) 
+
+ApproxMC is based on our CP'13 paper:
+
+A scalable approximate model counter
+S Chakraborty, KS Meel, MY Vardi - Principles and Practice of Constraint Programming, 2013
+
+People whose code has been incorporated:
+- Niklas Eén
+- Niklas Sörensson
+- Mate Soos
+
+Special thanks to:
+- Mate Soos
+- Sean Doyle
+
+Bug-hunting thanks to:
+- William Hung, Synopsys
+- Daniel Fremont, UCB

LICENSE-MIT

@@ -0,0 +1,20 @@
+ApproxMC --Copyright (c) 2014-2016 Kuldeep S Meel
+
+Permission is hereby granted, free of charge, to any person obtaining a
+copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS
+OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
+WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

README.md

@@ -0,0 +1,45 @@
+# ApproxMC #
+
+### What is it? ###
+ApproxMC2 is an approximate model counter for CNF formulas based on our IJCAI-16  paper: http://www.comp.nus.edu.sg/~meel/Papers/ijcai16_counting.pdf
+
+The version 1 can be invoked by setting searchMode to 0 (Use "-h" for
+more information when running approxmc binary).
+The version 1 was based on our CP-13 paper. 
+
+For more details on our hashing-based approach to sampling and counting, please visit: http://www.kuldeepmeel.com
+
+### The Latest Version ###
+The latest version can be downloaded from [https://bitbucket.org/kuldeepmeel/approxmc](https://bitbucket.org/kuldeepmeel/approxmc).
+
+
+### Licensing ###
+ApproxMC is released under MIT License. For more details, please see the file `LICENSE`. 
+
+## USAGE ##
+
+```
+#!shell
+
+ ./approxmc --epsilon=0.8 --delta=0.2 --gaussuntil=400 <input file>
+
+```
+The file ProbMapFile.txt should be in the same directory from which
+approxmc is being invoked. 
+Both epsilon and delta should be floats between 0 and 1.
+Epsilon represents the accuracy of the result with respect to the
+exact answer. (1-delta) is the confidence.
+
+ApproxMC, run on a given CNF file, returns an approximate #SAT result, within epsilon percent of the exact count, with a confidence of (1-delta).
+
+
+### Questions/Feedback/Comments ###
+Report issues using bitbucket. Please do not email me. 
+
+### Contact ###
+
+
+  1. Kuldeep Meel ([kuldeep@rice.edu](mailto:kuldeep@rice.edu))
+
+
+Enjoy!

approx/INSTALL

@@ -0,0 +1,75 @@
+
+-----------
+GCC bug
+----------
+Beware, GCC has a bug affecting propagation in UniGen:
+
+http://gcc.gnu.org/bugzilla/show_bug.cgi?id=47365
+
+This seems to affect all gcc versions 4.5.x and is latent in
+trunk of upcoming 4.6.0
+
+-----------
+Libraries needed
+-----------
+You will need the following libraries to compile the sources:
+* libz
+
+-----------------
+Building the source
+-----------------
+
+If you got your source from the GIT/SVN, then you should do the following
+before doing the above::
+* Install automake, autoconf, libtool
+* Issue 'make -f Makefile.cvs' in the root dir
+
+$ mkdir build
+$ cd build
+$ ../configure
+$ make
+
+This should produce binary "approxmc" in the build directory.  ProbMapFile_36.txt and ProbMapFile_40.txt should be present in the directory from which approxmc is being invoked.
+
+
+
+-----------------
+Specifying Independent Support or Sampling Set
+-----------------
+
+To specify Independent Support or sampling set, you can specify the set in your CNF file by using "c ind" prefix. For example if the sampling set is {10, 13, 15, 16, 25, 28, 39, 41, 43, 45, 5, 53, 6, 69, 78, 9, 93}
+
+c ind 10 13 15 16 25 28 39 41 43 45 0
+c ind 5 53 6 69 78 9 93 0
+
+Note that each "c ind" line can list only 10 variables at most, followed by a closing '0'.
+
+
+----------------
+Running ApproxMC
+----------------
+$ ./approxmc --epsilon=0.8 --delta=0.02 <input file>
+
+Both epsilon and delta should be floats between 0 and 1.
+Epsilon represents the accuracy of the result with respect to the
+exact answer. (1-delta) is the confidence.
+
+ProbMapFile_36.txt and ProbMapFile_40.txt should be present in the directory from which approxmc is being invoked.
+
+
+--------------
+Verbose debug
+-------------
+You can also turn on verbose debugging.
+Simply remove the comment before 
+
+"//#define VERBOSE_DEBUG" 
+in Solver/constants.h and re-compile
+
+When executing:
+
+'./approxmc satfile.cnf'
+You will see a LOT of debug info. You should therefore maybe do:
+
+'./approxmc satfile.cnf > debuginfo.txt'
+then you can open the 'debuginfo.txt' file from a text editor and have a look

approx/Makefile.am

@@ -0,0 +1,12 @@
+# not a GNU package. You can remove this line, if
+# have all needed files, that a GNU package needs
+AUTOMAKE_OPTIONS = foreign 1.4
+ACLOCAL_AMFLAGS = -I m4
+
+SUBDIRS = cmsat man
+EXTRA_DIST = HOWTO_VisualCpp HOWTO_MinGW32 \
+	       LICENSE-MIT TODO
+
+all-local: cmsat
+	cp cmsat/approxmc .
+

approx/Makefile.cvs

@@ -0,0 +1,10 @@
+default: all
+
+all:
+	aclocal
+	autoheader
+	libtoolize --copy
+	automake --copy --add-missing
+	automake
+	autoconf
+

approx/ProbMapFile_36.txt

@@ -0,0 +1,70 @@
+1:0.64
+2:0.4096
+3:0.704512
+4:0.54525952
+5:0.7491026944
+6:0.62679678976
+7:0.783348347699
+8:0.684720866198
+9:0.81096404252
+10:0.729158464263
+11:0.833869604432
+12:0.76476025192
+13:0.853220223135
+14:0.794078413808
+15:0.869779929746
+16:0.818681406488
+17:0.884087516258
+18:0.839611361615
+19:0.896540839559
+20:0.857601076645
+21:0.907443973174
+22:0.873188309741
+23:0.917035558936
+24:0.886780956992
+25:0.92550684748
+26:0.898696615603
+27:0.933013712405
+28:0.90918784234
+29:0.939684956024
+30:0.9184589649
+31:0.945628233538
+32:0.926677668663
+33:0.950934391703
+34:0.933983222896
+35:0.955680718969
+36:0.940492471718
+37:0.9599334282
+38:0.946304294498
+39:0.963749585636
+40:0.951502991257
+41:0.967178632062
+42:0.956160895954
+43:0.970263598173
+44:0.960340424066
+45:0.973042086923
+46:0.964095698302
+47:0.975547075737
+48:0.967473854645
+49:0.977807577642
+50:0.970516102695
+51:0.979849190627
+52:0.973258594688
+53:0.98169455749
+54:0.975733143777
+55:0.98336375333
+56:0.977967822289
+57:0.984874614022
+58:0.979987463458
+59:0.98624301618
+60:0.981814084853
+61:0.987483116952
+62:0.983467247761
+63:0.988607560325
+64:0.984964363796
+65:0.989627655353
+66:0.986320957703
+67:0.990553530695
+68:0.98755089362
+69:0.991394269076
+70:0.988666570609

approx/ProbMapFile_40.txt

@@ -0,0 +1,50 @@
+1:0.6
+2:0.36
+3:0.648
+4:0.4752
+5:0.68256
+6:0.54432
+7:0.710208
+8:0.5940864
+9:0.73343232
+10:0.6331032576
+11:0.75349813248
+12:0.665208557568
+13:0.771156047462
+14:0.692452197827
+15:0.78689681739
+16:0.716063352717
+17:0.801063510324
+18:0.736841169021
+19:0.813907978585
+20:0.755337203316
+21:0.825622133638
+22:0.771950005029
+23:0.83635655936
+24:0.786978201039
+25:0.846232231024
+26:0.800652207959
+27:0.855348235637
+28:0.813154157143
+29:0.863787051336
+30:0.824630946493
+31:0.871618272305
+32:0.835203094801
+33:0.878901307806
+34:0.844970930649
+35:0.885687383237
+36:0.854019031224
+37:0.89202105364
+38:0.862419478284
+39:0.897941368711
+40:0.870234294178
+41:0.903482783617
+42:0.877517296627
+43:0.908675881015
+44:0.884315533221
+45:0.913547950574
+46:0.890670406558
+47:0.918123459377
+48:0.896618568002
+49:0.922424437652
+50:0.902192635847