We obtain the smallest unsatisfiable formulas in subclasses of $k$-CNF (exactly $k$ distinct literals per clause) with bounded variable or literal occurrences. Smaller unsatisfiable formulas of this type translate into stronger inapproximability results for MaxSAT in the considered formula class. Our results cover subclasses of 3-CNF and 4-CNF; in all subclasses of 3-CNF we considered we were able to determine the smallest size of an unsatisfiable formula; in the case of 4-CNF with at most 5 occurrences per variable we decreased the size of the smallest known unsatisfiable formula. Our methods combine theoretical arguments and symmetry-breaking exhaustive search based on SAT Modulo Symmetries (SMS), a recent framework for isomorph-free SAT-based graph generation. To this end, and as a standalone result of independent interest, we show how to encode formulas as graphs efficiently for SMS.

翻译：我们获得了在具有有限变量或文字出现次数的$k$-CNF（每个子句恰好包含$k$个不同文字）子类中的最小不可满足公式。这类更小的不可满足公式转化为所考虑公式类中MaxSAT更强的不可近似性结果。我们的结果涵盖了3-CNF和4-CNF的子类；在我们考虑的所有3-CNF子类中，我们都能确定不可满足公式的最小规模；在变量最多出现5次的4-CNF情况下，我们减小了已知最小不可满足公式的规模。我们的方法结合了理论论证和基于SAT模对称性（SMS）的对称破缺穷举搜索，SMS是最近提出的用于基于SAT的无同构图生成的框架。为此，并且作为一个具有独立意义的独立结果，我们展示了如何为SMS高效地将公式编码为图。