Unit propagation (UP) based method are widely used in Branch and Bound (BnB) Max-SAT solvers for detecting disjoint inconsistent subsets (IS) during the lower bound (LB) estimation. UP consists in assigning to true (propagating) all the literals which appear in unit clauses. The existing implementations of UP only consider the first unit clause causing the assignment of each variable, thus the propagations must be done and undone chronologically to ensure that all the unit clauses are properly exploited. Max-SAT BnB solvers transforms the formulas to ensure IS disjointness. These transformations remove clauses from the formula thus propagations are frequently undone. Since the propagations are undone in chronological order, many useless unassignments and reassignments are performed. We propose in this paper a new unit propagation scheme which considers all the unit clauses causing the assignment of the variables by UP. This new scheme allows to undo propagations in a non-chronological way and thus it reduces the number of redundant propagation steps made by BnB solvers. We also show how the information available with this new scheme can be used to influence the characteristics of the IS built by BnB solvers. We propose a heuristic which aims at reducing their size, and thus improving the quality of the LB estimation. We have implemented the new propagation scheme as well as the IS building heuristic in our solver MSsolver. We present and discuss the results of the experimental study we have performed.

A number of problems involve managing a set of optional clauses. For example, the soft clauses in a MAXSAT formula are optional—they can be falsified for a cost. Similarly, when computing a Minimum Correction Set for an unsatisfiable formula, all clauses are optional—some can be falsified in order to satisfy the remaining. In both of these cases the task is to find a subset of the optional clauses that achieves some criteria, and whose removal leaves a satisfiable formula. Relaxation search is a simple method of using a standard SAT solver to solve this task. Relaxation search is easy to implement, sometimes requiring only a simple modification of the variable selection heuristic in the SAT solver; it offers considerable flexibility and control over the order in which subsets of optional clauses are examined; and it automatically exploits clause learning to exchange information between the two phases of finding a suitable subset of optional clauses and checking if their removal yields satisfiability. We demonstrate how relaxation search can be used to solve MAXSAT and to compute Minimum Correction Sets. In both cases relaxation search is able to achieve state-of-the-art performance and solve some instances other solvers are not able to solve.

Propositional satisfiability (SAT) solvers based on conflict directed clause learning (CDCL) implicitly produce resolution refutations of unsatisfiable formulas. The precise class of formulas for which they can produce polynomial size refutations has been the subject of several studies, with special focus on the clause learning aspect of these solvers. The results, however, assume the use of non-standard and non-asserting learning schemes, or rely on polynomially many restarts for simulating individual steps of a resolution refutation, or work with a theoretical model that significantly deviates from certain key aspects of all modern CDCL solvers such as learning only one asserting clause from each conflict and other techniques such as conflict guided backjumping and phase saving. We study non-restarting CDCL solvers that learn only one asserting clause per conflict and show that, with simple preprocessing that depends only on the number of variables of the input formula, such solvers can polynomially simulate resolution. We show, moreover, that this preprocessing allows one to convert any CDCL solver to one that is non-restarting.

We compare the sample complexity of private learning [Kasiviswanathan et al. 2008] and sanitization~[Blum et al. 2008] under pure $\epsilon$-differential privacy [Dwork et al. TCC 2006] and approximate $(\epsilon,\delta)$-differential privacy [Dwork et al. Eurocrypt 2006]. We show that the sample complexity of these tasks under approximate differential privacy can be significantly lower than that under pure differential privacy. We define a family of optimization problems, which we call Quasi-Concave Promise Problems, that generalizes some of our considered tasks. We observe that a quasi-concave promise problem can be privately approximated using a solution to a smaller instance of a quasi-concave promise problem. This allows us to construct an efficient recursive algorithm solving such problems privately. Specifically, we construct private learners for point functions, threshold functions, and axis-aligned rectangles in high dimension. Similarly, we construct sanitizers for point functions and threshold functions. We also examine the sample complexity of label-private learners, a relaxation of private learning where the learner is required to only protect the privacy of the labels in the sample. We show that the VC dimension completely characterizes the sample complexity of such learners, that is, the sample complexity of learning with label privacy is equal (up to constants) to learning without privacy.

Abstract--While correlation measures are used to discern statistical relationships between observed variables in almost all branches of datadriven scientific inquiry, what we are really interested in is the existence of causal dependence. Statistical tests for causality, it turns out, are significantly harder to construct; the difficulty stemming from both philosophical hurdles in making precise the notion of causality, and the practical issue of obtaining an operational procedure from a philosophically sound definition. In particular, designing an efficient causality test, that may be carried out in the absence of restrictive presuppositions on the underlying dynamical structure of the data at hand, is nontrivial. Nevertheless, ability to computationally infer statistical prima facie evidence of causal dependence may yield a far more discriminative tool for data analysis compared to the calculation of simple correlations. In the present work, we present a new nonparametric test of Granger causality for quantized or symbolic data streams generated by ergodic stationary sources. In contrast to state-of-art binary tests, our approach makes precise and computes the degree of causal dependence between data streams, without making any restrictive assumptions, linearity or otherwise. Additionally, without any a priori imposition of specific dynamical structure, we infer explicit generative models of causal crossdependence, which may be then used for prediction. These explicit models are represented as generalized probabilistic automata, referred to crossed automata, and are shown to be sufficient to capture a fairly general class of causal dependence. The theoretical results are applied to weekly search-frequency data from Google Trends API for a chosen set of socially "charged" keywords. The causality network inferred from this dataset reveals, quite expectedly, the causal importance of certain keywords. It is also illustrated that correlation analysis fails to gather such insight.

