Skip to content

Latest commit

 

History

History
549 lines (474 loc) · 21.2 KB

ROADMAP.org

File metadata and controls

549 lines (474 loc) · 21.2 KB

GOAL

  • Efficient (approximate) model counting of nonlinear bitvector constraints

Plan

setup environment

convert bitvector constraints to SAT

evaluate tools

figure out how to convert BV constraints to BDDs

questions

RESOURCES

fix all-sat

implement all-sat with smt solvers

Tools

SAT/SMT

Boolector

  • Sang patched it to dump CNF formulas
  • API doesn’t provide high level logical operators (and/or between formulas)
    • blocking counter can be implement only with text interface

All-SAT (Orna’s tool)

  • Enumerates all solutions by preserving the DPLL tree between invocations of zChaff
  • Projection variables must be the last ones
  • To compile:
    • Add “include <cstring>” on batch_sat_solver.h
    • Add “-m32 -DNDEBUG” to the compiler flags on the makefile
    • this generates a 32-bit executable and disable assertions

check what’s the performance impact of specifying larger batches

Z3

  • Simple to implement a blocking counter
  • We use it to translate smt to cnf formulas

#(SAT/SMT)

Categories:

Exact

sharpSat
  • Well known #SAT solver
  • Source: https://sites.google.com/site/marcthurley/sharpsat (lots of papers)
  • Note: We will be using the augmented version with projection found at https://github.com/vladrich/sharpSAT. This version returns an upper bound of the number of models for a given projection. See DSharp-p (below) input format for more info on how to use the projection.
  • Results:
    • run1: root@5d3867d6581a:/tools/sharpSAT# time ./Release/sharpSAT ../PC1.smt2.cnf -*** Projection vars 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 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64

    Solving ../PC1.smt2.cnf variables (all/used/free): 342/342/0 clauses (all/long/binary/unit): 980/460/486/34

    Preprocessing ..Number of free variables among remembered: 0 DONE variables (all/used/free): 164/164/0 clauses (all/long/binary/unit): 478/186/292/0 Maximum cache size: 1594 MB

    FINAL COUNT AFTER PROJECTION: 100000

    variables (total / active / free) 164/164/0 clauses (removed) 980 (502) decisions 47 conflicts 0 conflict clauses (all/bin/unit) 0/0/0

    failed literals found by implicit BCP 0 implicit BCP miss rate 100% cache size 7MB cache (stores / hits) 48/58 cache miss rate 0% avg. variable count (stores / hits) 57.0208/25.3793

    100000

    time: 0.009336s

    real 0m0.015s user 0m0.012s sys 0m0.000s

    • run2:

    root@5d3867d6581a:/tools/sharpSAT# time ./Release/sharpSAT ../s-rsa-10.smt2.cnf -*** Projection vars 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 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 Solving ../s-rsa-10.smt2.cnf variables (all/used/free): 11804/11804/0 clauses (all/long/binary/unit): 57856/48713/9138/5

    Preprocessing ..Number of free variables among remembered: 0 DONE variables (all/used/free): 7725/7725/0 clauses (all/long/binary/unit): 35971/28357/7614/0 Maximum cache size: 1511 MB

    FINAL COUNT AFTER PROJECTION: 1696

    variables (total / active / free) 7725/7725/0 clauses (removed) 57856 (21883) decisions 1695 conflicts 0 conflict clauses (all/bin/unit) 3302/78/2

    failed literals found by implicit BCP 2143 implicit BCP miss rate 99.7683% cache size 54MB cache (stores / hits) 1696/0 cache miss rate 100% avg. variable count (stores / hits) 6472.45/0

    1696

    time: 19.2473s

    real 0m19.263s user 0m19.224s sys 0m0.040s

    • run3:

    root@5d3867d6581a:/tools/sharpSAT# time ./Release/sharpSAT ../s-rsa-13.smt2.cnf -*** Projection vars 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 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 Solving ../s-rsa-13.smt2.cnf variables (all/used/free): 15949/15949/0 clauses (all/long/binary/unit): 78143/65884/12252/7

    Preprocessing ..Number of free variables among remembered: 0 DONE variables (all/used/free): 11386/11386/0 clauses (all/long/binary/unit): 52909/41937/10972/0 Maximum cache size: 1155 MB

    FINAL COUNT AFTER PROJECTION: 1694

    variables (total / active / free) 11386/11386/0 clauses (removed) 78143 (25234) decisions 1693 conflicts 0 conflict clauses (all/bin/unit) 2915/86/0

    failed literals found by implicit BCP 2034 implicit BCP miss rate 99.7995% cache size 80MB cache (stores / hits) 1694/0 cache miss rate 100% avg. variable count (stores / hits) 9982.24/0

    1694

    time: 31.8438s

    real 0m31.863s user 0m31.800s sys 0m0.028s

    • run 4: mateus@antenora:~/workspace/sharpSAT$ ./sharpSAT ../bvcount/inputs/s-rsa-1.smt2.cnf

    Solving ../bvcount/inputs/s-rsa-1.smt2.cnf variables (all/used/free): 22531/22531/0 clauses (all/long/binary/unit): 54386/22421/31965/0 Preprocessing .. DONE variables (all/used/free): 18723/13795/4928 clauses (all/long/binary/unit): 42425/16245/26180/0 56 16 Maximum cache size: 1121 MB variables (total / active / free) 18723/13795/4928 clauses (removed) 54386 (11955) decisions 3465 conflicts 1748 conflict clauses (all/bin/unit) 13758/289/6 failed literals found by implicit BCP 8752 implicit BCP miss rate 99.5518% bytes cache size 42110088 bytes cache (overall) 63032172 bytes cache (infra / comps) 20234400/21875688 bytes pure comp data (curr) 21759272 bytes pure comp data (overall) 42575948 bytes cache with sysoverh (curr) 21988472 bytes cache with sysoverh (overall) 43012816 cache (stores / hits) 1819/0 cache miss rate 100% avg. variable count (stores / hits) 11839.2/0

    701307556295128209636714898138305940607056817271188923359087003155513381928582872889943608626334410206294055637466502208495374095228601660156838825824788563469514280757358037558997511232684421978334176559145825018081510446739265712972288627975858999234371610076224094374373608572493049785409796315090373010686268057631041427670713572760866079797590081413843630909971940792472068731664170470348968912497370987246341615963197538472863869186954458883336040793775409868694208850007359852700630835455065472053604717270611646256686452441801255199575666731229593746131141897926006387423807896289375036836766309624930056085848984206684652364937827279467440365694429183681411975523043124563439626347194748751536793152602894377995151380331257504502623143396866640088356971442883686243665377407318032570619293161540814740133428244471089134579711170986779324874560257884203679862315097369106253909490553898228417806381522330301203425598770973818391077462205385031515305612587290527580970248016182872260492235180761478931255100142143139014072660696935324405111673696630953700285044363602867268863277933447651853135993762413636802978668406201270144289323298895597723751982156289914462596738074121066596636500919534240503484621007492146213783125361337935559227592833362601777663437796387218593210290816618658750589303748706644829038362457740026505295247071970960467427650384139459086223002777100380494825466103580576115921225544536084842230147310538709594950842729834251228633235540420696569009940192444247179264

    time: 35.7415s

