Restoring CSP Satisfiability with MaxSAT

• Autorzy: Lynce I. , Marques-Silva J.
• Języki publikacji: EN

Abstrakty

EN

The extraction of a Minimal Unsatisfiable Core (MUC) in a Constraint Satisfaction Problem (CSP) aims to identify a subset of constraints that make a CSP instance unsatisfiable. Recent work has addressed the identification of a Minimal Set of Unsatisfiable Tuples (MUST) in order to restore the CSP satisfiability with respect to that MUC. A two-step algorithm has been proposed: first, a MUC is identified, and second, a MUST in the MUC is identified. This paper proposes an integrated algorithm for restoring satisfiability in a CSP, making use of a MaxSAT solver. The proposed approach encodes the CSP instance as a partial MaxSAT instance, in such a way that solving the MaxSAT instance corresponds to identifying the smallest set of tuples to be removed from the CSP instance to restore satisfiability. Experimental results illustrate the feasibility of the approach.

Słowa kluczowe

EN

constraint satisfaction problems; minimal unsatisfiable cores; minimal set of unsatisfiable tuples; maximum satisfiability

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2011
• Tom: Vol. 107, nr 2/3
• Strony: 249--266
• Opis fizyczny: Bibliogr. 26 poz., tab., wykr.

Twórcy

autor

Lynce I.

autor

Marques-Silva J.

• INESC-ID/IST Technical University of Lisbon, Lisbon, Portugal,

Bibliografia

• [1] Ansótegui, C., Bonet, M. L., Levy, J.: Solving (Weighted) Partial MaxSAT through Satisfiability Testing, International Conference on Theory and Applications of Satisfiability Testing, 2009.
• [2] Argelich, J., Cabiscol, A., Lynce, I., Manyá, F.: Modelling Max-CSP as Partial Max-SAT, International Conference on Theory and Applications of Satisfiability Testing, 2008.
• [3] Argelich, J., Manyá, F.: Solving Over-Constrained Problems with SAT Technology, International Conference on Theory and Applications of Satisfiability Testing, 2005.
• [4] Argelich, J., Manyá, F.: Partial Max-SAT Solvers with Clause Learning, International Conference on Theory and Applications of Satisfiability Testing, 2007.
• [5] Bessière, C., Hebrard, E., Walsh, T.: Local Consistencies in SAT, International Conference on Theory and Applications of Satisfiability Testing, 2003.
• [6] Bruni, R.: On exact selection of minimally unsatisfiable subformulae, Annals of Mathematics and Artificial Intelligence, 43(1), 2005, 35-50.
• [7] Fu, Z., Malik, S.: On Solving the Partial MAX-SAT Problem, International Conference on Theory and Applications of Satisfiability Testing, 2006.
• [8] Goldberg, E. I., Novikov, Y.: Verification of Proofs of Unsatisfiability for CNF Formulas, Design, Automation and Test in Europe Conference, 2003.
• [9] González, S. M., Meseguer, P.: Boosting MUS Extraction, International Symposium on Abstraction, Reformulation, and Approximation, 2007.
• [10] Grégoire, ´ E., Mazure, B., Piette, C.: Extracting MUSes, European Conference on Artificial Intelligence, 2006.
• [11] Grégoire, ´ E., Mazure, B., Piette, C.: Local-search Extraction of MUSes, Constraints, 12(3), 2007, 325-344.
• [12] Grégoire, ´ E., Mazure, B., Piette, C.: MUST: Provide a Finer-Grained Explanation of Unsatisfiability, International Conference on Principles and Practice of Constraint Programming, 2007.
• [13] Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSat: A New Weighted Max-SAT Solver, International Conference on Theory and Applications of Satisfiability Testing, 2007.
• [14] Junker, U.: QUICKXPLAIN: Preferred Explanations and Relaxations for Over-Constrained Problems, AAAI National Conference on Artificial Intelligence, 2004.
• [15] Kullmann, O., Lynce, I., Marques-Silva, J.: Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel, International Conference on Theory and Applications of Satisfiability Testing, 2006.
• [16] Li, C. M., Manyá, F.: MaxSAT, Hard and Soft Constraints, in: SAT Handbook (A. Biere, M. Heule, H. van Maaren, T. Walsh, Eds.), IOS Press, 2009, 613-631.
• [17] Liffiton, M., Mneimneh, M., Lynce, I., Andraus, Z., Marques-Silva, J., Sakallah, K.: A Branch and Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Subformulas, Constraints, 14(4), 2009, 415-442.
• [18] Liffiton, M., Sakallah, K.: On Finding All Minimally Unsatisfiable Subformulas, International Conference on Theory and Applications of Satisfiability Testing, 2005.
• [19] Liffiton, M., Sakallah, K.: Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints, Journal of Automated Reasoning, 40(1), 2008, 1-33.
• [20] Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for Weighted Boolean Optimization, International Conference on Theory and Applications of Satisfiability Testing, 2009.
• [21] Marques-Silva, J., Lynce, I.: Towards Robust CNF Encodings of Cardinality Constraints, International Conference on Principles and Practice of Constraint Programming, 2007.
• [22] Marques-Silva, J., Manquinho, V.: Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms, International Conference on Theory and Applications of Satisfiability Testing, 2008.
• [23] Marques-Silva, J., Planes, J.: Algorithms for Maximum Satisfiability using Unsatisfiable Cores, Design, Automation and Test in Europe Conference, 2008.
• [24] Sinz, C.: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints, International Conference on Principles and Practice of Constraint Programming, 2005.
• [25] Walsh, T.: SAT v CSP, International Conference on Principles and Practice of Constraint Programming, 2000.
• [26] Zhang, L., Malik, S.: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications, Design, Automation and Test in Europe Conference, 2003.