This paper studies the relationship between resolution and conflict driven clause learning (CDCL) without restarts, and refutes some conjectured possible separations. We prove that the guarded, xor-ified pebbling tautology clauses, which Urquhart proved are hard for regular resolution, as well as the guarded graph tautology clauses of Alekhnovich, Johannsen, Pitassi, and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. For the latter set of clauses, we extend this to prove that a CDCL search without restarts can refute these clauses in polynomial time, provided it makes the right choices for decision literals and clause learning. This holds even if the CDCL search is required to greedily process conflicts arising from unit propagation. This refutes the conjecture that the guarded graph tautology clauses or the guarded xor-ified pebbling tautology clauses can be used to separate CDCL without restarts from general resolution. Together with subsequent results by Buss and Ko lodziejczyk, this means we lack any good conjectures about how to establish the exact logical strength of conflict-driven clause learning without restarts.

The minimum message length(MML) principle[7] is an information theoretic criterion that links data compression with statistical inference [6]. It has a number of useful properties and it has close connections with Kolmogorov complexity [8]. Using the MML principle to construct estimators is known to be NPhard in general [4] so it is common to use approximations in practice [6]. The term'strict minimum message length' (SMML) is used for the exact MML criterion, to distinguish it from the various approximations. The only known algorithm for calculating an SMML estimator is Farr's algorithm [4] which applies to data taking values in a finite set which is (in some sense) 1-dimensional. A method for calculating SMML estimators for 1-dimensional exponential families with continuous sufficient statistics was also recently given in [3]. However, calculating SMML estimators for higher-dimensional data is still a difficult problem.

Recent work introduced the cube-and-conquer technique to solve hard SAT instances. It partitions the search space into cubes using a lookahead solver. Each cube is tackled by a conflict-driven clause learning (CDCL) solver. Crucial for strong performance is the cutoff heuristic that decides when to switch from lookahead to CDCL. Yet, this offline heuristic is far from ideal. In this paper, we present a novel hybrid solver that applies the cube and conquer steps simultaneously. A lookahead and a CDCL solver work together on each cube, while communication is restricted to synchronization. Our concurrent cube-and-conquer solver can solve many instances faster than pure lookahead, pure CDCL and offline cube-and-conquer, and can abort early in favor of a pure CDCL search if an instance is not suitable for cube-and-conquer techniques.

We observe a trend regarding restart strategies used in SAT solvers. A few years ago, most state-of-the-art solvers restarted on average after a few thousands of backtracks. Currently, restarting after a dozen backtracks results in much better performance. The main reason for this trend is that heuristics and data structures have become more restart-friendly. We expect further continuation of this trend, so future SAT solvers will restart even more rapidly. Additionally, we present experimental results to support our observations.

The split Bregman (SB) method [T. Goldstein and S. Osher, SIAM J. Imaging Sci., 2 (2009), pp. 323-43] is a fast splitting-based algorithm that solves image reconstruction problems with general l1, e.g., total-variation (TV) and compressed sensing (CS), regularizations by introducing a single variable split to decouple the data-fitting term and the regularization term, yielding simple subproblems that are separable (or partially separable) and easy to minimize. Several convergence proofs have been proposed, and these proofs either impose a "full column rank" assumption to the split or assume exact updates in all subproblems. However, these assumptions are impractical in many applications such as the X-ray computed tomography (CT) image reconstructions, where the inner least-squares problem usually cannot be solved efficiently due to the highly shift-variant Hessian. In this paper, we show that when the data-fitting term is quadratic, the SB method is a convergent alternating direction method of multipliers (ADMM), and a straightforward convergence proof with inexact updates is given using [J. Eckstein and D. P. Bertsekas, Mathematical Programming, 55 (1992), pp. 293-318, Theorem 8]. Furthermore, since the SB method is just a special case of an ADMM algorithm, it seems likely that the ADMM algorithm will be faster than the SB method if the augmented Largangian (AL) penalty parameters are selected appropriately. To have a concrete example, we conduct a convergence rate analysis of the ADMM algorithm using two splits for image restoration problems with quadratic data-fitting term and regularization term. According to our analysis, we can show that the two-split ADMM algorithm can be faster than the SB method if the AL penalty parameter of the SB method is suboptimal. Numerical experiments were conducted to verify our analysis.