Intensification and diversification are the key factors that control the performance of stochastic local search in satisfiability (SAT). Recently, Novelty Walk has become a popular method for improving diversification of the search and so has been integrated in many well-known SAT solvers such as TNM and gNovelty + . In this paper, we introduce new heuristics to improve the effectiveness of Novelty Walk in terms of reducing search stagnation. In particular, we use weights (based on statistical information collected during the search) to focus the diversification phase onto specific areas of interest. With a given probability, we select the most frequently unsatisfied clause instead of a totally random one as Novelty Walk does. Amongst all the variables appearing in the selected clause, we then select the least flipped variable for the next move. Our experimental results show that the new weight-enhanced diversification method significantly improves the performance of gNovelty$^+$ and thus outperforms other local search SAT solvers on a wide range of structured and random satisfiability benchmarks.

We will show how human computation insights can be key to identifying so-called backdoor variables in combinatorial optimization problems. Backdoor variables can be used to obtain dramatic speed-ups in combinatorial search. Our approach leverages the complementary strength of human input, based on a visual identification of problem structure, crowdsourcing, and the power of combinatorial solvers to exploit complex constraints. We describe our work in the context of the domain of materials discovery. The motivation for considering the materials discovery domain comes from the fact that new materials can provide solutions for key challenges in sustainability, e.g., in energy, new catalysts for more efficient fuel cell technology.

The number partitioning problem seeks to divide a set of n numbers across k distinct subsets so as to minimize the sum of the largest partition. In this work, we develop a new optimal algorithm for multi-way number partitioning. A critical observation motivating our methodology is that a globally optimal k -way partition may be recursively constructed by obtaining suboptimal solutions to subproblems of size k – 1. We introduce a new principle of optimality that provides necessary and sufficient conditions for this construction, and use it to strengthen the relationship between sequential decompositions by enforcing upper and lower bounds on intermediate solutions. We also demonstrate how to further prune unpromising partial assignments by detecting and eliminating dominated solutions. Our approach outperforms the previous state-of-the-art by up to four orders of magnitude , reducing average runtime on the largest benchmarks from several hours to less than a second.

It is widely acknowledged that stochastic local search (SLS) algorithms can efficiently find models of satisfiable formulae for the Boolean Satisfiability (SAT) problem. There has been much interest in studying SLS algorithms on random $k$-SAT instances. Compared to random 3-SAT instances which have special statistical properties rendering them easy to solve, random $k$-SAT instances with long clauses are similar to structured ones and remain very difficult. This paper is devoted to efficient SLS algorithms for random $k$-SAT instances with long clauses. By combining a novel variable property $subscore$ with the commonly used property $score$, we design a scoring function named {\it comprehensive score}, which is utilized to develop a new SLS algorithm called CScoreSAT. The experiments show that CScoreSAT outperforms state-of-the-art SLS solvers, including the winners of recent SAT competitions, by one to two orders of magnitudes on large random 5-SAT and 7-SAT instances. In addition, CScoreSAT significantly outperforms its competitors on random $k$-SAT instances for each $k=4,5,6,7$ from SAT Challenge 2012, which indicates its robustness.

Single-peakedness is one of the most commonly used domain restrictions in social choice. However, the extent to which agent preferences are single-peaked in practice, and the extent to which recent proposals for \emph{approximate single-peakedness} can further help explain voter preferences, is unclear. In this article, we assess the ability of both single-dimensional and multi-dimensional approximations to explain preference profiles drawn from several real-world elections. We develop a simple \emph{branch-and-bound} algorithm that finds multi-dimensional, single-peaked axes that best fit a given profile, and which works with several forms of approximation. Empirical results on two election data sets show that preferences in these elections are far from single-peaked in any one-dimensional space, but are nearly single-peaked in two dimensions. Our algorithms are reasonably efficient in practice, and also show excellent anytime performance.

We focus on solving two-player zero-sum extensive-form games with perfect information and simultaneous moves. In these games, both players fully observe the current state of the game where they simultaneously make a move determining the next state of the game. We solve these games by a novel algorithm that relies on two components: (1) it iteratively solves the games that correspond to a single simultaneous move using a double-oracle method, and (2) it prunes the states of the game using bounds on the sub-game values obtained by the classical Alpha-Beta search on a serialized variant of the game. We experimentally evaluate our algorithm on the Goofspiel card game, a pursuit-evasion game, and randomly generated games. The results show that our novel algorithm typically provides significant running-time improvements and reduction in the number of evaluated nodes compared to the full search algorithm.

Natural deduction, which is a method for establishing validity of propositional type arguments, helps develop important reasoning skills and is thus a key ingredient in a course on introductory logic. We present two core components, namely solution generation and practice problem generation, for enabling computer-aided education for this important subject domain. The key enabling technology is use of an offline-computed data-structure called Universal Proof Graph (UPG) that encodes all possible applications of inference rules over all small propositions abstracted using their bitvector-based truth-table representation. This allows an efficient forward search for solution generation. More interestingly, this allows generating fresh practice problems that have given solution characteristics by performing a backward search in UPG. We obtained around 300 natural deduction problems from various textbooks. Our solution generation procedure can solve many more problems than the traditional forward-chaining based procedure, while our problem generation procedure can efficiently generate several variants with desired characteristics.

We present algorithms for generating alternative solutions for explicit acyclic AND/OR structures in non-decreasing order of cost. Our algorithms use a best first search technique and report the solutions using an implicit representation ordered by cost. Experiments on randomly constructed AND/OR DAGs and problem domains including matrix chain multiplication, finding the secondary structure of RNA, etc, show that the proposed algorithms perform favorably to the existing approach in terms of time and space.

This paper addresses the Target-Value Search (TVS) problem, which is the problem of finding a path between two nodes in a graph whose cost is as close as possible to a given target value, T. This problem has been previously addressed only for directed acyclic graphs. In this work we develop the theory required to solve this problem optimally for any type of graphs. We modify traditional heuristic search algorithms for this setting, and propose a novel bidirectional search algorithm that is specifically suited for TVS. The benefits of this bidirectional search algorithm are discussed both theoretically and experimentally on several domains.

This paper investigates the manpower allocation problem with time windows and job-teaming constraints(MAPTWTC), a practical scheduling and routing problem that tries to synchronize workers’ schedules to complete all tasks. We first provide an integer programming model for the problem and discuss its properties. Next, we show that tree data structure can be used to represent the MAPTWTC solutions, and its optimal solution can be obtained from one of trees by solving a minimum cost flow model for each worker type. Consequently, we develop for the problem a novel tabu search algorithm employing search operators based on the tree data structure. Finally, we prove the effectiveness of the tabu search algorithm by computational experiments on two sets of instances.