A General Nogood-Learning Framework for Pseudo-Boolean Multi-Valued SAT (Extended Abstract ? )
Siddhartha Jain, Ashish Sabharwal, Meinolf Sellmann · 2011
Jain et al. [4] recently introduced a new no-good learning approach for multivalued satisfaction (MV-SAT) problems. This approach was shown to infer significantly stronger no-goods than those inferred by a mechanism that is based on a Boolean representation of a multi-valued problem as a SAT instance. Like earlier methods, the learning approach is based on an implication graph where nodes represent domain events and edges are implications drawn by the clauses in the given problem. One of the novelties of Jain et al. was the sole focus on variable inequations to infer the minimal reasons for a failure. In this work, we investigate why the particular use of inequations results in stronger no-goods and we formulate a general framework for multi-valued nogood-learning that can handle more general constraints, and also different domain representations, such as interval domains, which are commonly used for bounds consistency in constraint programming (CP). This is an essential step towards an integration of pseudo-Boolean and multi-valued SAT. State-of-the-art SAT and CP methods differ significantly in style and philosophy,