Improving Model Counting by Leveraging Definability
Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence. Pages 751-756.
Abstract
We present a new preprocessing technique for propositional model counting. This technique leverages definability, i.e., the ability to determine that some gates are implied by the input formula Σ. Such gates can be exploited to simplify Σ without modifying its number of models. Unlike previous techniques based on gate detection and replacement, gates do not need to be made explicit in our approach. Our preprocessing technique thus consists of two phases: computing a bipartition I, O of the variables of Σ where the variables from O are defined in Σ in terms of I, then eliminating some variables of O in Σ. Our experiments show the computational benefits which can be achieved by taking advantage of our preprocessing technique for model counting.
@inproceedings{ijcai2016p112,
title = {Improving Model Counting by Leveraging Definability},
author = {Lagniez, Jean-Marie and Lonca, Emmanuel and Marquis, Pierre},
booktitle = {Proceedings of the Twenty-Fifth International Joint Conference on
Artificial Intelligence, {IJCAI-16}},
publisher = {AAAI Press / International Joint Conferences on Artificial Intelligence},
editor = {Subbarao Kambhampati},
pages = {751--756},
year = {2016},
month = {7},
url = {https://ijcai.org/proceedings/2016/112},
}
TY - CPAPER TI - Improving Model Counting by Leveraging Definability AU - Lagniez, Jean-Marie AU - Lonca, Emmanuel AU - Marquis, Pierre T2 - Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI-16 PB - AAAI Press / International Joint Conferences on Artificial Intelligence PY - 2016 SP - 751 EP - 756 UR - https://ijcai.org/proceedings/2016/112 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
