diff --git a/approxmc b/approxmc new file mode 100755 index 0000000..ace68c7 Binary files /dev/null and b/approxmc differ diff --git a/maxcount.py b/maxcount.py old mode 100644 new mode 100755 index 4fdc772..ccfe937 --- a/maxcount.py +++ b/maxcount.py @@ -1,3 +1,5 @@ +#!/usr/bin/env python3 + # MaxCount 1.0.0 # An approximate Max#SAT solver # Written by Daniel Fremont and Markus Rabe @@ -12,6 +14,7 @@ import time import itertools import argparse +import re ### parse command-line arguments @@ -28,7 +31,7 @@ parser.add_argument('--seed', help='random seed to use', metavar='s', type=int, default=0) parser.add_argument('--runIndex', help='number included in temporary file names (useful for running multiple instances simultaneously)', metavar='r', type=int, default=0) parser.add_argument('--verbosity', help='information to output: 0 = max-count estimate and witness; 1 = also max-count bounds; 2 = everything', metavar='level', type=int, choices=[0,1,2], default=2) -parser.add_argument('--scalmc', help='path to scalmc binary', metavar='path', default='./scalmc') +parser.add_argument('--scalmc', help='path to scalmc binary', metavar='path', default='./approxmc') # sampling parser.add_argument('--samples', help='number of samples to generate from self-composition', metavar='n', type=int, default=20) @@ -201,6 +204,8 @@ def printV(verbosityLevel, text, withNewline=True): raise Exception('Non-integer counting variable on line '+str(lineNumber)) numCountingVars = len(countingVars) +printV(2, "c Counting vars:", countingVars) +printV(2, "c Maximisation vars:", maxVars) printV(2, 'c Formula has %d maximization and %d counting variables' % (len(maxVars), numCountingVars)) ### sample from assignments to maximization variables @@ -218,16 +223,18 @@ def sampleFromSelfComposition(): printV(2, 'c Sampling with tolerance (1+%f)... ' % sampleEpsilon, False) sys.stdout.flush() - timepoint = time.time() - sampleCommand = scalmcPath+' --cuspLogFile='+cuspLogFilename - sampleCommand += ' --multisample='+('1' if useMultisampling else '0') - sampleCommand += ' --random='+str(seed) - sampleCommand += ' --pivotAC='+str(samplingPivotAC) - sampleCommand += ' --tApproxMC='+str(samplingTApproxMC) - sampleCommand += ' --kappa='+str(kappa) - sampleCommand += ' --samples='+str(uniGenNumSamples) - sampleCommand += ' --sampleFile='+sampleFilename + sampleCommand = scalmcPath+' --log '+cuspLogFilename + sampleCommand += ' --multisample '+('1' if useMultisampling else '0') + sampleCommand += ' --seed '+str(seed) + sampleCommand += ' --threshold '+str(samplingPivotAC) # pivot AC + sampleCommand += ' --measure '+str(samplingTApproxMC) # measurements + sampleCommand += ' --kappa '+str(kappa) + sampleCommand += ' --samples '+str(uniGenNumSamples) + sampleCommand += ' --sampleout '+sampleFilename sampleCommand += ' '+kfoldFilename+' > '+outputFilename + + timepoint = time.time() + print("Running ApproxMC: %s" % sampleCommand) os.system(sampleCommand) printV(2, 'completed in %d s' % (time.time() - timepoint)) @@ -237,25 +244,29 @@ def sampleFromSelfComposition(): formulaUnsat = False with open(outputFilename, 'r') as outputFile: for line in outputFile: - if line == 'The input formula is unsatisfiable.\n': + printV(3, "ApproxMC output line is:", line.strip()) + if 'UNSAT' in line: formulaUnsat = True break if not formulaUnsat: with open(sampleFilename, 'r') as sampleFile: for line in sampleFile: - fields = line[1:].split(':')[0].split() - if fields[-1] != '0': - raise Exception('Malformed sample file from scalmc') - literals = set(map(lambda f: int(f), fields[:-1])) - sample = [] + m = re.match("(.*):(.*) 0$", line) + if m is None: + print("ERROR: Wrong sample line from sample file:", line) + exit(-1) + lits = m.group(2).strip().split(' ') + literals = set(map(lambda f: int(f), lits)) + sample_on_maxvars = [] for var in maxVars: if var in literals: - sample.append(var) + sample_on_maxvars.append(var) elif -var in literals: - sample.append(-var) + sample_on_maxvars.append(-var) else: raise Exception('Incomplete sample from scalmc') - samples.add(tuple(sample)) + printV(4, "Sample's maxVars:", sample_on_maxvars) + samples.add(tuple(sample_on_maxvars)) except IOError as e: raise Exception('Sampling did not complete successfully') @@ -287,7 +298,9 @@ def sampleFromSelfComposition(): ### count solutions for each sample # construct 1-fold self-composition and extract clauses -os.system('python selfcomposition.py 1 '+inputFilename+' > '+onefoldFilename) +torun = 'python selfcomposition.py 1 '+inputFilename+' > '+onefoldFilename +printV(2, "c Runing self composition: ", torun) +os.system(torun) clauses = [] with open(onefoldFilename, 'r') as onefoldFile: @@ -299,10 +312,10 @@ def sampleFromSelfComposition(): def countSampleWithHashing(sample, epsilon=countEpsilon, confidence=perSampleCountingConfidence): pivotAC = int(math.ceil(9.84 * (1 + (epsilon / (1.0 + epsilon))) * (1 + (1.0/epsilon)) * (1 + (1.0/epsilon)))) tApproxMC = int(math.ceil(17 * log2(3.0 / (1 - confidence)))) - countCommand = scalmcPath+' --cuspLogFile='+cuspLogFilename - countCommand += ' --random='+str(seed) - countCommand += ' --pivotAC='+str(pivotAC) - countCommand += ' --tApproxMC='+str(tApproxMC) + countCommand = scalmcPath+' --log '+cuspLogFilename + countCommand += ' --seed '+str(seed) + countCommand += ' --threshold '+str(pivotAC) + countCommand += ' --measure '+str(tApproxMC) countCommand += ' '+countFilename+' > '+outputFilename # assign maximization variables by adding unit clauses os.system('cp '+onefoldFilename+' '+countFilename) @@ -315,12 +328,13 @@ def countSampleWithHashing(sample, epsilon=countEpsilon, confidence=perSampleCou hashCount = -1 with open(outputFilename, 'r') as outputFile: for line in outputFile: - if line[:24] == 'Number of solutions is: ': + if 'Number of solutions is: ' in line: if cellCount >= 0: raise Exception('Malformed output from scalmc') - fields = line[24:].split('x') - cellCount = int(fields[0]) - hashCount = int(fields[1][3:]) + d = re.match("^.*Number of solutions is: ([^x]*) x 2.([^x]*)$", line) + assert d is not None, "ApproxMC output is weird..." + cellCount = int(d.group(1)) + hashCount = int(d.group(2)) elif line == 'The input formula is unsatisfiable.\n': if cellCount >= 0: raise Exception('Malformed output from scalmc') diff --git a/scalmc-binaries/README.md b/scalmc-binaries/README.md deleted file mode 100644 index b4d024c..0000000 --- a/scalmc-binaries/README.md +++ /dev/null @@ -1,8 +0,0 @@ -# scalmc binaries - -Here are _scalmc_ binaries compiled for various platforms. -Pick the appropriate one for your system and move it into the same directory as the Python scripts. - -* __x86_64-apple-darwin__: for 64-bit Macs; tested under macOS 10.12.5 - -* __x86_64-linux__: for 64-bit Linux; tested under Ubuntu 16.04 \ No newline at end of file diff --git a/scalmc-binaries/x86_64-apple-darwin/scalmc b/scalmc-binaries/x86_64-apple-darwin/scalmc deleted file mode 100755 index 76b1f8c..0000000 Binary files a/scalmc-binaries/x86_64-apple-darwin/scalmc and /dev/null differ diff --git a/scalmc-binaries/x86_64-linux/scalmc b/scalmc-binaries/x86_64-linux/scalmc deleted file mode 100755 index 023b85c..0000000 Binary files a/scalmc-binaries/x86_64-linux/scalmc and /dev/null differ