SAT-Based Horn Least Upper Bounds
DOI10.1007/978-3-319-24318-4_30zbMATH Open1471.68256OpenAlexW2294892320MaRDI QIDQ3453244FDOQ3453244
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
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
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)
Cites Work
- LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
- Algorithms for computing backbones of propositional formulae
- Title not available (Why is that?)
- Solving satisfiability problems with preferences
- A theory of diagnosis from first principles
- Towards efficient MUS extraction
- Knowledge compilation and theory approximation
- Algorithms for computing minimal equivalent subformulas
- Progression in maximum satisfiability
- Title not available (Why is that?)
- On computing minimal models
- Open-WBO: a modular MaxSAT solver
- Improving Glucose for incremental SAT solving with assumptions: application to MUS extraction
- Semantical and computational aspects of Horn approximations
- First order LUB approximations: characterization and algorithms
- Horn upper bounds and renaming
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Unification as a complexity measure for logic programming
- Title not available (Why is that?)
- Algorithms for selective enumeration of prime implicants
- MUS Extraction Using Clausal Proofs
- Factoring Out Assumptions to Speed Up MUS Extraction
- An SE-tree-based prime implicant generation algorithm
- Information loss in knowledge compilation: a comparison of Boolean envelopes
- Horn Upper Bounds and Renaming
Cited In (3)
Uses Software
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)
