Abstract: This paper proposes a new algorithm for the genomic median problem that combines greedy and stochastic search. Our computational experiments suggest that for more complex problems our algorithm finds better solutions than previous approaches. In particular we find an improved midpoint for a human-mouse-rat comparison with 424 markers. In order to understand why such problems are hard, we explore a phase transition in the complexity of the median problem for random data, associated with the emergence of a giant component in the breakpoint graph.
Abstract:
In the past few years we have seen significant progress in the area of
Boolean satisfiability (SAT) solving and its applications. More
recently, new efforts have focused on developing solvers for
Quantified Boolean Formulas (QBFs). Recent QBF evaluation results
show that developing practical QBF solvers is more challenging than
one might expect. Even relatively small QBF problems are sometimes
beyond the reach of current QBF solvers. We present a new approach for
solving unsatisfiable two-alternation QBFs. Our approach is able to
solve hard random QBF formulas that current algorithms are not able
to handle.
Our solver WaklMinQBF combines the power of stochastic local search
methods and complete SAT solvers. Our solver is incomplete and outputs
unsat if a certificate for unsatisfiability is found
otherwise it outputs unknown . To test our approach, we use
the model for random formulas introduced in (Chen and Interian 2005)
and the models A and B introduced in (Gent and Walsh 1999). We
compare WaklMinQBF with the state-of-the-art QBF solvers Ssolve and
Qube-BJ. We show that WaklMinQBF outperforms these solvers in time and in
the number of formulas solved. We believe our work provides new
insights on strategies that should be useful in complete QBF solvers.
As a side result we have developed a stochastic local search algorithm
for the minimum unsatisfiability problem (MIN-SAT).
Abstract: The quantified boolean formula (QBF) problem is a powerful generalization of the boolean satisfiability (SAT) problem where variables can be both universally and existentially quantified. Inspired by the fruitfulness of the established model for generating random SAT instances, we define and study a general model for generating random QBF instances. We exhibit experimental results showing that our model bears certain desirable similarities to the random SAT model, as well as a number of theoretical results concerning our model.
Abstract: We consider a model for generating random k-SAT formulas, in which each literal occurs approximately the same number of times in the formula clauses (regular random k-SAT). Our experimental results show that such regular random k-SAT instances are much harder than the usual uniform random k-SAT problems. This is in agreement with other results that show that more balanced instances of random combinatorial problems are often much more difficult to solve than uniformly random instances, even at phase transition boundaries. There are almost no formal results known for such problem distributions. The balancing constraints add a dependency between variables that complicates a standard analysis. Regular random 3-SAT exhibits a phase transition as a function of the ratio r of clauses to variables. The transition takes place at approximately r=3.5. We will show that for r > 3.78 w.h.p. random Regular 3-SAT formulas are unsatisfiable. We will also show that the analysis of a greedy algorithm proposed in Kaporis et al for the uniform 3-SAT model can be adapted for regular random 3-SAT. In particular, we show that for formulas with ratio r < 2.46, a greedy algorithm finds a satisfying assignment with positive probability.
Abstract: We provide a rigorous analysis of a greedy approximation algorithm for the maximum random k-SAT (MAX-R-kSAT) problem. The algorithm assigns variables one at a time in a predefined order. A variable is assigned TRUE if it occurs more often positively than negatively; otherwise, it is assigned FALSE. After eachvariable assignment, problem instance is simplified and a new variable is selected. We show that this algorithm gives a 10/9.5-approximation, improving over the 9/8-approximation given by de la Vega and Karpinski 2002. The new approximation ratio is achieved by using a different algorithm than the one proposed in de la Vega and Karpinski 2002, along with a new upper bound on the maximum number of clauses that can be satisfied in a random k-SAT formula (Achlioptas et al 2003) .