Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency

DOI10.3233/FI-2011-428zbMath1242.68289arXiv1103.3693MaRDI QIDQ2895792

Oliver Kullmann

Publication date: 4 July 2012

Published in: Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1103.3693

zbMATH Keywords

satisfiability problemsatisfiabilitypolynomial timeconstraint satisfaction problemdeficiencysigned formulasautarkiesgeneralized clause-setslean clause-setsmatching autarkiesnon-Boolean variablesBoolean translationsdirect encodingdisjoint DNFgeneralised clause-setsHermitian defecthitting clause-setsirredundant clause-setsminimally unsatisfiable clause-sets. deficiencynested translation

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Applications of graph theory (05C90) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05)

Related Items (11)

Quantified maximum satisfiability ⋮ Counting minimal unsatisfiable subsets ⋮ Autarkies and Persistencies for QUBO ⋮ Computing Maximal Autarkies with Few and Simple Oracle Queries ⋮ Minimal sets on propositional formulae. Problems and reductions ⋮ On Davis-Putnam reductions for minimally unsatisfiable clause-sets ⋮ On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\) ⋮ Are hitting formulas hard for resolution? ⋮ Algorithms for computing minimal equivalent subformulas ⋮ On Variables with Few Occurrences in Conjunctive Normal Forms ⋮ Present and Future of Practical SAT Solving

Uses Software

• tawSolver

This page was built for publication: Constraint Satisfaction Problems in Clausal Form I: Autarkies and Deficiency