Title: An Efficient Solver for Parametrized Difference Revision
Abstract: We present GenC, an efficient and highly-parallel belief revision solver for paramatrized difference operators. GenC uses an AllSAT solver to enumerate the possible models of a formula, and then determines the output of revision through a series of bit comparisons. The result is a system that can calculate the result of revision for formulas with 100 variables and millions of clauses in just seconds; the running times obtained by GenC far surpass existing solvers for belief revision. The system also has many features that are useful for practical problems: it supports both interactive and offline data entry, it allows multiple formats for entering formulas, and it provides output in human-readable format. Most importantly, GenC is able to model revision by any parametrized difference operator, which allows a wide range of practical problems to be easily captured.
Publication Year: 2019
Publication Date: 2019-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 7
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot