We develop an Answer Set Programming (ASP)-based approach for computing the smallest bidirectional macro schemes (BMSs), a fundamental NP-hard optimization problem in dictionary-based compression. Our approach relies on high-level ASP encodings and delegates both the grounding and solving tasks to an off-the-shelf ASP solver. The proposed encoding is compact and extensible, and leverages advanced ASP techniques to improve scalability, including ASP modulo acyclicity and refined declarative encodings of acyclicity constraints. We further show that our ASP encoding can be naturally extended to compute the smallest straight-line programs (SLPs), another important NP-hard measure of repetitiveness. Furthermore, we establish the competitiveness of our approach by empirically contrasting it with a more dedicated MaxSAT-based approach.

In this paper, we propose an enhancement to the SAT-based counterexample-guided abstraction refinement (CEGAR) approach for solving the Hamiltonian Cycle Problem (HCP). Many SAT-based methods for HCP have been proposed, including a CEGAR-based method that repeatedly solves a relaxed version of HCP strengthened by counterexamples. However, when the counterexample space - represented by the full set of subcycle partitions - is large, it becomes difficult to find a solution. To address this, we introduce cut-set constraints in the refinement step, replacing traditional subcycle blocking constraints. Our evaluation shows that these cut-set constraints achieve equal or better reduction in the counterexample space, making it easier to find valid solutions. We further assessed performance using all 1001 instances from the FHCP challenge set and confirmed that the proposed method solved 937 instances within 1800 seconds, outperforming both the existing eager and CEGAR encodings (which solved at most 666 instances). This demonstrates the effectiveness of incorporating cut-set constraints into SAT-based CEGAR approaches.

We propose Large Neighborhood Prioritized Search (LNPS) for solving combinatorial optimization problems in Answer Set Programming (ASP). LNPS is a metaheuristic that starts with an initial solution and then iteratively tries to find better solutions by alternately destroying and prioritized searching for a current solution. Due to the variability of neighborhoods, LNPS allows for flexible search without strongly depending on the destroy operators. We present an implementation of LNPS based on ASP. The resulting heulingo solver demonstrates that LNPS can significantly enhance the solving performance of ASP for optimization. Furthermore, we establish the competitiveness of our LNPS approach by empirically contrasting it to (adaptive) large neighborhood search.

This paper describes techniques for simplifying a propositional clausal formula during the search process of the satisfiability checking of the formula. Generally, simplification technique has a trade-off between the checking cost and the effect of it. If the simplification technique is executed during search, then the cost can be problematic. We propose some on-the-fly simplification techniques whose computational cost is negligibly small. Hence, these techniques are executed frequently throughout the process of a CDCL solver, that is, unit propagation, conflict analysis, removal of satisfied clauses, etc. The proposed simplification techniques are based on binary resolvents, which are derived from unit propagation process, and consist of various probing techniques, self-subsuming resolution and on-demand addition of binary resolvents. The experimental results show that these simplification techniques can improve the performance of CDCL solvers.

Meta-level abduction is a method to abduce missing rules in explaining observations. By representing rule structures of a problem in a form of causal networks, meta-level abduction infers missing links and unknown nodes from incomplete networks to complete paths for observations. We examine applicability of meta-level abduction on networks containing both positive and negative causal effects. Such networks appear in many domains including biology, in which inhibitory effects are important in several biological pathways. Reasoning in networks with inhibition involves nonmonotonic inference, which can be realized by making default assumptions in abduction. We show that meta-level abduction can consistently produce both positive and negative causal relations as well as invented nodes. Case studies of meta-level abduction are presented in p53 signaling networks, in which causal relations are abduced to suppress a tumor with a new protein and to stop DNA synthesis when damage has occurred. Effects of our method are also analyzed through experiments of completing networks randomly generated with both positive and negative links.

We propose a satisfiability testing (SAT) based exact approach for solving the two-dimensional strip packing problem (2SPP). In this problem, we are given a set of rectangles and one large rectangle called a strip. The goal of the problem is to pack all rectangles without overlapping, into the strip by minimizing the overall height of the packing. Although the 2SPP has been studied in Operations Research, some instances are still hard to solve. Our method solves the 2SPP by translating it into a SAT problem through a SAT encoding called order encoding. The translated SAT problems tend to be large; thus, we apply several techniques to reduce the search space by symmetry breaking and positional relations of rectangles. To solve a 2SPP, that is, to compute the minimum height of a 2SPP, we need to repeatedly solve similar SAT problems. We thus reuse learned clauses and assumptions from the previously solved SAT problems. To evaluate our approach, we obtained results for 38 instances from the literature and made comparisons with a constraint satisfaction solver and an ad-hoc 2SPP solver.

In this paper, we propose two kinds of semi-automatic training-example generation algorithms for rapidly synthesizing a domain-specific Web search engine. We use the keyword spice model, as a basic framework, which is an excellent approach for building a domain-specific search engine with high precision and high recall. The keyword spice model, however, requires a huge amount of training examples which should be classified by hand. For overcoming this problem, we propose two kinds of refinement algorithms based on semi-automatic training-example generation: (i) the sample decision tree based approach, and (ii) the similarity based approach. These approaches make it possible to build a highly accurate domain-specific search engine with a little time and effort. The experimental results show that our approaches are very effective and practical for the personalization of a general-purpose search engine

In this paper, we study frequent subsequence extraction from a single very-long data-sequence. First we propose a novel frequency measure, called the total frequency, for counting multiple occurrences of a sequential pattern in a single data sequence. The total frequency is anti-monotonic, and makes it possible to count up pattern occurrences without duplication. Moreover the total frequency has a good property for implementation based on the dynamic programming strategy. Second we give a simple on-line algorithm for a specialized subsequence extraction problem, i.e., a problem with the infinite window-length. This specialized problem is considered to be a relaxation of the general-case problem, thus this fast on-line algorithm is important from the view of practical applications.

In recent years, research on planning algorithms has made big progress. Recent approaches encode the plan search space into a data structure called the planning graph. To extract plans, a planning graph is transformed into the satisfiability problem (SAT), which is solved by a high-speed SAT solver. This kind of planning is called SAT planning. On the other hand, recent research on reasoning about action has also progressed. Since Gelfond and Lifschitz (1993) proposed the action language /spl Ascr/, a lot of work has been done to improve action languages. We combine these two approaches. Namely, we extend techniques for SAT planning to cover other aspects of reasoning about action, so that various types of queries can be answered for action languages. For this purpose, we implemented an action language processing system AMP in Java. Using this system, it becomes possible to answer queries for not only planning but model generation for a domain description written in the action language /spl Ascr/.