| |
|
Description: |
Consider some complicated manufacturing process (producing for example a car, or a software component within a generative library), where not all orders can be fulfilled, but where the order has to be checked for inconsistency. In case the order is inconsistent (can not be fulfilled) we want to get a reasonable error message.
We study the problem of locating the error in the context of using a "SAT solver" for the consistency check, motivated by the decent efficiency often gained in this way. In order to apply the "SAT solver", the original query has to be shredded into tiny pieces (that is, into "clauses"). Now how to obtain the "cause" of the failure out of the collection of these tiny pieces?
I want to present a general approach towards this problem, based on logical and combinatorial properties of "clause-sets". All necessary background regarding "SAT" etc. will be explained.
Area(s): Logic and Computation
|
|
Date: |
|
| Start Time: |
16:30 |
|
Speaker: |
Oliver Kullmann (Swansea)
|
|
Place: |
2.5
|
| Research Groups: |
-Algebra, Logic and Topology
|
|
See more:
|
<Main>
|
|
