SAT on Monday, August 14th

Invited Talk (09:00‑10:00)
Chair: Carla P. Gomes
Location: Metropolitan B

09:00‑10:00

Fahiem Bacchus (University of Toronto, Canada) CSPs: Adding Structure to SAT [ppt] One way of viewing the difference between SAT and CSPs is to think of programming in assembler vs programming in C. It can be considerably simpler to program in C than assembler. Similarly it can be considerably simpler to model real world problems in CSP than in SAT. On the other hand C's machine model is still rather close to the underlying hardware model accessed directly in assembler. Similarly, in CSPs the main method of reasoning, backtracking search, can be viewed as being an extension of DPLL, the main method of reasoning for SAT. Where the analogy breaks down is that unlike C and assember whose machine models are computationally equivalent, some CSP techniques offer a considerable boost in inferential power over the resolution inferences preformed in DPLL. An intresting question is how to combine this additional inferential power with the more powerful forms of resolution preformed in modern DPLL solvers. One approach for achieving such a combination will be presented.

Break (10:00‑10:30)

Session 6: MAX-SAT (10:30‑12:30)
Chair: Ewald Speckenmeyer
Location: Metropolitan B

10:30‑11:00	María Luisa Bonet (Universitat Politčcnica de Catalunya) Jordi Levy (IIIA - CSIC) Felip Manyŕ (IIIA - CSIC) A Complete Calculus for Max-SAT Max-SAT is the problem of finding an assignment minimizing the number of unsatisfied clauses of a given CNF formula. We propose a resolution-like calculus for Max-SAT and prove its soundness and completeness. We also prove the completeness of some refinements of this calculus. From the completeness proof we derive an exact algorithm for Max-SAT and a time upper bound.
11:00‑11:30	Zhaohui Fu (Princeton University) Sharad Malik (Princeton University) On Solving The Partial MAX-SAT Problem Boolean Satisfiability (SAT) has seen many successful applications in various fields, such as Electronic Design Automation and Artificial Intelligence. In each of these, the problem constraints are encoded into a propositional logic formula, typically represented in Conjuncted Normal Form (CNF). However, in some cases, it may be required/preferable to use variations of the general SAT problem. In this paper, we consider one important variation, the Partial MAX-SAT problem. Unlike SAT, Partial MAX-SAT has certain constraints (clauses) that are marked as relaxable and the rest are hard, i.e. non-relaxable. The objective is to find a variable assignment that satisfies all non-relaxable clauses together with the maximum number of relaxable ones. Partial MAX-SAT has various applications, including multiple property checking, FPGA routing, scheduling, etc. We have implemented two solvers for the Partial MAX-SAT problem using a contemporary SAT solver, zChaff. The first approach is a novel diagnosis based algorithm; it iteratively analyzes the UNSAT core of the current SAT instance and eliminates the core through a modification of the problem instance by adding relaxation variables. The second approach is encoding based; it constructs an efficient auxiliary counter that constrains the number of relaxed clauses and supports binary search or linear scan for the optimal solution. Both solvers are complete as they guarantee the optimality of the solution. Further, we show how both techniques lend themselves naturally to the benefits from the persistent learning techniques of incremental SAT. Experiments using practical instances of this problem show significant improvements over the best known solvers. We also discuss the relative strengths and thus applicability of the two solvers for different solution scenarios.
11:30‑12:00	Evgeny Dantsin (Roosevelt University) Alexander Wolpert (Roosevelt University) MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster than in $O(2^n)$ Time We give an exact deterministic algorithm for MAX-SAT. On input CNF formulas with constant clause density (the ratio of the number of clauses to the number of variables is a constant), this algorithm runs in $O(c^n)$ time where $c<2$ and $n$ is the number of variables. Worst-case upper bounds for MAX-SAT less than $O(2^n)$ were previously known only for $k$-CNF formulas and for CNF formulas with small clause density.
12:00‑12:15	Osamu Watanabe (Tokyo Institute of Technology) Masaki Yamamoto (Tokyo Institute of Technology) Average-case analysis of the MAX-2SAT problem We propose a simple probability model for MAX-2SAT instances for discussing the average-case complexity of the MAX-2SAT problem. Our mode is a planted solution model, where each instance is generated randomly from a target solution. We show that for a large range of parameters, the planted solution is in fact the unique optimum solution for the generated instance with high probability. We then give one very simple linear time algorithm based on a message passing method, and we prove that it indeed solves the MAX-2SAT problem with high probability for a certain range of parameters.
12:15‑12:30	Chu Min Li MAX-SAT Evaluation Information on the MAX-SAT Evaluation resides on a seperate page.

