An Approximate Skolem Function Counter
summary
An algorithm produces a PAC guaranteed multiplicative approximation to the log number of Skolem functions, using two exact #SAT calls and a linear number of sampling/counting oracle calls (with Dagum-style adaptive sampling and state‑of‑the‑art counters). Implementation scales to formulas with thousands of variables and solves 379 of 608 QBF-derived benchmarks versus 8 for an exact-enumeration baseline; on 158 small instances with epsilon=0.8 the mean relative error is ~0.2 and the worst error is under 0.5.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 2:39Skolem functions and problem
- 5:20Skolem function counting applications
- 9:02Problem complexity
- 11:59Algorithm overview
- 13:53Algorithm and implementation
- 16:36Experimental results
- 20:11Benchmark accuracy
- 22:22Summary and open questions
- 23:48Open problems
- 26:33Q&A
related talks
13mProgram Analysis via Efficient Symbolic Abstraction
17mSatisfiability Algorithms Based on Concentrated Shrinkage
18mScalable Floating-Point Satisfiability via Staged Optimization
35mA Peek Inside SAT Solvers
55mLower Bounds Against PC With Extension Variables
18mFast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect...
17mAlgebro-geometric Algorithms for Template-Based Synthesis of Polynomial Program...
18mEquivalence and Similarity Refutation for Probabilistic Programs