View: session overviewtalk overviewside by side with other conferences

09:00 | SPEAKER: Ralf Rothenberger ABSTRACT. We study non-uniform random k-SAT on n variables with an arbitrary probability distribution p on the variable occurrences. The number t = t(n) of randomly drawn clauses at which random formulas go from asymptotically almost surely (a.a.s.) satisfiable to a.a.s. unsatisfiable is called the satisfiability threshold. Such a threshold is called sharp if it approaches a step function as n increases. We show that a threshold t(n) for random k-SAT with an ensemble (p_n)_{n\in\N} of arbitrary probability distributions on the variable occurrences is sharp if ||p||_2 = O_n(t^(-2/k)) and ||p||_infinity = o_n(t^(-k/(2k-1)) * log^(-(k-1)/(2k-1))(t)). This result generalizes Friedgut’s sharpness result from uniform to non-uniform random k-SAT and implies sharpness for thresholds of a wide range of random k-SAT models with heterogeneous probability distributions, for example such models where the variable probabilities follow a power-law distribution. |

09:30 | SPEAKER: Stephan Gocht ABSTRACT. We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflict-driven pseudo-Boolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that so-called saturation is used instead of division. It is known that on CNF inputs cutting planes with cancelling addition and saturation is essentially just resolution. We show that even if general addition is allowed, this proof system is still polynomially simulated by resolution with respect to proof size as long as coefficients are polynomially bounded. As a further way of delineating the proof power of subsystems of CP, we propose to study a number of easy (but tricky) instances of problems in NP. Most of the formulas we consider have short and simple tree-like proofs in general CP, but the restricted subsystems seem to reveal a much more varied landscape. Although we are not able to formally establish separations between different subsystems of CP -which would require major technical breakthroughs in proof complexity- these formulas appear to be good candidates for obtaining such separations. We believe that a closer study of these benchmarks is a promising approach for shedding more light on the reasoning power of pseudo-Boolean solvers. |

10:00 | SPEAKER: Jacobo Toran ABSTRACT. We characterize several complexity measures for the resolution of Tseitin formulas in terms of a two person cop-robber game. Our game is a slight variation of the the one Seymour and Thomas used in order to characterize the tree-width parameter. For any undirected graph, by counting the number of cops needed in our game in order to catch a robber in it, we are able to exactly characterize the width, variable space and depth measures for the resolution of the Tseitin formula corresponding to that graph. We also give an exact game characterization of resolution variable space for any formula. We show that our game can be played in a monotonous way. This implies that the corresponding resolution measures on Tseitin formulas correspond to those under the restriction of regular resolution. Using our characterizations we improve the existing complexity bounds for Tseitin formulas showing that resolution width, depth and variable space coincide up to a logarithmic factor, and that variable space is bounded by the clause space times a logarithmic factor. |

16:00 | SPEAKER: Hoda Abbasizanjani ABSTRACT. Minimally Unsatisfiable clause-sets (MUs) are building blocks for understanding Minimally Unsatisfiable Sub-clause-sets (MUSs), and they are also interesting in their own right, as hardest unsatisfiable clause-sets. There are two important previously known but isolated characterisations for MUs, both with ingenious but complicated proofs: Characterising 2-CNF MUs, and characterising MUs with deficiency 2 (two more clauses than variables). Via a novel connection to Minimal Strong Digraphs (MSDs), we give short and intuitive new proofs of these characterisations, revealing an underlying common structure. We obtain unique isomorpism type descriptions of normal forms, for both cases. An MSD is a strongly connected digraph, where removing any arc destroys the strong connectedness. We introduce the new class DFM of special MUs, which are in close correspondence to MSDs. The known relation between 2-CNFs and digraphs is used, but in a simpler and more direct way. The non-binary clauses in DFMs can be ignored. For a binary clause (a or b) normally both arcs (-a -> b) and (-b -> a) need to be considered, but here we have a canonical choice of one of them. The definition of DFM is indeed very simple: an MU, where all clauses except of two are binary, while the two non-binary clauses are the two "full monotone clauses", the disjunction of all variables and the disjunction of all negated variables. We expect this basic class of MUs to be very useful in the future. Every variables occurs at least twice positively and twice negatively ("non-singularity"), and its isomorphism problem is GI-complete, while we have polytime decision, and likely we have good properties related to MUS-search. Via "saturations" and "marginalisations", adding resp. removing literal occurrences, as well as via "non-singular extensions", adding new variables, this class reaches out to apparently unrelated classes. |

16:30 | SPEAKER: Ryan Berryhill ABSTRACT. Computing minimal (or even just small) certificates is a central problem in automated reasoning and, in particular, in automated formal verification. For unsatisfiable formulas in CNF such certificates take the form of Minimal Unsatisfiable Subsets (MUSes) and have a wide range of applications. As a formula can have multiple MUSes and different MUSes provide different insights on unsatisfiability, commonly studied problems include computing a smallest MUS (SMUS) or computing all MUSes (AllMUS) of a given unsatisfiable formula. In this paper, we consider certificates to safety properties in the form of Minimal Safe Inductive Invariants (MSISes), and we develop algorithms for exploring such certificates by computing a smallest MSIS (SMSIS) or computing all MSISes (AllMSIS) of a given safe inductive invariant. More precisely, we show how two well-known algorithm CAMUS or MARCO for MUS enumeration can be adapted to MSIS enumeration as well. |

FLoC banquet at Examination Schools. Drinks and food available from 7pm (pre-booking via FLoC registration system required; guests welcome).