SAT-Based Horn Least Upper Bounds

DOI10.1007/978-3-319-24318-4_30MaRDI QIDQ3453244zbMATH OpenOpenAlexFDO

Authors Carlos Mencía, Alessandro Previti, Joao 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

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

Recommendations

• Satisfiability of mixed Horn formulas
• On the complexity of the maximum satisfiability problem for Horn formulas
• Upper bounds on the satisfiability threshold
• An improved upper bound for SAT
• Theory and Applications of Satisfiability Testing
• New worst-case upper bounds for SAT
• New worst-case upper bounds for SAT
• Satisfiability algorithms and lower bounds for Boolean formulas over finite bases
• Bounded queries to SAT and the Boolean hierarchy
• Theory and Applications of Satisfiability Testing

Cites work

• scientific article; zbMATH DE number 1946853 (Why is no real title available?)
• scientific article; zbMATH DE number 1509480 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• A theory of diagnosis from first principles
• Algorithms for computing backbones of propositional formulae
• Algorithms for computing minimal equivalent subformulas
• Algorithms for selective enumeration of prime implicants
• An SE-tree-based prime implicant generation algorithm
• Factoring Out Assumptions to Speed Up MUS Extraction
• First order LUB approximations: characterization and algorithms
• Horn Upper Bounds and Renaming
• Horn upper bounds and renaming
• Improving Glucose for incremental SAT solving with assumptions: application to MUS extraction
• Information loss in knowledge compilation: a comparison of Boolean envelopes
• Knowledge compilation and theory approximation
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• MUS Extraction Using Clausal Proofs
• On computing minimal models
• Open-WBO: a modular MaxSAT solver
• Progression in maximum satisfiability
• Semantical and computational aspects of Horn approximations
• Solving satisfiability problems with preferences
• Towards efficient MUS extraction
• Unification as a complexity measure for logic programming

Cited in

(3)

• Satisfiability of mixed Horn formulas
• Horn upper bounds and renaming
• First order LUB approximations: characterization and algorithms

Describes a project that uses

Uses Software

• QUICKXPLAIN
• Ltur
• Open-WBO
• Glucose

This page was built for publication: SAT-Based Horn Least Upper Bounds

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