SAT-Based Horn Least Upper Bounds

DOI10.1007/978-3-319-24318-4_30zbMath1471.68256OpenAlexW2294892320MaRDI QIDQ3453244

Carlos Mencía, Alessandro Previti, João P. Marques-Silva

Publication date: 20 November 2015

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24318-4_30

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Uses Software

• Glucose
• Open-WBO
• Ltur
• QUICKXPLAIN

Cites Work

• Algorithms for computing minimal equivalent subformulas
• Solving satisfiability problems with preferences
• Information loss in knowledge compilation: a comparison of Boolean envelopes
• A theory of diagnosis from first principles
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• On computing minimal models
• Semantical and computational aspects of Horn approximations
• Algorithms for selective enumeration of prime implicants
• An SE-tree-based prime implicant generation algorithm
• First order LUB approximations: characterization and algorithms
• Towards efficient MUS extraction
• MUS Extraction Using Clausal Proofs
• Open-WBO: A Modular MaxSAT Solver,
• Horn Upper Bounds and Renaming
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Unification as a complexity measure for logic programming
• Knowledge compilation and theory approximation
• Algorithms for computing backbones of propositional formulae
• Factoring Out Assumptions to Speed Up MUS Extraction
• Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item