Algorithms for computing minimal equivalent subformulas

DOI10.1016/J.ARTINT.2014.07.011zbMATH Open1405.68340OpenAlexW2091072454MaRDI QIDQ460638FDOQ460638

Authors Anton Belov, Mikoláš Janota, Inês Lynce, Joao Marques-Silva

Publication date 13 October 2014

Published in Artificial Intelligence (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.artint.2014.07.011

zbMATH Keywords

redundancyBoolean satisfiabilityminimal unsatisfiabilityirredundant subformula

Mathematics Subject Classification ID

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

Recommendations

• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
• Computing minimally unsatisfiable subformulas: state of the art and future directions
• Minimally unsatisfiable Boolean circuits
• scientific article; zbMATH DE number 2080337
• Algorithms for computing backbones of propositional formulae

Cites work

• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 1946853 (Why is no real title available?)
• scientific article; zbMATH DE number 5032602 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• A Way to Simplify Truth Functions
• A structure-preserving clause form translation
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Blocked clause elimination for QBF
• Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
• Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
• Determining computational complexity from characteristic ``phase transitions
• Efficient combination of decision procedures for MUS computation
• Eliminating Redundant Clauses in SAT Instances
• Failed literal detection for QBF
• Finding Guaranteed MUSes Fast
• Inprocessing rules
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• Logical and algorithmic properties of stable conditional independence
• MUST: Provide a Finer-Grained Explanation of Unsatisfiability
• Minimal Representation of Directed Hypergraphs
• On improving MUS extraction algorithms
• On the power of clause-learning SAT solvers as resolution engines
• Optimal compression of propositional Horn knowledge bases: Complexity and approximation
• Principles and practice of constraint programming. 18th international conference, CP 2012, Québec City, QC, Canada, October 8--12, 2012. Proceedings
• Redundancy in logic. I: CNF propositional formulae
• Redundancy in logic. II: 2CNF and Horn propositional formulae
• Redundancy in logic. III: Non-monotonic reasoning
• Removing propagation redundant constraints in redundant modeling
• Temporal induction by incremental SAT solving
• The Problem of Simplifying Truth Functions
• The complexity of Boolean formula minimization
• The scaling window of the 2-SAT transition
• Theory and Applications of Satisfiability Testing
• Towards efficient MUS extraction
• Two-level logic minimization: an overview
• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems

Cited in

(4)

• Quantified maximum satisfiability
• SAT-Based Horn Least Upper Bounds
• Minimal sets on propositional formulae. Problems and reductions
• On redundant topological constraints

Describes a project that uses

Uses Software

• MiniSat
• PicoSAT
• Bloqqer
• QUICKXPLAIN

This page was built for publication: Algorithms for computing minimal equivalent subformulas

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