ABSTRACT. Multi-agents games are extensively used for modelling settings in which different entities share resources. For example, the setting in which entities need to route messages in a network is modelled by network-formation games: the network is modelled by a graph, and each agent has to select a path satisfying his reachability objective. In practice, the objectives of the entities are often more involved than reachability. The need to specify and reason about rich specifications has been extensively studied in the context of verification and synthesis of reactive systems. The talk describes a lifting of ideas from formal methods to multi-agent games. For example, in network-formation games with regular objectives, the edges of the graph are labeled by alphabet letters and the objective of each player is a regular language over the alphabet of labels. Thus, beyond reachability, a player may restrict attention to paths that satisfy certain properties, referring, for example, to the providers of the traversed edges, the actions associated with them, their quality of service, security, etc.

The talk assumes no previous knowledge in game theory. We will introduce the basic concepts and problems, describe how their extension to games with more expressive specification of objectives poses new challenges, and study the resulting games.

Joint work with Guy Avni and Tami Tamir.

ABSTRACT. In 2010, Spence and Van Gelder presented a family of CNF formulas based on combinatorial block designs. They showed empirically that this construction yielded small instances that were orders of magnitude harder for state-of-the-art SAT solvers than other benchmarks of comparable size, but left open the problem of proving theoretical lower bounds. We establish that these formulas are exponentially hard for resolution and even for polynomial calculus, which extends resolution with algebraic reasoning. We also present updated experimental data showing that these formulas are indeed still hard for current CDCL solvers, provided that these solvers do not also reason in terms of cardinality constraints (in which case the formulas can become very easy). Somewhat intriguingly, however, the very hardest instances in practice seem to arise from so-called fixed bandwidth matrices, which are provably easy for resolution and are also simple in practice if the solver is given a hint about the right branching order to use. This would seem to suggest that CDCL with current heuristics does not always search efficiently for short resolution proofs, despite the theoretical results of [Pipatsrisawat and Darwiche 2011] and [Atserias, Fichte, and Thurley2011].

ABSTRACT. We investigate the proof complexity of a class of propositional formulas expressing a combinatorial principle known as the Kneser-Lovasz Theorem. This is a family of propositional tautologies, indexed by an nonnegative integer parameter k that generalizes the Pigeonhole Principle (PHP, obtained for k=1).

We show for all fixed $k$ $2^{\Omega(n)}$ lower bounds on resolution complexity and exponential lower bounds for bounded depth Frege proofs. These results hold even for the more restricted class of formulas encoding Schrijver's strengthening of the Kneser-Lovasz Theorem. On the other hand for the cases $k=2,3$ (for which combinatorial proofs of the Kneser-Lovasz Theorem are known) we give polynomial size Frege (k=2), respectively extended Frege (k=3) proofs. The paper concludes with a brief discussion of the results (that will be presented in a subsequent paper) on the complexity of the general case of the Kneser-Lovasz theorem.

ABSTRACT. Incremental SAT solving under assumptions, introduced in Minisat, is in wide use. However, Minisat's algorithm for incremental SAT solving under assumptions has two main drawbacks which hinder performance considerably. First, it is not compliant with the highly effective and commonly used preprocessor SatELite. Second, all the assumptions are left in the formula, rather than being represented as unit clauses, propagated, and eliminated. Two previous attempts to overcome these problems solve either the first or the second of them, but not both. This paper remedies this situation by proposing a comprehensive solution for incremental SAT solving under assumptions, where SatELite is applied and all the assumptions are propagated. Our algorithm outperforms existing approaches over publicly available instances generated by a prominent industrial application in hardware validation.

ABSTRACT. Portfolio approach for parallel SAT solvers is known as the standard parallelization technique. In portfolio, diversification is one of the important factors in order to enable workers (solvers) to conduct a vast search. The diversification is implemented by setting different parameters for each worker in the state-of-the-art parallel portfolio SAT solvers. However, existing diversification can be insufficient because the combination of the parameters is limited, in which two or more workers can search same spaces. For this issue, we propose a novel diversification technique, called community branching. In this method, we assign a different set (or sets) of variables (called a community) to each worker and force them to select these variables as decision variables in early decision levels. In this manner, we can avoid overlaps of search spaces between the workers more intentionally than the existing method. We create a graph, where a vertex is corresponds to a variable and an edge stands for relations in a same clause, and we apply a modularity-based community detection algorithm to it. The variables in a community have strong relationships, and a distributed search for different communities can benefit the whole search. Experimental results shot that we could speedup the existing parallel SAT solvers with our proposal.

ABSTRACT. (Tentative) In this paper, we present a simple parallel version of Glucose that uses a lazy policy to exchange clauses between cores. By working on the clause exchange policy, we ensure that in the context of many cores, the large number of incoming clauses will not degrade each core performances.

ABSTRACT. Various "hardness" measures have been studied for resolution, providing theoretical insight into the proof complexity of resolution and its fragments, as well as explanation for the hardness of instances in SAT solving. In this paper we aim at a unified view of a number of hardness measures, including different measures of width, space and size.

As our main contribution we obtain combinatorial characterisations of these hardness measures. Our characterisations are both in terms of Prover-Delayer games and of sets of partial assignments with some consistency strength. These unified characterisations allow elegant proofs of relations between the different hardness measures. In particular, we obtain a generalised version of Atserias and Dalmau's result on the relation between resolution width and space from (J. Comput. Syst. Sci. 2008). Our results do not only hold for unsatisfiable instances, but also transfer to the satisfiable case, for which little is known regarding hardness measures.

ABSTRACT. Quantified Boolean formula (QBF) evaluation has a broad range of applications in computer science and is gaining increasing attention. Recent progress has shown that for a certain family of formulas Q-resolution, which forms the foundation of learning in modern search-based QBF solvers, is exponentially inferior in proof length to its extended variants: long-distance Q-resolution (LQ-resolution) and Q-resolution with resolution over universal literals (QU-resolution). The relative proof power between LQ-resolution and QU-resolution, however, remains unknown. In this paper, we show their incomparability by exponential separations on two families of QBFs, and further proposes a combination of the two resolution methods to achieve an even more powerful proof system. These results may shed light on solver development with enhanced learning mechanisms. In addition, we show how QBF Skolem/Herbrand certificate extraction can benefit from polynomial LQ-resolution proofs in contrast to their exponential Q-resolution counterparts.