Knowledge Representation and Reasoning Seminar

Lehrveranstaltung mit SWS 0/2/0 (Vorlesung/Übung/Praktikum) in WS 2018

Dozent

Steffen Hölldobler
Johannes Fichte

Umfang (SWS)

0/2/0

Module

Leistungskontrolle

Mündliche Prüfung
Referat

Information

Topic: Solving #SAT and Weighted Model Counting

In this seminar, we want to compile together introductory talks that deal with propositional model counting (#SAT) and weighted model counting and its solving. See Seminar-literature.bib for the full citations referred in the text.

The problem #SAT asks to compute the number of solutions of a propositional formula, which is theoretically of high worst case complexity (#P-hard). If in addition each literal in the formula has an associated weight and we are interested in the sum of weights of all solutions, where the weight of a truth assignment is the product of the weights of its literals, we call the problem weighted model counting (WMC).

These problems have various applications to computational problems in modern society. Examples of such problems are identifying the reliability of energy infrastructure or learning preference distributions.

Main parts/topics:

1) Applications

Bayesian Inference

2) Techniques

Brute-Force
Branch-and-Bound (and compilations)
Sampling

Distributed Solving

A webpage that provides a good overview on solvers is [1].

Schedule

the seminar will take place on Wednesday, 15:30 (starting on 17.10.2018)
location: 2008

Format of the Seminar

Reading and Presenting (including software presentation)

Instructions/Goal

You will pick a topic - generally FIFO (first come first served), but some topics might be split into two as well. Topics are not ordered by hardness, but for some topics it might be nice to hear one talk before another. So we should slightly coordinate presentation dates.

One week before the talk, you will have to hand in a short report of about 5 to 10 pages about the topic. The talk itself should be about 30 minutes.

For most topics there is usually also a solver available, we expect that you try out the solver, present its techniques (as described) and give a brief overview on its usage during your talk. If you compare them, even better; but that's not required.

For presentations we highly encourage you to make things more visual, provide examples on the whiteboard etc. see [2] [3] for good examples.

For each topic we provide 2-3 references on reading material and a reference on an available solver. Since we are lazy and want you to work on the topic instead of googling around, we provide you with a bibtex file that contains all necessary references and a folder that contains all papers. Together with the topic we provide in brackets the bibtex cite key. PDFs are named analogously. We do not expect you to read all suggested papers in detail, you might have to be selective.

Comment: Topics marked with :f: would also be a starter for a future long term

assignment or thesis project with our group.

Pointers

For solvers try not to use a VM to setup your solvers. This usually makes things much easier (even though it makes not much sense for benchmarking). To setup an environment you need a hypervisor such as virtual box [4] a tool that takes care of the deployment [5], and prepared machines [6].

References

Introduction to #SAT and WMC
- Handbook of Satisfiability: Model Counting (GomesKautzSabharwalSelman08a)
- On the Hardness of Approximate Reasoning (Roth96a)
- Algorithms and Complexity Results for SAT and Bayesian Inference (BacchusDalmaoPitassi03)
- [optional] Solution Enumeration for Projected Boolean Search Problems (GebserKaufmannSchaub09a)
- [optional] Projected Model Counting (AzizChuMuise15a)
Applications of Model Counting and Weighted Model Counting
- solvers:
  - No solver given
  - If you are able to write a compiler that compiles UAI instances into WMC this is a plus. http://www.hlt.utdallas.edu/~vgogate/uai16-evaluation/uaiformat.html
- Performing Bayesian Inference by Weighted Model Counting (SangBeameKautz05a)
- Counting-Based Reliability Estimation for Power-Transmission Grids (MeelEtAl17a)
Classical DPLL/CDCL-based solving using Component Caching
- solvers:
  - cachet: https://www.cs.rochester.edu/u/kautz/Cachet/index.htm
  - sharpSAT: https://sites.google.com/site/marcthurley/sharpsat
  - sharpCDCL: http://tools.computational-logic.org/content/sharpCDCL.php
- Combining Component Caching and Clause Learning for Effective Model Counting (SangEtAl04)
- Counting Models with Advanced Component Caching and Implicit BCP (Thurley06)
Knowledge Compilation
- solvers:
  - http://www.cril.univ-artois.fr/KC/index.html
  - c2d: http://reasoning.cs.ucla.edu/c2d/
  - d4: http://www.cril.univ-artois.fr/KC/d4.html
  - bdd_minisat_all: http://www.sd.is.uec.ac.jp/toda/code/cnf2obdd.html
  - reasoner for WMC: http://www.cril.univ-artois.fr/KC/d-DNNF-reasoner.html
