Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel

DOI10.1007/11814948_4MaRDI QIDQ5756578zbMATH OpenOpenAlexFDO

Authors Oliver Kullmann, Inês Lynce, Joao Marques-Silva

Publication date 4 September 2007

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://eprints.soton.ac.uk/262430/1/jpms-sat06b.pdf

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets
• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• On exact selection of minimally unsatisfiable subformulae
• scientific article; zbMATH DE number 2080329

Cited in

(15)

• Minimal sets on propositional formulae. Problems and reductions
• Semantic relevance
• Local-search extraction of mUSes
• Fast, flexible MUS enumeration
• Efficient reasoning for inconsistent Horn formulae
• Computing maximal autarkies with few and simple oracle queries
• Finding Guaranteed MUSes Fast
• Efficient combination of decision procedures for MUS computation
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• On semidefinite least squares and minimal unsatisfiability
• Does This Set of Clauses Overlap with at Least One MUS?
• 2006 Summer Meeting of the Association for Symbolic Logic: Logic Colloquium '06
• Present and Future of Practical SAT Solving
• An automata view to goal-directed methods
• Explanations of unsatisfiability beyond minimal subsets

This page was built for publication: Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5756578)