c2d
  • Converts CNF to d-DNNF(Deterministic, Decomposable Negation Normal Form), which allows counting in polynomial time. sharpSat’s webpage says that it is slower, but it may handle troublesome problems (for sharpSat) easily.
  • Source: New Advances in Compiling CNF to Decomposable Negation Normal Form
  • Skipping this one for DSharp
relsat
DSharp
  • Improves upon c2d by using fancy features from sharpSAT
  • Source: DSHARP: Fast d-DNNF Compilation with sharpSAT
  • Note: We will be using the version found at https://bitbucket.org/vladimirkl/dsharp because it supports projection.
  • Results
    • run1:

    Took a long time, forgot to call time…

Mathematica
  • See boolean.nb for experiments. In summary: Counting blows up quickly (OOM).

Probabilistic

  • (ε,δ). These counters were originally introduced by Karp and Luby to count the models of DNF formulas. They guarantee with a probability of at least 1 − δ that the result will be between 1 − ε and 1 + ε times the actual number of models. An instantiation of this class for CNF formulas is APPROX-MC.
  • lower/upper bounding counters. These counters drop the tolerance guarantee and compute an upper/lower bound for the number of models that is correct with a probability of at least 1 − δ (for a user-specified δ ). Examples are BPCOUNT, MINICOUNT, MBOUND and HYBRID-MBOUND.
  • guarantee-less counters. These counters provide no formal guarantees but can be very good in practice. Examples are APPROXCOUNT, SEARCHTREESAMPLER, SE and SAMPLESEARCH.
    • First approach, [Jerrum et al., 1986] (from “From Sampling to Model Counting”):

      Consider a Boolean formula F with M satisfying assignments. Assuming we could sample these satisfying assignments uniformly at random, we can measure the fraction of all models that have x1 set to True, M+, by taking the ratio of the number of assignments in the sample that have x1 set to True over the sample size. This fraction will converge with increasing sample size to the true fraction of models with x1 set positively, γ = M+/M. (For now, assume that γ > 0.) It follows immediately that M = (1/γ)M+. We will call 1/γ the “multiplier” (> 0). We have thus reduced the problem of counting the models of F to counting the models of a simpler formula, F+. We can recursively repeat the process, leading to a series of multipliers, until all variables are assigned or until we can count the number of models of the remaining formulas with an exact counter. For robustness, one usually sets selected variable to the truth value that occurs more often in the sample. This also avoids the problem of having γ = 0 and therefore an infinite multiplier. (Note that the more frequently occurring truth value gives a multiplier of at most 2.)

