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

zbMATH Open1394.68359MaRDI QIDQ4583686FDOQ4583686

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/

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

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)

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)