NDLI: Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints

Content Provider	Springer Nature Link
Author	Liffiton, Mark H. Sakallah, Karem A.
Copyright Year	2007
Abstract	Much research in the area of constraint processing has recently been focused on extracting small unsatisfiable “cores” from unsatisfiable constraint systems with the goal of finding minimal unsatisfiable subsets (MUSes). While most techniques have provided ways to find an approximation of an MUS (not necessarily minimal), we have developed a sound and complete algorithm for producing all MUSes of an unsatisfiable constraint system. In this paper, we describe a relationship between satisfiable and unsatisfiable subsets of constraints that we subsequently use as the foundation for MUS extraction algorithms, implemented for Boolean satisfiability constraints. The algorithms provide a framework with which many related subproblems can be solved, including relaxations of completeness to handle intractable instances, and we develop several variations of the basic algorithms to illustrate this. Experimental results demonstrate the performance of our algorithms, showing how the base algorithms run quickly on many instances, while the variations are valuable for producing results on instances whose complete results are intractably large. Furthermore, our algorithms are shown to perform better than the existing algorithms for solving either of the two distinct phases of our approach.
Starting Page	1
Ending Page	33
Page Count	33
File Format	PDF
ISSN	01687433
Journal	Journal of Automated Reasoning
Volume Number	40
Issue Number	1
e-ISSN	15730670
Language	English
Publisher	Springer Netherlands
Publisher Date	2007-09-13
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Constraint satisfaction Minimal unsatifiable subset CAMUS Symbolic and Algebraic Manipulation Mathematical Logic and Foundations Artificial Intelligence (incl. Robotics) Mathematical Logic and Formal Languages
Content Type	Text
Resource Type	Article
Subject	Artificial Intelligence Computational Theory and Mathematics Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Optimal Length Resolution Refutations of Difference Constraint Systems

Constraint Solving for Proof Planning

Clause Weighting Local Search for SAT

Satisfiability Checking in Łukasiewicz Logic as Finite Constraint Satisfaction

Java Bytecode Verification: Algorithms and Formalizations

IJCAR Preface

SAT Modulo Linear Arithmetic for Solving Polynomial Constraints

Theorem Proving Modulo

Java Bytecode Verification

Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints

Similar Documents

Optimal Length Resolution Refutations of Difference Constraint Systems

Constraint Solving for Proof Planning

Clause Weighting Local Search for SAT

Satisfiability Checking in Łukasiewicz Logic as Finite Constraint Satisfaction

Java Bytecode Verification: Algorithms and Formalizations

IJCAR Preface

SAT Modulo Linear Arithmetic for Solving Polynomial Constraints

Theorem Proving Modulo

Java Bytecode Verification

Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints