Computing minimally unsatisfiable subformulas: state of the art and future directions

MaRDI QIDQ4583686zbMATH OpenFDO

Authors Joao Marques-Silva

Publication date 3 September 2018

Full work available at URL http://www.oldcitypublishing.com/journals/mvlsc-home/mvlsc-issue-contents/mvlsc-volume-19-number-1-3-2012/mvlsc-19-1-3-p-163-183/

zbMATH Keywords

Boolean satisfiabilityminimally unsatisfiable subformulasextensions of Boolean satisfiabilityunsatisfiability proofs

Mathematics Subject Classification ID

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

Recommendations

• Minimally unsatisfiable Boolean circuits
• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
• On computing the union of MUSes
• FMUS2: An Efficient Algorithm to Compute Minimal Unsatisfiable Subsets
• Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making

Cited in

(9)

• On computing minimal independent support and its applications to sampling and counting
• Extracting unsatisfiable cores for LTL via temporal resolution
• Enhancing unsatisfiable cores for LTL with information on temporal relevance
• Algorithms for computing minimal equivalent subformulas
• Minimal sets on propositional formulae. Problems and reductions
• Minimally unsatisfiable Boolean circuits
• On the complexity of inconsistency measurement
• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
• Approximating minimal unsatisfiable subformulae by means of adaptive core search

This page was built for publication: Computing minimally unsatisfiable subformulas: state of the art and future directions

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