Realization of c-Inference as a SAT Problem
Semantically based on Spohn’s ranking functions, c-representations are special ranking models obtained by assigning individual integer impacts to the conditionals in a knowledge base R and by defining the rank of each possible world as the sum of the impacts of falsified conditionals. c-Inference is...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
LibraryPress@UF
2022-05-01
|
| Series: | Proceedings of the International Florida Artificial Intelligence Research Society Conference |
| Online Access: | https://journals.flvc.org/FLAIRS/article/view/130663 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850271018719903744 |
|---|---|
| author | Christoph Beierle Martin von Berg Arthur Sanin |
| author_facet | Christoph Beierle Martin von Berg Arthur Sanin |
| author_sort | Christoph Beierle |
| collection | DOAJ |
| description | Semantically based on Spohn’s ranking functions, c-representations are special ranking models obtained
by assigning individual integer impacts to the conditionals in a knowledge base R and by defining the rank of each
possible world as the sum of the impacts of falsified conditionals. c-Inference is the inference relation taking all
c-representations of a given knowledge base R into account. In this paper, we show that c-inference can be realized
as a boolean satisfiability problem (SAT), which in turn allows c-inference to be implemented by a SAT solver. We
provide a stepwise transformation of the characterization of c-inference as as constraint satisfaction problem (CSP),
into a solvable-equivalent SAT problem. We present a SAT-based implementation of c-inference using the SMT
solver Z3, demonstrating the feasibility of the approach. Up to now, there has been only one previous implementation
of c-inference; this previous implementation utilizes a Prolog-based CSP solver. First evaluation results demonstrate
that our SAT-based implementation outperforms the previous CSP-based implementation, providing a promising basis for
further developing this approach. |
| format | Article |
| id | doaj-art-22f1c66f661e4a0aaf37007a01a143df |
| institution | OA Journals |
| issn | 2334-0754 2334-0762 |
| language | English |
| publishDate | 2022-05-01 |
| publisher | LibraryPress@UF |
| record_format | Article |
| series | Proceedings of the International Florida Artificial Intelligence Research Society Conference |
| spelling | doaj-art-22f1c66f661e4a0aaf37007a01a143df2025-08-20T01:52:22ZengLibraryPress@UFProceedings of the International Florida Artificial Intelligence Research Society Conference2334-07542334-07622022-05-013510.32473/flairs.v35i.13066366862Realization of c-Inference as a SAT ProblemChristoph Beierle0Martin von Berg1Arthur Sanin2FernUniversität in HagenFernUniversität in HagenFernUniversität in HagenSemantically based on Spohn’s ranking functions, c-representations are special ranking models obtained by assigning individual integer impacts to the conditionals in a knowledge base R and by defining the rank of each possible world as the sum of the impacts of falsified conditionals. c-Inference is the inference relation taking all c-representations of a given knowledge base R into account. In this paper, we show that c-inference can be realized as a boolean satisfiability problem (SAT), which in turn allows c-inference to be implemented by a SAT solver. We provide a stepwise transformation of the characterization of c-inference as as constraint satisfaction problem (CSP), into a solvable-equivalent SAT problem. We present a SAT-based implementation of c-inference using the SMT solver Z3, demonstrating the feasibility of the approach. Up to now, there has been only one previous implementation of c-inference; this previous implementation utilizes a Prolog-based CSP solver. First evaluation results demonstrate that our SAT-based implementation outperforms the previous CSP-based implementation, providing a promising basis for further developing this approach.https://journals.flvc.org/FLAIRS/article/view/130663 |
| spellingShingle | Christoph Beierle Martin von Berg Arthur Sanin Realization of c-Inference as a SAT Problem Proceedings of the International Florida Artificial Intelligence Research Society Conference |
| title | Realization of c-Inference as a SAT Problem |
| title_full | Realization of c-Inference as a SAT Problem |
| title_fullStr | Realization of c-Inference as a SAT Problem |
| title_full_unstemmed | Realization of c-Inference as a SAT Problem |
| title_short | Realization of c-Inference as a SAT Problem |
| title_sort | realization of c inference as a sat problem |
| url | https://journals.flvc.org/FLAIRS/article/view/130663 |
| work_keys_str_mv | AT christophbeierle realizationofcinferenceasasatproblem AT martinvonberg realizationofcinferenceasasatproblem AT arthursanin realizationofcinferenceasasatproblem |