Journal on Satisfiability,Boolean Modelling and Computation

An independent set of variables is one in which no two variables occur in the same clause in a given k-SAT instance. Recently, independent sets have obtained more attention. Due to a simple observation we prove that a k-SAT instance over n variables with independent set of size i can be solved in time O ( ϕ 2 ( k − 1 ) ( n − i ) ) where ϕ k ( n ) denotes an upper bound on the complexity of solving k-SAT over n variables.

In this paper, nogood recording is investigated for CSP within the randomization and restart framework. Our goal is to avoid the same situations to occur from one run to the next ones. More precisely, nogoods are recorded when the current cutoff value is reached, i.e. before restarting the search algorithm. Such a set of nogoods is extracted from the last branch of the current search tree and exploited using the structure of watched literals originally proposed for SAT. We prove that the worst-case time complexity of extracting such nogoods at the end of each run is only O ( n 2 d ) where n is the number of variables of the constraint network and d the size of the greatest domain, whereas for any node of the search tree, the worst-case time complexity of exploiting these nogoods to enforce Generalized Arc Consistency (GAC) is O ( n | B | ) where | B | denotes the number of recorded nogoods. As the number of nogoods recorded before each new run is bounded by the length of the last branch, the total number of recorded nogoods is polynomial in the number of restarts. Interestingly, we show that when the minimization of the nogoods is envisioned with respect to an inference operator ϕ, it is possible to directly identify some nogoods that cannot be minimized. For ϕ = AC (i.e. for MAC), the worst-case time complexity of extracting minimal nogoods is slightly increased to O ( e n 2 d 3 ) where e is the number of constraints of the network. Experimentation over a wide range of CSP instances using a generic state-of-the-art CSP solver demonstrates the effectiveness of this approach. Recording nogoods (and in particular, minimal nogoods) from restarts significantly improves the robustness of the solver.

In this paper, we address the issue of designing from SAT new value ordering heuristics for CSP. We show that using the direct and support SAT encodings of CSP instances, such heuristics can be naturally derived from the well-known two-sided Jeroslow-Wang heuristic. These heuristics exploit the bi-directionality of constraint supports to give a more comprehensive picture in terms of domain reduction when a given value is assigned to (resp. removed from) a given variable. Interestingly, in the context of a backtracking search algorithm that exploits binary branching and the adaptive variable ordering heuristic dom/wdeg, we experimentally observed that the new heuristics yielded the best results on satisfiable and unsatisfiable instances when following the promise and the fail-first policies, respectively.

Recently, off-the-shelf Boolean SAT solvers have been used to construct ground decision procedures for various theories, including Quantifier-Free Presburger (QFP) arithmetic. One such approach (often called the eager approach) is based on a satisfiability-preserving translation to a Boolean formula. Eager approaches are usually based on encoding integers as bit-vectors and su er from the loss of structure and sometime very large size for the bit-vectors.

In this paper, we present a decision procedure for QFP that is based on alternately under and over-approximating a formula, where Boolean interpolants are used to compute the overapproximation. The novelty of the approach lies in using information from each phase (either underapproximation or overapproximation) to improve the other phase. Our preliminary experiments indicate that the algorithm consistently outperforms approaches based on eager and very lazy methods, on a set of verification benchmarks. In our experience, the use of interpolants results in better abstractions being generated compared to an earlier method based on proofs directly.

In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions, we provide a tight integration of recent SAT solving techniques with interval-based arithmetic constraint solving. Our approach deviates substantially from lazy theorem proving approaches in that it directly controls arithmetic constraint propagation from the SAT solver rather than delegating arithmetic decisions to a subordinate solver. Through this tight integration, all the algorithmic enhancements that were instrumental to the enormous performance gains recently achieved in propositional SAT solving carry over smoothly to the rich domain of non-linear arithmetic constraints. As a consequence, our approach is able to handle large constraint systems with extremely complex Boolean structure, involving Boolean combinations of multiple thousand arithmetic constraints over some thousands of variables.