T-Wise Literal Subset Covering

[uulm-janbaudisch]

Adds the option to only fully cover a subset of variables or literals during t-wise sampling.

Usage

ddnnife -i ddnnf.nnf -o sample.txt t-wise -l 1,2,3,-4

Check Functionality

ddnnife -i ddnnf.nnf t-wise-check sample.txt -l 1,2,3,-4

---

Builds on #98

Closes #93

[github-actions]

Bencher Report

Branch	twise-variables
Testbed	aarch64-linux

Click to view all benchmark results

Benchmark	Latency	Benchmark Result microseconds (µs) (Result Δ%)	Upper Boundary microseconds (µs) (Limit %)
load auto1 (d4)	📈 view plot 🚷 view threshold	39,529.00 µs (+0.09%) Baseline: 39,491.67 µs	40,538.21 µs (97.51%)
load auto2 (c2d)	📈 view plot 🚷 view threshold	504,830.00 µs (-5.94%) Baseline: 536,705.00 µs	567,584.60 µs (88.94%)
load busybox (c2d)	📈 view plot 🚷 view threshold	1,429.70 µs (-0.50%) Baseline: 1,436.89 µs	1,460.56 µs (97.89%)
load small (c2d)	📈 view plot 🚷 view threshold	5.71 µs (-1.50%) Baseline: 5.80 µs	5.92 µs (96.40%)
t-wise busybox (c2d) t=2	📈 view plot 🚷 view threshold	850,600.00 µs (+0.13%) Baseline: 849,501.67 µs	1,030,002.75 µs (82.58%)
t-wise small (c2d) t=2	📈 view plot 🚷 view threshold	10.97 µs (-7.14%) Baseline: 11.81 µs	12.60 µs (87.04%)
t-wise small (c2d) t=3	📈 view plot 🚷 view threshold	12.31 µs (-5.32%) Baseline: 13.00 µs	13.70 µs (89.85%)

🐰 View full continuous benchmarking report in Bencher

[github-actions]

Bencher Report

Branch	twise-variables
Testbed	x86_64-linux

Click to view all benchmark results

Benchmark	Latency	Benchmark Result microseconds (µs) (Result Δ%)	Upper Boundary microseconds (µs) (Limit %)
load auto1 (d4)	📈 view plot 🚷 view threshold	43,185.00 µs (+2.58%) Baseline: 42,099.58 µs	44,189.78 µs (97.73%)
load auto2 (c2d)	📈 view plot 🚷 view threshold	579,510.00 µs (+2.89%) Baseline: 563,236.67 µs	596,508.88 µs (97.15%)
load busybox (c2d)	📈 view plot 🚷 view threshold	1,552.20 µs (-3.55%) Baseline: 1,609.38 µs	1,671.36 µs (92.87%)
load small (c2d)	📈 view plot 🚷 view threshold	6.01 µs (-31.25%) Baseline: 8.75 µs	10.53 µs (57.09%)
t-wise busybox (c2d) t=2	📈 view plot 🚷 view threshold	909,610.00 µs (+6.90%) Baseline: 850,881.67 µs	937,833.04 µs (96.99%)
t-wise small (c2d) t=2	📈 view plot 🚷 view threshold	12.21 µs (-10.54%) Baseline: 13.65 µs	15.18 µs (80.45%)
t-wise small (c2d) t=3	📈 view plot 🚷 view threshold	13.14 µs (-6.50%) Baseline: 14.05 µs	15.09 µs (87.09%)

🐰 View full continuous benchmarking report in Bencher

[github-actions]

Bencher Report

Branch	twise-variables
Testbed	x86_64-darwin

Click to view all benchmark results

Benchmark	Latency	Benchmark Result microseconds (µs) (Result Δ%)	Upper Boundary microseconds (µs) (Limit %)
load auto1 (d4)	📈 view plot 🚷 view threshold	59,102.00 µs (-0.39%) Baseline: 59,332.25 µs	77,796.27 µs (75.97%)
load auto2 (c2d)	📈 view plot 🚷 view threshold	812,780.00 µs (-6.92%) Baseline: 873,235.83 µs	1,074,879.97 µs (75.62%)
load busybox (c2d)	📈 view plot 🚷 view threshold	2,315.30 µs (-2.32%) Baseline: 2,370.22 µs	2,841.88 µs (81.47%)
load small (c2d)	📈 view plot 🚷 view threshold	23.55 µs (-2.23%) Baseline: 24.08 µs	30.13 µs (78.15%)
t-wise busybox (c2d) t=2	📈 view plot 🚷 view threshold	988,540.00 µs (-4.06%) Baseline: 1,030,350.00 µs	1,272,983.77 µs (77.66%)
t-wise small (c2d) t=2	📈 view plot 🚷 view threshold	24.95 µs (-6.55%) Baseline: 26.70 µs	31.28 µs (79.76%)
t-wise small (c2d) t=3	📈 view plot 🚷 view threshold	27.28 µs (-4.63%) Baseline: 28.60 µs	33.29 µs (81.93%)

🐰 View full continuous benchmarking report in Bencher