scientific article; zbMATH DE number 1470716
algorithmscomplexity analysiscomputation problemscutting plane algorithmsdata structuresessentially quantified Boolean termsextension of propositional logicFrege systemsHorn logiclength of resolution proofslinear inequation systemnormal formsNP-completenesspropositional logicresolution calculussatisfiability checking algorithmssatisfiability problem for clausessequent systemstableauxtransformation algorithms
Introductory exposition (textbooks, tutorial papers, etc.) pertaining to mathematical logic and foundations (03-01) Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Software, source code, etc. for problems pertaining to mathematical logic and foundations (03-04) Classical propositional logic (03B05) Mechanization of proofs and logical operations (03B35) Logic in computer science (03B70) Complexity of proofs (03F20) Analysis of algorithms and problem complexity (68Q25) Analysis of algorithms (68W40)
- scientific article; zbMATH DE number 702472
- scientific article; zbMATH DE number 4008367
- The propositional logic induced by means of basic algebras
- scientific article; zbMATH DE number 4039849
- scientific article; zbMATH DE number 4031629
- scientific article; zbMATH DE number 3259885
- scientific article; zbMATH DE number 6001202
- scientific article; zbMATH DE number 4079387
- Backdoor sets of quantified Boolean formulas
- Optimizing propositional calculus formulas with regard to questions of deducibility
- Homomorphisms of conjunctive normal forms.
- Minimal sets on propositional formulae. Problems and reductions
- On exact selection of minimally unsatisfiable subformulae
- Generalizations of matched CNF formulas
- Extension and equivalence problems for clause minimal formulae
- Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic
- The complexity of problems for quantified constraints
- The treewidth of proofs
- Using decomposition-parameters for QBF: mind the prefix!
- On conversions from CNF to ANF
- Directed hypergraphs and Horn minimization
- Boolean functions with long prime implicants
- On the computational consequences of independence in propositional logic
- On the query complexity of selecting minimal sets for monotone predicates
- Boolean functions as models for quantified Boolean formulas
- Treewidth-aware reductions of normal \textsc{ASP} to \textsc{SAT} - is normal \textsc{ASP} Harder than \textsc{SAT} after all?
- Solving projected model counting by utilizing treewidth and its limits
- scientific article; zbMATH DE number 1705165 (Why is no real title available?)
- Total space in resolution
- Quantifier reordering for QBF
- Failed literal detection for QBF
- Generalized conflict-clause strengthening for satisfiability solvers
- Propositional SAT solving
- Small resolution proofs for QBF using dependency treewidth
- Introduction to Mathematics of Satisfiability
- A CNF Class Generalizing Exact Linear Formulas
- Combinatorial Problems for Horn Clauses
- A decomposition method for CNF minimality proofs
- Boolean functions with a simple certificate for CNF complexity
- Construction and learnability of canonical Horn formulas
- Reasoning about visibility
- scientific article; zbMATH DE number 702472 (Why is no real title available?)
- scientific article; zbMATH DE number 1380573 (Why is no real title available?)
- scientific article; zbMATH DE number 782033 (Why is no real title available?)
- Backdoors into two occurrences
- Learning definite Horn formulas from closure queries
- Constraint acquisition
- Ground Interpolation for Combined Theories
- Boolean Constraint Satisfaction Problems: When Does Post’s Lattice Help?
- Exploiting Database Management Systems and Treewidth for Counting
- Inductive definitions in logic versus programs of real-time cellular automata
- Subsumption-linear Q-resolution for QBF theorem proving
- Logic-based ontology comparison and module extraction, with an application to DL-Lite
- A logic-based approach to polymer sequence analysis
- Reasoning with propositional logic: from SAT solvers to knowledge compilation
- On the benefits of knowledge compilation for feature-model analyses
- Tight double exponential lower bounds
- IASCAR: incremental answer set counting by anytime refinement
- Small unsatisfiable k-CNFs with bounded literal occurrence
- The relative strength of \#SAT proof systems
- Refinement-based enumeration of QBF solutions
- Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
- Producing and verifying extremely large propositional refutations
- Counting QBF solutions at level two
- The complexity of variable minimal formulas
- Inferring RPO symbol orderings
- The relative strength of \#SAT proof systems
- Body-decoupled grounding via reduction: a novel approach on the \textsc{Asp} bottleneck
- Theory revision with queries: Horn, read-once, and parity formulas
- Solving peptide sequencing as satisfiability
- Models and quantifier elimination for quantified Horn formulas
- Exclusive and essential sets of implicates of Boolean functions
- A new 3-CNF transformation by parallel-serial graphs
- Satisfiability of mixed Horn formulas
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4488342)
