[cs-talks] (UPDATED) Upcoming Seminars: iBench (Thurs)
cs at bu.edu
Fri Mar 27 15:57:55 EDT 2015
An Overview of Knowledge Compilation for Solving #SAT and Its Application to Cybersecurity
Richard W. Skowrya, MIT Lincoln Library
Thursday, April 2, 2015 at 12:30pm in MCS B21
Abstract: Boolean model counting, referred to as #SAT, is the problem of determining for a given formula the number of satisfying truth assignments to its variables. Many real-world problem domains are inherently beyond the ability of modern SAT solvers despite being semantically amenable to modeling as a Boolean formula, as the quality of a solution may depend not only on satisfying the formula but also on the total number of satisfying solutions that exist under some constraint. In this talk I will provide a motivating example from the cybersecurity domain and discuss a knowledge compilation approach to solving #SAT developed by Adnan Darwiche. His Decomposable Deterministic Negation Normal Form (D-DNNF) encodes a Boolean formula in a directed graph which admits polynomial time model counting and output-linear time model enumeration. I will conclude with some lessons learned while implementing a tool for translating a domain-specific modelling and query language to and from D-DNNF.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the cs-talks