Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae

MaRDI QIDQ2741521zbMATH OpenFDO

Authors Renato Bruni, Antonio Sassano

Publication date 24 September 2001

zbMATH Keywords

heuristic

Mathematics Subject Classification ID

Combinatorial optimization (90C27) Approximation methods and heuristics in mathematical programming (90C59)

Recommendations

• scientific article; zbMATH DE number 2080329
• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• On exact selection of minimally unsatisfiable subformulae
• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
• Theory and Applications of Satisfiability Testing

Cites work

• A machine program for theorem-proving
• Branching rules for satisfiability
• scientific article; zbMATH DE number 6118223 (Why is no real title available?)
• scientific article; zbMATH DE number 3568056 (Why is no real title available?)
• scientific article; zbMATH DE number 1302170 (Why is no real title available?)
• scientific article; zbMATH DE number 1324220 (Why is no real title available?)
• scientific article; zbMATH DE number 1342119 (Why is no real title available?)
• scientific article; zbMATH DE number 2033323 (Why is no real title available?)
• scientific article; zbMATH DE number 2080329 (Why is no real title available?)
• scientific article; zbMATH DE number 1380573 (Why is no real title available?)
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• Solving satisfiability in less than \(2^ n\) steps

Cited in

(7)

• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Extracting unsatisfiable cores for LTL via temporal resolution
• Restoring CSP satisfiability with MaxSAT
• Towards a notion of unsatisfiable and unrealizable cores for LTL
• scientific article; zbMATH DE number 2080329 (Why is no real title available?)
• New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability

Describes a project that uses

Uses Software

• Leibniz

This page was built for publication: Restoring satisfiability or maintaining unsatisfiability by finding small unsatisfiable subformulae

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