A string attractor of a string T[1..|T|] is a set of positions Γ of T such that any substring w of T has an occurrence that crosses a position in Γ, i.e., there is a position i such that w = T[i..i+|w|-1] and the intersection [i,i+|w|-1]∩ Γ is nonempty. The size of the smallest string attractor of Fibonacci words is known to be 2. We completely characterize the set of all smallest string attractors of Fibonacci words, and show a recursive formula describing the 2^{n-4} + 2^{⌈n/2⌉ - 2} distinct position pairs that are the smallest string attractors of the nth Fibonacci word for n ≥ 7. Similarly, the size of the smallest string attractor of period-doubling words is known to be 2. We also completely characterize the set of all smallest string attractors of period-doubling words, and show a formula describing the two distinct position pairs that are the smallest string attractors of the nth period-doubling word for n ≥ 2. Our results show that strings with the same smallest attractor size can have a drastically different number of distinct smallest attractors.

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.

We present SRIP, a SAT-based system for solving the Independent Set Reconfiguration Problem (ISRP) under the Token Jumping (TJ) rule. SRIP formulates ISRP with SAT problems employing a clique-partition-based constraint model and a set of pruning constraints that strengthen propagation and reduce the search space for reconfiguration. The resulting model is compiled into a sequence of SAT problems and solved using incremental SAT within a bounded model checking framework, enabling SRIP to compute shortest reconfiguration sequences efficiently. We evaluate SRIP on benchmark instances from the CoRe Challenge, a competition series dedicated to ISRP under TJ. SRIP finds optimal (shortest) reconfiguration sequences for 477 out of 693 instances, achieving the best results among state-of-the-art solvers on this benchmark suite.

We introduce the Multi-Objective Combinatorial Reconfiguration Optimization Problem (MO-CROP), and propose an Answer Set Programming (ASP) based approach for its solution. MO-CROP involves finding the Pareto-optimal sequences (or Pareto front) of adjacent feasible solutions between two given feasible solutions of a combinatorial problem, considering both cost and length. Our algorithm is compactly implemented through multi-shot ASP solving, and its implementing solver optirecon provides an effective tool for solving MO-CROP. As a concrete example of MO-CROP, we present an ASP encoding for solving the multi-objective independent set reconfiguration optimization problem. Experimental results on the benchmark set from the recent CoRe Challenge demonstrate our approach’s ability to capture diverse optimal sequences that reveal trade-offs between cost and length, a capability often lacking in traditional combinatorial reconfiguration methods.

Boolean networks (BNs) are widely used to model biological regulatory networks. Attractors here hold significant meaning as they represent long-term behaviors such as homeostasis and the results of cell differentiation. As such, computing attractors is of critical importance to guarantee the validity of a model or to assess its stability and robustness. However, this problem is quite challenging when it comes to large real-world models. To overcome the limits of state-of-the-art BDD-based or ASP-based enumeration approaches, we introduce a SAT-based approach to compute fixed points (singleton attractors) of BN and exhibit its merits for counting the number of singleton attractors of large-scale benchmarks well established in the literature.

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.

Abstract The dominating set reconfiguration problem is defined as determining, for a given dominating set problem and two among its feasible solutions, whether one is reachable from the other via a sequence of feasible solutions subject to a certain adjacency relation. This problem is PSPACE-complete in general. The concept of the dominating set is known to be quite useful for analyzing wireless networks, social networks, and sensor networks. We develop an approach to solve the dominating set reconfiguration problem based on answer set programming (ASP). Our declarative approach relies on a high-level ASP encoding, and both the grounding and solving tasks are delegated to an ASP-based combinatorial reconfiguration solver. To evaluate the effectiveness of our approach, we conduct experiments on a newly created benchmark set.

