2,706 research outputs found
A First Journey into the Complexity of Statistical Statements in Probabilistic Answer Set Programming
No full textProbabilistic Answer Set Programming is an efficient formalism to express uncertain information with an answer
set program (PASP). Recently, this formalism has been extended with statistical statements, i.e., statements that
can encode a certain property of the considered domain, within the PASTA framework. To perform inference,
these statements are converted into answer set rules and constraints with aggregates. The complexity of PASP
has been studied in depth, with results regarding both membership and completeness. However, a complexity
analysis of programs with statements is missing. In this paper, we close this gap by studying the complexity of
PASTA statements
Analyzed Benchmarks and Raw Data on Experiments for gpusat
No full text<p>For details see: </p>
<p>Johannes K. Fichte, Markus Hecher, Stefan Woltran, Markus Hecher: Weighted Model Counting on the GPU by Exploiting Small Treewidth, Proceedings of the 26th Annual European Symposium on Algorithms (ESA'2018).</p>
<p>For benchmarking we used a benchmark-tool. See https://github.com/daajoe/benchmark-tool for details.</p>
<p> </p>
Analyzed Benchmarks on Experiments for frasmt v2.0.0
No full textFor details see:
Johannes K. Fichte, Markus Hecher, Stefan Szeider: Breaking Symmetries with RootClique and LexTopSort, Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP'2020).
For frasmt we refer to https://github.com/daajoe/frasmt/releases/tag/v2.0.
Structure-Guided Automated Reasoning
No full textAlgorithmic meta-theorems state that problems definable in a fixed logic can be solved efficiently on structures with certain properties. An example is Courcelle’s Theorem, which states that all problems expressible in monadic second-order logic can be solved efficiently on structures of small treewidth. Such theorems are usually proven by algorithms for the model-checking problem of the logic, which is often complex and rarely leads to highly efficient solutions. Alternatively, we can solve the model-checking problem by grounding the given logic to propositional logic, for which dedicated solvers are available. Such encodings will, however, usually not preserve the input’s treewidth.
This paper investigates whether all problems definable in monadic second-order logic can efficiently be encoded into SAT such that the input’s treewidth bounds the treewidth of the resulting formula. We answer this in the affirmative and, hence, provide an alternative proof of Courcelle’s Theorem. Our technique can naturally be extended: There are treewidth-aware reductions from the optimization version of Courcelle’s Theorem to MAXSAT and from the counting version of the theorem to #SAT. By using encodings to SAT, we obtain, ignoring polynomial factors, the same running time for the model-checking problem as we would with dedicated algorithms. Another immediate consequence is a treewidth-preserving reduction from the model-checking problem of monadic second-order logic to integer linear programming (ILP). We complement our upper bounds with new lower bounds based on ETH; and we show that the block size of the input’s formula and the treewidth of the input’s structure are tightly linked.
Finally, we present various side results needed to prove the main theorems: A treewidth-preserving cardinality constraints, treewidth-preserving encodings from CNFs into DNFs, and a treewidth-aware quantifier elimination scheme for QBF implying a treewidth-preserving reduction from QSAT to SAT. We also present a reduction from projected model counting to #SAT that increases the treewidth by at most a factor of 2^{k+3.59}, yielding a algorithm for projected model counting that beats the currently best running time of 2^{2^{k+4}}⋅poly(|ψ|)
Analyzed Benchmarks on Experiments for gpusat2
No full text<p>For details see: </p>
<p>Johannes K. Fichte, Markus Hecher, Markus Hecher: An Improved GPU-based SAT Model Counter, Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming (CP'2019).</p>
<p>For benchmarking we used a benchmark-tool. See https://github.com/daajoe/benchmark-tool for details.</p>
<p>See also: <a href="https://github.com/daajoe/GPUSAT">https://github.com/daajoe/GPUSAT</a> and <a href="https://github.com/daajoe/gpusat_experiments">https://github.com/daajoe/gpusat_experiments</a></p>
Analyzed Benchmarks and Raw Data on Experiments for FraSMT
No full textFor details see:
Johannes K. Fichte, Markus Hecher, Neha Lodha, Stefan Szeider: An SMT Approach to Fractional Hypertree Width, Proceedings of the 24th International Conference on Principles and Practice of Constraint Programming (CP'2018)
Analyzed Benchmarks on Experiments for a SAT Time Leap Challenge
No full textFor details see:
Johannes K. Fichte, Markus Hecher, Stefan Szeider: A Time Leap Challenge for SAT-Solving, Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP'2020).
We include the sources from various authors.
zchaff is available at: https://www.princeton.edu/~chaff/ zchaff.html
For the benchmark set, we refer to https://www.cs.uni-potsdam.de/wv/projects/sets/set-industrial-09-12.tar.xz or https://www.cs.uni-potsdam.de/wv/projects/sets. The instances are also available on Zenodo at: https://doi.org/10.5281/zenodo.398907
A Benchmark Collection of #SAT Instances and Tree Decompositions
No full text<p>Benchmarks used for the paper</p>
<p>Johannes K. Fichte, Markus Hecher, Stefan Woltran, Markus Hecher: Weighted Model Counting on the GPU by Exploiting Small Treewidth, Proceedings of the 26th Annual European Symposium on Algorithms (ESA'2018).</p>
<p>For details we refer to the original sources of the benchmarks (https://tinyurl.com/countingbenchmarks), which contains benchmarks from the following sources:</p>
<ul>
<li><strong>ApproxMC</strong>(165 Instances): <a href="https://www.cs.rice.edu/CS/Verification/Projects/ApproxMC/">https://www.cs.rice.edu/CS/Verification/Projects/ApproxMC/</a></li>
<li><strong>C2D</strong>(14 Instances): <a href="http://reasoning.cs.ucla.edu/c2d/results.html">http://reasoning.cs.ucla.edu/c2d/results.html</a></li>
<li><strong>Cachet</strong>(1090 Instances): <a href="https://www.cs.rochester.edu/u/kautz/Cachet/Model_Counting_Benchmarks/index.html">https://www.cs.rochester.edu/u/kautz/Cachet/Model<em>Counting</em>Benchmarks/index.html</a></li>
<li><strong>counting-benchmarks</strong>(1451 Instances): <a href="https://github.com/dfremont/counting-benchmarks">https://github.com/dfremont/counting-benchmarks</a></li>
</ul>
Proofs for Propositional Model Counting
No full textAlthough propositional model counting (#SAT) was long considered too hard to be practical, today’s highly efficient solvers facilitate applications in probabilistic reasoning, reliability estimation, quantitative design space exploration, and more. The current trend of solvers growing more capable every year is likely to continue as a diverse range of algorithms are explored in the field. However, to establish model counters as reliable tools like SAT-solvers, correctness is as critical as speed.
As in the nature of complex systems, bugs emerge as soon as the tools are widely used. To identify and avoid bugs, explain decisions, and provide trustworthy results, we need verifiable results. We propose a novel system for certifying model counts. We show how proof traces can be generated for exact model counters based on dynamic programming, counting CDCL with component caching, and knowledge compilation to Decision-DNNF, which are the predominant techniques in today’s exact implementations. We provide proof-of-concepts for emitting proofs and a parallel trace checker. Based on this, we show the feasibility of using certified model counting in an empirical experiment
A Benchmark Collection of Hypergraphs
No full text<p>This benchmark currently contains 2191 hypergraph instances that originate from CQs and CSPs instances from various sources. All hypergraphs have been generated and published by W. Fischl, G. Gottlob, D. M. Longo, and R. Pichler (2017) at <a href="http://hyperbench.dbai.tuwien.ac.at">http://hyperbench.dbai.tuwien.ac.at</a> together with different hypergraph properties including various notions of width.</p>
<p>See Johannes K. Fichte, Markus Hecher, Neha Lodha, and Stefan Szeider: An SMT Approach to Fractional Hypertree Width, Proceedings of the 24th International Conference on Principles and Practice of Constraint Programming (CP2018) for details on the original sources of the benchmarks.</p>
- …