Lunch break (12:30‑14:00)

Session 7: Local Search and Survey Propagation (14:00‑16:00)
Chair: Hans van Maaren
Location: Metropolitan B

14:00‑14:30	Steven Prestwich (Cork Constraint Computation Centre) Ines Lynce (IST/INESC-ID, Technical University of Lisbon) Local Search for Unsatisfiability Local search is widely applied to satisfiable SAT problems, and on some classes outperforms backtrack search. An interesting challenge posed by Selman, Kautz and McAllester in 1997 is to use it to prove unsatisfiability. We investigate two distinct approaches. Firstly we apply standard local search to a reformulation of the problem, such that a solution to the reformulation corresponds to a refutation of the original problem. Secondly we design a greedy randomised resolution algorithm that can handle proofs of any size while using bounded memory, and has a completeness property. We report initial successes with both approaches.
14:30‑15:00	Andrei Bulatov (Simon Fraser University) Evgeny Skvortsov (Simon Fraser University) Efficiency of Local Search The Local Search algorithm is one of the simplest heuristic algothms for solving the MAX-SAT problem. The goal of this paper is to estimate the relative error produced by this algorithm being applied to random 3-CNFs with fixed density $r$. We prove that, for any $r$, there is a constant $c$ such that a weakened version of Local Search that we call One-Pass Local Search almost surely outputs an assignment containing $cn+o(n)$ unsatisfied clauses. Then using certain assumtions we also show this for Local Search. Although the assumptions remain unproved the results well matches experiments.
15:00‑15:30	Panagiotis Manolios (Georgia Tech) Yimin Zhang (Georgia Institute of Technology) Implementing Survey Propagation on Graphics Processing Units We show how to exploit the raw power of current graphics processing units (GPUs) to obtain implementations of SAT solving algorithms that surpass the performance of CPU-based algorithms. We have developed a GPU-based version of the survey propagation algorithm, an incomplete method capable of solving hard instances of random k-CNF problems close to the critical threshold with millions of propositional variables. Our experimental results show that our GPU-based algorithm attains about a nine-fold improvement over the fastest known CPU-based algorithms running on high-end processors.
15:30‑16:00	Eric Hsu (University of Toronto) Sheila McIlraith (University of Toronto) Characterizing Propagation Methods for Boolean Satisfiability Iterative algorithms such as Belief Propagation and Survey Propagation can handle some of the largest randomly-generated satisfiability problems (SAT) created to this point. But they can make inaccurate estimates or fail to converge on instances whose underlying constraint graphs contain small loops--a particularly strong concern with structured problems. More generally, their behavior is only well-understood in terms of statistical physics on a specific underlying model. Our alternative characterization of propagation algorithms presents them as value and variable ordering heuristics whose operation can be codified in terms of the Expectation Maximization (EM) method. Besides explaining failure to converge in the general case, understanding the equivalence between Propagation and EM yields new versions of such algorithms. When these are applied to SAT, such an understanding even yields a slight modification that guarantees convergence.

Break (16:00‑16:30)

Keynote Session: Marking the Gödel Centenary (16:30‑18:00)
Chair: Wolfram Schulte, Moshe Vardi
Location: Metropolitan A and B

16:30‑17:15

John Dawson (Penn State, York Campus) Shaken Foundations or Groundbreaking Realignment? A Centennial Assessment of Kurt Gödel's Impact on Logic, Mathematics, and Computer Science [ppt] The publication of Gödel's incompleteness theorems, seventy-five years ago, has often been portrayed as a devastating event -- one that undermined Hilbert's program for securing the foundations of mathematics and showed the axiomatic method to be incapable of yielding all truths of arithmetic -- resulting, according to one eminent critic, in an irredeemable "loss of certainty" within mathematics. On the other hand, Gödel has also been credited with having demonstrated that the human mind is inherently superior to any computer, thereby settling once and for all the long-standing debate over mind versus mechanism. In fact, both those accounts are caricatures. Gödel's impact on modern logic, and, less directly, on computer science, has been profound; but mathematical practice has hardly been affected by the incompleteness theorems, and their philosophical significance remains a subject of debate. Nor is mathematics less "secure" than it was before Gödel's work. Indeed, his proof that the axiom of choice is consistent with the other axioms of set theory put an end to one of the most contentious foundational debates of the century.

17:15‑18:00

Dana Scott (Carnegie Mellon University) The Future of Proof [pdf] ...