SAT encodings for distance-based belief merging operators

1Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

Abstract

We present SAT encoding schemes for distance-based belief merging operators relying on the (possibly weighted) drastic distance or the Hamming distance between interpretations, and using sum, GMax (leximax) or GMin (leximin) as aggregation function. In order to evaluate these encoding schemes, we generated benchmarks of a time-tabling problem and translated them into belief merging instances. Then, taking advantage of these schemes, we compiled the merged bases of the resulting instances into query-equivalent CNF formulae. Experiments have shown the benefits which can be gained by considering the SAT encoding schemes we pointed out. Especially, thanks to them, we succeeded in computing query-equivalent formulae for merging instances based on hundreds of variables, which are out of reach of previous implementations.

Cite

CITATION STYLE

APA

Konieczny, S., Lagniez, J. M., & Marquis, P. (2017). SAT encodings for distance-based belief merging operators. In 31st AAAI Conference on Artificial Intelligence, AAAI 2017 (pp. 1163–1169). AAAI press. https://doi.org/10.1609/aaai.v31i1.10681

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free