ApproxCount
ApproxMC
  • [X] installed
  • [X] working
  • Source: A Scalable Approximate Model Counter
  • Type: (ε,δ)
  • Code: http://www.cs.rice.edu/CS/Verification/Projects/ApproxMC/
  • Command: python ApproxMC.py -delta=0.14 -epsilon=0.5 ../s-rsa-10.smt2.cnf
  • Results:
    • run1: time python ApproxMC.py -delta=0.14 -epsilon=0.5 -logging=1 ../s-rsa-10.smt2.cnf

    {‘epsilon’: ‘0.5’, ‘inputFile’: ‘../s-rsa-10.smt2.cnf’, ‘logging’: ‘1’, ‘delta’: ‘0.14’} Count with tolerance: 0.5 and confidence: 0.86 is 1632

    real 5m21.995s user 5m17.832s sys 0m2.480s

ApproxMC-P
  • [X] installed
  • [X] working
  • Source: Sound Probabilistic #SAT with Projection
  • Type: (ε,δ)
  • Code: http://formal.iti.kit.edu/weigl/software/approxmc-py/
  • Command: ./approxmc-p.py -vvvv –sat-command ‘adapters/sharpCDCL.sh {maxcount} {file}’ $INPUT_FILE
  • Notes:
    • Compile cryptominisat4 with the flags: -DUSE_GAUSS=ON -DCMAKE_BUILD_TYPE=Release -DONLY_SIMPLE=OFF -DUSE_PTHREADS=ON
    • Email from Alexander (one of the authors)

    Hello Mateus,

    thank for your interrest into ApproxMC-py. I needed the following steps to reproduce a working ApproxMC-py instance:

    1. Ensure that scipy is installed – for me ‘sudo dnf python3-scipy’
    2. Ensure you have a bounded #SAT with projection installed, like

    clasp, sharpCDCL or an adapted version cryptominisat [1].

    1. Some adapters need xorblast [2], as a SAT-preprocessor for

    xor-clauses.

    1. Ensure, e.g. that xorblast.py and sharpCDCL executable, is on $PATH:

    export PATH=$PATH:/home/weigl/work/xorblast/ export PATH=$PATH:/home/weigl/work/sharpCDCL/build

    1. Run using approxmc-p.py (formely known as run.py):

    ~/w/approxmc-py % ./approxmc-p.py -vvvv –sat-command ‘adapters/sharpCDCL.sh {maxcount} {file}’ \ ~/work/qif-sat/case_study_crc/logs_2/1452259749/crc32_8_0x04C11DB7.pp.cnf

    I hope that works for you.

    best regards,

    Alexander

  • Results: defaults are ε=0.5,δ=0.14
    • run1:

    root@2e94282b6763:/tools/approxmc-py# time ./approxmc-p.py -vvvv –sat-command ‘adapters/cryptominisat4.sh {maxcount} {file}’ ../s-rsa-10.smt2.cnf Model-Count: 1600

    real 0m2.116s user 0m1.952s sys 0m0.300s

    • run2: root@2e94282b6763:/tools/approxmc-py# time ./approxmc-p.py -vvvv –sat-command ‘adapters/cryptominisat4.sh {maxcount} {file}’ ../s-rsa-10.smt2.cnf Model-Count: 1664

    real 0m2.201s user 0m2.060s sys 0m0.344s

    • run3:

    root@2e94282b6763:/tools/approxmc-py# time ./approxmc-p.py –sat-command ‘adapters/cryptominisat4.sh {maxcount} {file}’ ../s-rsa-10.smt2.cnf Model-Count: 1472

    real 0m2.092s user 0m1.960s sys 0m0.228s

    • run4:

    root@5d3867d6581a:/tools/approxmc-py# time ./approxmc-p.py –sat-command ‘adapters/cryptominisat4.sh {maxcount} {file}’ ../PC1.smt2.cnf Model-Count: 102400

    real 0m0.706s user 0m0.600s sys 0m0.316s

    • run5:

    root@5d3867d6581a:/tools/approxmc-py# time ./approxmc-p.py –sat-command ‘adapters/cryptominisat4.sh {maxcount} {file}’ ../s-rsa-13.smt2.cnf Model-Count: 1664

    real 0m3.017s user 0m2.760s sys 0m0.376s

    • run6:

    root@5d3867d6581a:/tools/approxmc-py# time ./approxmc-p.py –sat-command ‘adapters/cryptominisat4.sh {maxcount} {file}’ ../s-rsa-13.smt2.cnf Model-Count: 1856

    real 0m2.885s user 0m2.748s sys 0m0.284s