Abstract We present the third generation of the constraint answer set system clingcon , combining Answer Set Programming (ASP) with finite domain constraint processing (CP). While its predecessors rely on a black-box approach to hybrid solving by integrating the CP solver gecode , the new clingcon system pursues a lazy approach using dedicated constraint propagators to extend propagation in the underlying ASP solver clasp . No extension is needed for parsing and grounding clingcon 's hybrid modeling language since both can be accommodated by the new generic theory handling capabilities of the ASP grounder gringo . As a whole, clingcon 3 is thus an extension of the ASP system clingo 5, which itself relies on the grounder gringo and the solver clasp . The new approach of clingcon offers a seamless integration of CP propagation into ASP solving that benefits from the whole spectrum of clasp 's reasoning modes, including, for instance, multi-shot solving and advanced optimization techniques. This is accomplished by a lazy approach that unfolds the representation of constraints and adds it to that of the logic program only when needed. Although the unfolding is usually dictated by the constraint propagators during solving, it can already be partially (or even totally) done during preprocessing. Moreover, clingcon 's constraint preprocessing and propagation incorporate several well-established CP techniques that greatly improve its performance. We demonstrate this via an extensive empirical evaluation contrasting, first, the various techniques in the context of CSP solving and, second, the new clingcon system with other hybrid ASP systems.

This paper proposes a new hybrid encoding of finite linear CSP to SAT integrating order and log encodings. The former maintains bound consistency by unit propagation and works well for instances with small/middle domain sized variables and/or arity of constraints. The latter generates smaller CNF and is suitable for instances with larger domain sized variables, but its performance is not good in general because more inference steps are required to ripple carries. This paper describes the first attempt of hybridizing the order and log encodings without channeling. Each variable is encoded by either the order encoding or the log encoding, and each constraint can contain both types of variables. We evaluate its performance with two benchmark sets. The first one consists of our handmade instances to verify the synergy effect of the hybridization. The second one consists of 1002 instances from the 2009 CSP solver competition to have a comprehensive evaluation on a wide variety of problems. The result shows the proposed hybrid encoding solves several instances which cannot be solved by both two encodings and its performance is superior to them.

This paper presents a SAT-based pseudo-Boolean (PB for short) solver named PBSugar. PBSugar translates a PB instance to a SAT instance by using the order encoding, andsearches its solution by using an external SAT solver, such as Glucose. We first introduce an optimized version of the order encoding, and it is appliedto encode each PB constraint a1x1+...anxn# k. The encoding isreformulated as a sparse Boolean matrix, named Counter Matrix, of size n × (k+1) constructed for each PB constraint. The same Counter Matrix can be usedfor any relations ≥, ≤, =, and ≠, and can be reused for other PBconstraints having common sub-terms. The experimental results for 669 instances of DEC-SMALLINT-LIN category(decision problems, small integers, linear constraints) demonstrates thesuperior performance of PBSugar compared to other state-of-the-art PB solvers interms of the number of solved instances within the given time limit.

Abstract The course timetabling problem can be generally defined as the task of assigning a number of lectures to a limited set of timeslots and rooms, subject to a given set of hard and soft constraints. The modeling language for course timetabling is required to be expressive enough to specify a wide variety of soft constraints and objective functions. Furthermore, the resulting encoding is required to be extensible for capturing new constraints and for switching them between hard and soft, and to be flexible enough to deal with different formulations. In this paper, we propose to make effective use of ASP as a modeling language for course timetabling. We show that our ASP-based approach can naturally satisfy the above requirements, through an ASP encoding of the curriculum-based course timetabling problem proposed in the third track of the second international timetabling competition (ITC-2007). Our encoding is compact and human-readable, since each constraint is individually expressed by either one or two rules. Each hard constraint is expressed by using integrity constraints and aggregates of ASP. Each soft constraint S is expressed by rules in which the head is the form of penalty(S,V,C), and a violation V and its penalty cost C are detected and calculated respectively in the body. We carried out experiments on four different benchmark sets with five different formulations. We succeeded either in improving the bounds or producing the same bounds for many combinations of problem instances and formulations, compared with the previous best known bounds.

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.