ABSTRACT. Over the last few years, our community has started a collective conversation on several topics related to our publication culture: our emphasis on conference publishing; our large number of specialty conferences; concerns that we have created a culture of hypercritical reviewing, which stifle rather than encourage innovative research; concerns that tenure and promotion practice encourage incremental short-term research; the tension between the ideal of open access and the reality of reader-pay publishing; and the role of social media in scholarly publishing. While computing research has been phenomenally successful, there is a feeling that our publication models are quite often obstacles. Yet, there is no agreement on whether our publication models need to be radically changed or fine tuned, and there is no agreement on how such change may occur. This panel is aimed at furthering the conversation on this topic, with the hope of moving us closer to an agreement.

ABSTRACT. In this paper we present new methods for deciding the satisfiability of formulas involving integer polynomial constraints. In previous work we proposed to solve SMT(NIA) problems by reducing them to SMT(LIA): non-linear monomials are linearized by abstracting them with fresh variables and by performing case splitting on integer variables with finite domain. When variables do not have finite domains, artificial ones can be introduced by imposing a lower and an upper bound, and made iteratively larger until a solution is found (or the procedure times out). For the approach to be practical, unsatisfiable cores are used to guide which domains have to be relaxed (i.e., enlarged) from one iteration to the following one. However, it is not clear then how large they have to be made, which is critical.

Here we propose to guide the domain relaxation step by analyzing minimal models produced by the SMT(LIA) solver. Namely, we consider two different cost functions: the number of violated artificial domain bounds, and the distance with respect to the artificial domains. We compare these approaches with other techniques on benchmarks coming from constraint-based program analysis and show the potential of the method. Finally, we describe how one of these minimal-model-guided techniques can be smoothly adapted to deal with the extension Max-SMT of SMT(NIA) and then applied to program termination proving.

ABSTRACT. Message Passing (MP) has been presented in a unified and consistent notational frame in \cite{gableske}. The paper explained the product-based MP framework (PMPF) and various MP heuristics (BP, SP, and several interpolations). The paper concluded, that an increased flexibility of MP heuristics (in the form of tuneable parameters) leads to a tuneable MP algorithm that can be helpful to solve a wide variety of different CNFs. Based on this work, the paper at hand makes three contributions. First, we extend the PMPF regarding flexibility based on theoretical insights from the Ising Model \cite{ising}. As an immediate result, this extended PMPF (ePMPF) provides new possibilities for parameter tuning. Second, the ePMPF will also allow us to uncover various theoretical connections between well-known variable and value ordering heuristics for SAT (Zero-first, One-first, occurrence-based heuristics). We show, that these heuristics can be understood as special cases of Message Passing. Third, we show that the ePMPF provides numerous possibilities to tightly integrate Message Passing with various aspects of the CDCL search paradigm.

ABSTRACT. In this paper we introduce two distributions for the Max-2-SAT problem similar to the uniform distributions of satisfiable CNFs and the planted distribution for the decision version of SAT. In both cases there is a parameter p, 0<= p<= 1/4d, where d is the clause-to-variable ratio (density) of the formula, such that formulas chosen according to both distributions are p-satisfiable, that is, at least (3/4d+p)n clauses can be satisfied. In the planted distribution this happens for a fixed assignment, while for the p-satisfiable distribution formulas are chosen uniformly from the set of all p-satisfiable formulas.

Following Coja-Oghlan, Krivelevich, and Vilenchik (2007) we establish a connection between the probabilities of events under the two distributions. Then we consider the case when p is sufficiently large, p=r\sqrt{d\log d} and r>3/2. We present an algorithm that in the case of the planted distribution for any e>0 with high probability finds an assignment satisfying at least (3/4d+p-e)n clauses. For the p-satisfiable distribution for every d there is e(d) (which is a polynomial in d of degree depending on r) such that the algorithm with high probability finds an assignment satisfying at least (3/4d+p-e(d))n clauses. It does not seem this algorithm can be converted into an expected polynomial time algorithm finding a p-satisfying assignment.

Also we use the connection between the planted and uniform p-satisfiable distributions to evaluate the number of clauses satisfiable in a random (not p-satisfiable) 2-CNF. We find the expectation of this number, but do not improve the existing concentration results.

ABSTRACT. We show that the propositional model counting problem #SAT for CNF- formulas with hypergraphs that allow a disjoint branches decomposition can be solved in polynomial time. We show that this class of hypergraphs is incomparable to hypergraphs of bounded incidence cliquewidth which were the biggest class of hypergraphs for which #SAT was known to be solvable in polynomial time so far. Furthermore, we present a polynomial time algorithm that computes a disjoint branches decomposition of a given hypergraph if it exists and rejects otherwise. Finally, we show that some slight extensions of the class of hypergraphs with disjoint branches decompositions lead to intractable #SAT, leaving open how to generalize the counting result of this paper.

ABSTRACT. The third round of the Kurt Gödel Research Prize Fellowships Program, under the title: Connecting Foundations and Technology, aims at supporting young scholars in early stages of their academic careers by offering highest fellowships in history of logic, kindly supported by the John Templeton Foundation. Young scholars being less or exactly 40 years old at the time of the commencement of the Vienna Summer of Logic (July 9, 2014) will be awarded one fellowship award in the amount of EUR 100,000, in each of the following categories:

• Logical Foundations of Mathematics,
• Logical Foundations of Computer Science, and
• Logical Foundations of Artificial Intelligence

The following three Boards of Jurors were in charge of choosing the winners:

• Logical Foundations of Mathematics: Jan Krajíček, Angus Macintyre, and Dana Scott (Chair).
• Logical Foundations of Computer Science: Franz Baader, Johann Makowsky, and Wolfgang Thomas (Chair).
• Logical Foundations of Artificial Intelligence: Luigia Carlucci Aiello, Georg Gottlob (Chair), and Bernhard Nebel.

http://fellowship.logic.at/

ABSTRACT. The aim of the FLoC Olympic Games is to start a tradition in the spirit of the ancient Olympic Games, a Panhellenic sport festival held every four years in the sanctuary of Olympia in Greece, this time in the scientific community of computational logic. Every four years, as part of the Federated Logic Conference, the Games will gather together all the challenging disciplines from a variety of computational logic in the form of the solver competitions.

At the Award Ceremonies, the competition organizers will have the opportunity to present their competitions to the public and give away special prizes, the prestigious Kurt Gödel medals, to their successful competitors. This reinforces the main goal of the FLoC Olympic Games, that is, to facilitate the visibility of the competitions associated with the conferences and workshops of the Federated Logic Conference during the Vienna Summer of Logic.

This award ceremony will host the

• 3rd Confluence Competition (CoCo 2014);
• Configurable SAT Solver Challenge (CSSC 2014);
• Ninth Max-SAT Evaluation (Max-SAT 2014);
• QBF Gallery 2014; and
• SAT Competition 2014 (SAT-COMP 2014).