[1]: https://gitlab.com/QIF/cryptominisat4 [2]: https://gitlab.com/QIF/xorblast

smtapproxmc
  • [X]
  • Source: Approximate Probabilistic Inference via Word-Level Counting
  • Type: (ε,δ)
  • Code: https://bitbucket.org/kuldeepmeel/smtapproxmc
  • Results: ### Parsing the Output File ### The `<output_file>` generated by the script is a semicolon separated file with following values: <maximum_bitwidth>;<comma_separated_list_of_primes>;<median>;<time_in_seconds>;<# iterations_which_timedout>;<iteration_in_which_timedout>
    • run1:

    root@5d3867d6581a:/tools/smtapproxmc# python3 scripts/approxMC.py ../s-rsa-10.smt2 scripts/primes.txt 10 log out root@5d3867d6581a:/tools/smtapproxmc# cat out 32;3,;0.0;2.8200000000000003;0;Timedout in runs: set()

    • run2:

    root@5d3867d6581a:/tools/smtapproxmc# python3 scripts/approxMC.py ../s-rsa-10.smt2 scripts/primes.txt 100 log out root@5d3867d6581a:/tools/smtapproxmc# cat out 32;3,;0.0;20.41;0;Timedout in runs: set()

    • run3:

    root@5d3867d6581a:/tools/smtapproxmc# python3 scripts/approxMC.py ../PC1.smt2 scripts/primes.txt 100 log out root@5d3867d6581a:/tools/smtapproxmc# cat out 32;;111409.5;48.57;0;Timedout in runs: set()

    • run4:

    root@5d3867d6581a:/tools/smtapproxmc# python3 scripts/approxMC.py ../PC1.smt2 scripts/primes.txt 10 log out root@5d3867d6581a:/tools/smtapproxmc# cat out 32;;131074.0;3.93;0;Timedout in runs: set()root@5d3867d6581a:/tools/smtapproxmc#

    • run5:

    root@5d3867d6581a:/tools/smtapproxmc# python3 scripts/approxMC.py ../s-rsa-10.smt2 scripts/primes.txt 10 log out root@5d3867d6581a:/tools/smtapproxmc# cat out 32;3,;0.0;2.13;0;Timedout in runs: set()

    • run6:

    root@5d3867d6581a:/tools/smtapproxmc# python3 scripts/approxMC.py ../s-rsa-13.smt2 scripts/primes.txt 10 log out root@5d3867d6581a:/tools/smtapproxmc# cat out 32;;1963.5;12.11;0;Timedout in runs: set()

    • run7

    root@5d3867d6581a:/tools/smtapproxmc# python3 scripts/approxMC.py ../s-rsa-13.smt2 scripts/primes.txt 10 log out root@5d3867d6581a:/tools/smtapproxmc# cat out 32;257,;7.0;7.87;0;Timedout in runs: set()

    • run8

    root@5d3867d6581a:/tools/smtapproxmc# python3 scripts/approxMC.py ../s-rsa-13.smt2 scripts/primes.txt 50 log out root@5d3867d6581a:/tools/smtapproxmc# cat out 32;;1741.0;44.480000000000004;0;Timedout in runs: set()

