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

DOI10.1007/11814948_4zbMath1187.68552OpenAlexW2095623224MaRDI QIDQ5756578

Inês Lynce, Oliver Kullmann, João P. 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)

Related Items (14)

Fast, flexible MUS enumeration ⋮ Computing Maximal Autarkies with Few and Simple Oracle Queries ⋮ Local-search extraction of mUSes ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ Finding Guaranteed MUSes Fast ⋮ Enhancing unsatisfiable cores for LTL with information on temporal relevance ⋮ On semidefinite least squares and minimal unsatisfiability ⋮ 2006 Summer Meeting of the Association for Symbolic Logic: Logic Colloquium '06 ⋮ An Automata View to Goal-Directed Methods ⋮ Does This Set of Clauses Overlap with at Least One MUS? ⋮ Efficient Reasoning for Inconsistent Horn Formulae ⋮ Efficient Combination of Decision Procedures for MUS Computation ⋮ Present and Future of Practical SAT Solving ⋮ Semantic relevance

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