A General Nogood-Learning Framework for Pseudo-Boolean Multi-Valued SAT
Abstract
We formulate a general framework for pseudo-Boolean multi-valued nogood-learning, generalizing conflict analysis performed by modern SAT solvers and its recent extension for disjunctions of multi-valued variables. This framework can handle more general constraints as well as different domain representations, such as interval domains which are commonly used for bounds consistency in constraint programming (CP), and even set variables. Our empirical evaluation shows that our solver, built upon this framework, works robustly across a number of challenging domains.
Cite
Text
Jain et al. "A General Nogood-Learning Framework for Pseudo-Boolean Multi-Valued SAT." AAAI Conference on Artificial Intelligence, 2011. doi:10.1609/AAAI.V25I1.7824Markdown
[Jain et al. "A General Nogood-Learning Framework for Pseudo-Boolean Multi-Valued SAT." AAAI Conference on Artificial Intelligence, 2011.](https://mlanthology.org/aaai/2011/jain2011aaai-general/) doi:10.1609/AAAI.V25I1.7824BibTeX
@inproceedings{jain2011aaai-general,
title = {{A General Nogood-Learning Framework for Pseudo-Boolean Multi-Valued SAT}},
author = {Jain, Siddhartha and Sabharwal, Ashish and Sellmann, Meinolf},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2011},
pages = {48-53},
doi = {10.1609/AAAI.V25I1.7824},
url = {https://mlanthology.org/aaai/2011/jain2011aaai-general/}
}