SE
  • Source: Stochastic Enumeration Method for Counting NP-Hard Problems
  • Type: guarantee-less
  • Code: Couldn’t find.
SampleCount
BPCount/MiniCount
  • Source: Leveraging Belief Propagation, Backtrack Search, and Statistics for Model Counting
  • Type: Lower (bpcount), Upper (MiniCount)
  • Code: Not available
MBound
SampleSearch
  • [X]
  • Source: SampleSearch: Importance sampling in presence of determinism
  • Type: guarantee-less
  • Code: http://www.hlt.utdallas.edu/~vgogate/software.html
  • This one is strange: I can’t find a way to set a stop criteria - it just keeps going.
  • Results:
    • run 1

    root@5d3867d6581a:/tools# time ./satss s-rsa-10.smt2.cnf c Debugging is ON. DBL Min = 6.72421e-4932 Problem read Max cluster size =109 Estimate = 2.9828e+33 #sampled variables = 1730 out of 11804 Dom size i-bound = 12 Join graph done Nodes initialized Iteration 0 Done Iteration 1 Done Iteration 2 Done Iteration 3 Done Iteration 4 Done Iteration 5 Done Iteration 6 Done Iteration 7 Done Iteration 8 Done Iteration 9 Done buckets created DRC done ^C

    real 26m46.250s user 26m41.308s sys 0m1.460s

SearchTreeSampler

root@5d3867d6581a:/tools/STS# ./core/STS ../PC1.smt2.cnf -verb=0

WARNING: for repeatability, setting FPU to use double precision SATISFIABLE z <9.830400e+04, 9.830400e+04 > , time= 0.17, samp=1 z <9.895936e+04, 9.895936e+04 > , time= 0.28, samp=2 z <9.917781e+04, 9.917781e+04 > , time= 0.38, samp=3 z <9.895936e+04, 9.895936e+04 > , time= 0.48, samp=4 z <1.001390e+05, 1.001390e+05 > , time= 0.59, samp=5 z <9.983317e+04, 9.983317e+04 > , time= 0.69, samp=6 z <9.924023e+04, 9.924023e+04 > , time= 0.80, samp=7 z <9.945088e+04, 9.945088e+04 > , time= 0.90, samp=8 z <9.961472e+04, 9.961472e+04 > , time= 1.01, samp=9 z <9.922150e+04, 9.922150e+04 > , time= 1.11, samp=10 Different : 0 Chi-square : 0.000000 Estimated log-z: 11.505110 Estimated Z: 9.922150e+04

  • run2:

root@5d3867d6581a:/tools/STS# ./core/STS ../s-rsa-10.smt2.cnf -verb=0 WARNING: for repeatability, setting FPU to use double precision SATISFIABLE z <1.679360e+03, 1.679360e+03 > , time= 442.48, samp=1 ^Cz <1.658880e+03, 1.658880e+03 > , time= 562.13, samp=2 z <-nan, -nan > , time= 562.13, samp=3 z <-nan, -nan > , time= 562.13, samp=4 z <-nan, -nan > , time= 562.13, samp=5 z <-nan, -nan > , time= 562.14, samp=6 z <-nan, -nan > , time= 562.14, samp=7 z <-nan, -nan > , time= 562.14, samp=8 z <-nan, -nan > , time= 562.14, samp=9 z <-nan, -nan > , time= 562.14, samp=10 Different : 0 Chi-square : 0.000000 Estimated log-z: -nan Estimated Z: -nan

Snippets

count n vars cnf

tail -n +3 debug | tr ‘-’ ’ ’ | tr [:space:] ‘\n’ | sort -u | wc

Benchmarks

SATCOMP’16

  • Downloading…

ApproxMC

sharpSAT

ApproxMC-py

  • Can’t find the benchmarks anywhere.