Journal on Satisfiability,Boolean Modelling and Computation

We demonstrate hardness results for the detection of small backdoor sets with respect to base classes M r of CNF formulas with maximum deficiency ⩽ r ( M 0 is the class of matched formulas). One of the results applies also to a wide range of base classes with added ‘empty clause detection’ as recently considered by Dilkina, Gomes, and Sabharwal. We obtain the hardness results in the framework of parameterized complexity, considering the upper bound on the size of smallest backdoor sets as the parameter. Furthermore we compare the generality of the parameters maximum deficiency and the size of a smallest M r -backdoor set.

A simple model of signal transduction networks in molecular biology consists of CNF formulas with two and three literals per clause. A necessary condition for correctness of the network model is satisfiability of the formulas. Deciding satisfiability turns out to be NP -complete. However, for a subclass that still is of practical interest, a linear satisfiability algorithm and related characterization of unsatisfiability can be established. The subclass is a special case of so-called closed sums of CNF formulas.

The popular abstraction/refinement model frequently used in verification, can also explain the success of a SAT decision heuristic like Berkmin. According to this model, conflict clauses are abstractions of the clauses from which they were derived. We suggest a clause-based decision heuristic called Clause-Move-To-Front (CMTF), which attempts to follow an abstraction/refinement strategy (based on the resolve-graph) rather than satisfying the clauses in the chronological order in which they were created, as done in Berkmin. We also show a resolution-based score function for choosing the variable from the selected clause and a similar function for choosing the sign. We implemented the suggested heuristics in our SAT solver HaifaSat. Experiments on hundreds of industrial benchmarks demonstrate the superiority of this method comparing to the Berkmin heuristic. HaifaSat won the 3rd place in the industrial-benchmarks category in the SAT competition of 2005, and did not compete or was developed since. We present experimental results with the benchmarks of the 2007 competition that show that it is about 32% slower than RSAT, the winner of 2007. Considering the time difference, it shows that it is rather robust. The abstraction/refinement theoretical model is still relevant, and there is still room for further research on how to exploit it better given a recent result that permits storing and manipulating the resolve graph in the main memory.

The degree of falsity of an inequality in Boolean variables shows how many variables are enough to substitute in order to satisfy the inequality. Goerdt introduced a weakened version of the Cutting Plane (CP) proof system with a restriction on the degree of falsity of intermediate inequalities [6]. He proved an exponential lower bound for CP proofs with degree of falsity bounded by n log 2 n + 1 , where n is the number of variables.

In this paper we strengthen this result by establishing a direct connection between CP and Resolution proofs. This result implies an exponential lower bound on the proof length of Tseitin-Urquhart tautologies when the degree of falsity is bounded by c n for some constant c. We also generalize the notion of degree of falsity for extensions of Lovász-Schrijver calculi (LS), namely for LS k + CP k proof systems introduced by Grigoriev et al. [8]. We show that any LS k + CP k proof with bounded degree of falsity can be transformed into a Res ( k ) proof. We also prove lower and upper bounds on the proof length of tautologies in LS k + CP k with bounded degree of falsity.

Parallel computing has become an affordable reality forcing a shift in the programming paradigm from sequential to concurrent applications, specially those who demand much computational power or with large search spaces like SAT-solvers. In this context we present the research, planning and implementation of PMSat: a parallel version of MiniSAT with MPI (Message Passing Interface) technology, to be executed in clusters or grids of computers. The main features of the program are described: search modes, search space pruning and share of learnt clauses. An analysis of its performance and load balance is also presented.

Current SAT solvers are well engineered and highly efficient, and significant research effort has been put into creating data structures that can produce maximal efficiency for the core propagation engine within SAT solvers. However, there is still substantial room for improvement. As the disparity between CPU speeds and cache sizes have increased, cache conscious data structures and algorithms have become very important. They are even more important in the context of parallel SAT solving, as issues like cache contention and main memory contention can dramatically slow down a parallel SAT solver. We present a series of data structure and algorithmic modifications that are able to increase the core propagation speed of MiniSat 2.0 by an average of 80% on a set of medium sized industrial instances, and increase the speed of a parallelized version of MiniSat running with 8 threads by 140% on those same instances.

We present a new polyhedral approach to nonlinear Boolean optimization. Compared to other methods, it produces much smaller integer programming models, making it more efficient from a practical point of view. We mainly obtain this by two different ideas: first, we do not require the objective function to be in any normal form. The transformation into a normal form usually leads to the introduction of many additional variables or constraints. Second, we reduce the problem to the degree-two case in a very efficient way, by slightly extending the dimension of the original variable space. The resulting model turns out to be closely related to the maximum cut problem; we show that the corresponding polytope is a face of a suitable cut polytope in most cases. In particular, our separation problem reduces to the one for the maximum cut problem.

In practice, the approach appears to be very competitive for unconstrained Boolean optimization problems. First experimental results, which have been obtained for some particularly hard instances of the Max-SAT Evaluation 2007, show that our very general implementation can outperform even special-purpose Max-SAT solvers. The software is accessible online under “we.logoptimize.it”.

In this paper we explore the complexity of various problems pertaining to Input Resolution. In the first part of this paper we survey a number of earlier results for Input Resolution, showing the tractability of various aspects of this proof system. In the second part, we prove the PSPACE-Completeness of both Input Resolution total space and width, as well as a massive size/total space tradeoff for Input Resolution. These results suggest that although Input Resolution is completely tractable with respect to certain complexity measures such as refutation size, when quantities such as space and width are considered, the system shows a surprising level of difficulty.

The quantifier-free extensional theory of arrays T A plays an important role in hardware and software verification. In this article we present a novel decision procedure that refines formula abstractions with lemmas on demand. We consider the case where T A is combined with a decidable quantifier-free first-order theory T B . Unlike traditional lazy SMT approaches, where lemmas are added on the boolean abstraction layer, our decision procedure adds lemmas in T B . We discuss our decision procedure in detail. In particular, we prove soundness and completeness, and discuss complexity. We present our decision procedure in a generic context and provide implementation details and optimizations, in particular for bit-vectors. Finally, we report on experiments and discuss related work.