Account
Edit tools
Internal
SucheSearch
Deutsch

Knowledge Representation and Reasoning Seminar

From International Center for Computational Logic

Knowledge Representation and Reasoning Seminar

Course with SWS 0/2/0 (lecture/exercise/practical) in SS 2018

Lecturer

SWS

  • 0/2/0

Modules

Examination method

  • Oral exam
  • Seminar presentation



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 Monday, 6.DS (16:40 - 18:10, starting 16.4.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].

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
    • Depth-first Branch and Bound exploiting a tree decomposition (GivrySchiexVerfaillie06a)
    • Counting solutions in satisfaction (FavierGivryJegou09a)
    • Hybrid best-first search exploiting a tree decomposition (AlloucheGivryKatsirelos15a)




Retrieved from "https://iccl.inf.tu-dresden.de/w/index.php?title=Knowledge_Representation_and_Reasoning_Seminar_(SS2018)/en&oldid=25347"