2014/08/04 by Oliver Kullmann, Kullmann, Oliver, Xishun Zhao +1 · 3 citations
Computer Science · Mathematics · #05D99 (Secondary) #68R99 (Primary) 03B05 #Combinatorics (math.CO) #Constraint Satisfaction and Optimization #Discrete Mathematics (cs.DM) #F.2.2 #FOS: Computer and information sciences #FOS: Mathematics #G.2.2 #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #acm:03B05 #acm:05D99 #acm:68R99 #cs.DM #cs.LO #math.CO #msc:03B05 #msc:05D99 #msc:68R99 #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1408.0629
103 pages; second version has changed style, various small errors and typos corrected, and improved presentation of results, third version with editorial improvements, fourth version with editorial corrections and improvements/updates, fifth version with complete literature update and improved proofs and presentation; continues arXiv:1010.5756
openalex publication_date 2014/08/04 · arxiv created 2017/01/20 · arxiv updated 2017/01/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We investigate connections between SAT (the propositional satisfiability problem) and combinatorics, around the minimum degree (number of occurrences) of variables in various forms of redundancy-free boolean conjunctive normal forms (clause-sets). Lean clause-sets do not have non-trivial autarkies, that is, it is not possible to satisfy some clauses and leave the other clauses untouched. The deficiency of a clause-set is the difference of the number of clauses and the number of variables. We prove a precise upper bound on the minimum variable degree of lean clause-sets in dependency on the deficiency. If a clause-set does not fulfil this upper bound, then it must have a non-trivial autarky; we show that the autarky-reduction (elimination of affected clauses) can be done in polynomial time, while it is open to find the autarky itself in polynomial time. Then we investigate this upper bound for the special case of minimally unsatisfiable clause-sets. We show that the bound can be improved here, introducing a general method to improve the underlying recurrence. We consider precise relations, and thus the investigations have a number-theoretical flavour. We try to build a bridge from logic to combinatorics (especially to hypergraph colouring), and we discuss thoroughly the background and open problems, and provide many examples and explanations.