- An improved decision-DNNF compiler (LagniezMarquis17a)
- New Advances in Compiling CNF to Decomposable Negation Normal Form (Darwiche04a)
- Implementing Efficient All Solutions SAT Solvers (TodaSoh15a)
- Knowledge Compilation for Model Counting: Affine Decision Trees (KoricheLagniezMarquisThomas13a)
Parameterized Algorithms: Solving #SAT/WMC by Dynamic Programming :f:
- solvers
  - qpusat: https://github.com/Budddy/GPUSAT
  - dynQBF: https://github.com/gcharwat/dynqbf/tree/counting
  - dynASP: https://github.com/daajoe/dynasp
- Algorithms for propositional model counting (SamerSzeider10b)
- Answer Set Solving with Bounded Treewidth Revisited (FichteEtAl17a)
- SolvingSAT and MAXSAT by dynamic programming (SaetherTelleVatshelle15a)
- Weighted Model Counting on the GPU by Exploiting Small Treewidth (FichteEtAl18a)
Preprocessing Techniques :f:
- preprocessors
  - pmc: http://www.cril.univ-artois.fr/KC/pmc.html
  - B+E: http://www.cril.univ-artois.fr/KC/bpe2.html
- Preprocessing for Propositional Model Counting (LagniezMarquis14a)
- Improving Model Counting by Leveraging Definability (LagniezLoncaMarquis16a)
Approximate Model Counting
- solvers
  - ApproxMC: https://www.cs.rice.edu/CS/Verification/Projects/ApproxMC/
  - ApproxMC2: https://bitbucket.org/kuldeepmeel/approxmc
  - sts: http://cs.stanford.edu/~ermon/code/STS.zip
- Distribution-Aware Sampling and Weighted Model Counting for SAT. (ChakrabortyEtAl4a)
- From Weighted to Unweighted Model Counting (ChakrabortyEtAl15a)
- Uniform Solution Sampling Using a Constraint Solver As an Oracle (ErmonGomesSelman12a)
Distributed Solving :f:
- solvers
  - CountAntom (https://projects.informatik.uni-freiburg.de/projects/countantom)
  - dCountAntom (consult google or contact the authors)
- Distributed Parallel #SAT Solving (BurchardSchubertBecker16a)
- Laissez-Faire Caching for Parallel #SAT Solving (BurchardSchubertBecker15a)
Verification of SAT Refutations (only SAT) :f:
- tool
  - https://www.cs.utexas.edu/~marijn/drat-trim/
  - DRAT-trim: https://github.com/marijnheule/drat-trim
- Mechanical Verification of SAT Refutations with Extended Resolution (WetzlerHeuleHunt13a)
- The DRAT format and DRAT-trim checker (Heule16a)
Portfolio Solving/Algorithm Configuration :f:
- tools
  - SMAC3: https://github.com/automl/SMAC3
  - PyImp: https://github.com/automl/ParameterImportance
  - AutoFolio: https://github.com/mlindauer/AutoFolio
  - FlexFolio: http://www.ml4aad.org/algorithm-selection/flexfolio/
- SMAC: Sequential Model-based Algorithm Configuration (HutterRamage15b)
- claspfolio 2: Advances in Algorithm Selection for Answer Set Programming (HoosLindauerSchaub14a)
- AutoFolio: An automatically configured Algorithm Selector (LindauerHoosHutter15a)
Tensor Flow (Special Task) :f:
- tools
  - https://www.tensorflow.org/
- TensorFlow Tutorial: https://www.tensorflow.org/tutorials/
- Special Task

Give an overview on TensorFlow and present ideas on how one could use it to solve #SAT using dynamic programming. We expect detailed ideas on cases that occur during dynamic programming.

Extensions: Weigthed Partial Max-SAT
- solver
  - toulbar2: http://www7.inra.fr/mia/T/toulbar2/documentation.html
- Depth-first Branch and Bound exploiting a tree decomposition (GivrySchiexVerfaillie06a)
- Counting solutions in satisfaction (FavierGivryJegou09a)
- Hybrid best-first search exploiting a tree decomposition (AlloucheGivryKatsirelos15a)