NDLI: On deciding subsumption problems

Content Provider	Springer Nature Link
Author	Egly, Uwe Pichler, Reinhard Woltran, Stefan
Copyright Year	2004
Abstract	Subsumption is an important redundancy elimination method in automated deduction. A clause D is subsumed by a set $$\mathcal{C}$$ of clauses if there is a clause C ∈ $$\mathcal{C}$$ and a substitution σ such that the literals of Cσ are included in D. In the field of automated model building, subsumption has been modified to an even stronger redundancy elimination method, namely the so-called clausal H-subsumption. Atomic H-subsumption emerges from clausal H-subsumption by restricting D to an atom and $$\mathcal{C}$$ to a set of atoms. Both clausal and atomic H-subsumption play an indispensable key role in automated model building. Moreover, problems equivalent to atomic H-subsumption have been studied with different terminologies in many areas of computer science. Both clausal and atomic H-subsumption are known to be intractable, i.e., Π p 2 -complete and NP-complete, respectively. In this paper, we present a new approach to deciding (clausal and atomic) H-subsumption that is based on a reduction to QSAT2 and SAT, respectively.
Starting Page	255
Ending Page	294
Page Count	40
File Format	PDF
ISSN	10122443
Journal	Annals of Mathematics and Artificial Intelligence
Volume Number	43
Issue Number	1-4
e-ISSN	15737470
Language	English
Publisher	Springer Netherlands
Publisher Date	2004-12-31
Publisher Place	Dordrecht
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	subsumption equational problems satisfiability QBFs Artificial Intelligence (incl. Robotics) Mathematics Computer Science Statistical Physics, Dynamical Systems and Complexity
Content Type	Text
Resource Type	Article
Subject	Applied Mathematics Artificial Intelligence

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

The SAT2002 competition

The complexity of Boolean constraint satisfaction local search problems

Toward leaner binary-clause reasoning in a satisfiability solver

On exact selection of minimally unsatisfiable subformulae

Dynamic symmetry-breaking for Boolean satisfiability

Special issue on multi-agent systems

Applicable algebra and artificial intelligence

Efficient data structures for backtrack search SAT solvers

Annals of Mathematics and Artificial Intelligence

On deciding subsumption problems

Similar Documents

The SAT2002 competition

The complexity of Boolean constraint satisfaction local search problems

Toward leaner binary-clause reasoning in a satisfiability solver

On exact selection of minimally unsatisfiable subformulae

Dynamic symmetry-breaking for Boolean satisfiability

Special issue on multi-agent systems

Applicable algebra and artificial intelligence

Efficient data structures for backtrack search SAT solvers

Annals of Mathematics and Artificial Intelligence

On deciding subsumption problems