We develop an approach to solve curriculum-based course timetabling (CB-CTT) problems with Large Neighborhood Prioritized Search (LNPS) based on Answer Set Programming (ASP). LNPS is a metaheuristic that starts with an initial solution and then ...

We propose an approach called bounded combinatorial reconfiguration for solving combinatorial reconfiguration problems based on Answer Set Programming (ASP). The general task is to study the solution spaces of combinatorial problems and to decide ...

In this study, we investigate the computational complexity of some variants of generalized puzzles. We are provided with two sets ${\mathcal{S}}_1$ and ${\mathcal{S}}_2$ of polyominoes. The first puzzle asks us to form the same shape using polyominoes in ${\mathcal{S}}_1$ and ${\mathcal{S}}_2$. We ...${\mathcal{}}_{\mathrm{}}$${\mathcal{}}_{\mathrm{}}$${\mathcal{}}_{\mathrm{}}$${\mathcal{}}_{\mathrm{}}$${\mathcal{}}_{\mathrm{}}$

We develop an approach called bounded combinatorial reconfiguration for solving combinatorial reconfiguration problems based on Answer Set Programming. The general task is to study the solution spaces of source combinatorial problems and to decide ...

The Hamiltonian cycle reconfiguration problem is defined as determining, for a given Hamiltonian cycle problem and two among its feasible solutions, whether one is reachable from another via a sequence of feasible solutions subject to certain ...

In this paper, we present a SAT-based Attractor Finder (SAF) which computes attractors in biological regulatory networks modelled as asynchronous automata networks. SAF is based on translating the problem of finding attractors of a bounded size ...

We develop an approach to solving mono- and multi-objective vehicle equipment specification problems considering the corporate average fuel economy standard (CAFE problems, in short) in automobile industry. Our approach relies upon Answer Set ...

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 ...

The Hamiltonian cycle problem (HCP) is the problem of finding a spanning cycle in a given graph. HCP is NP-complete and has been known as an important problem due to its close relationship to the travelling salesman problem (TSP), which can be seen as ...

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 ...

In this paper, we present the Scarab system which is a prototyping tool for developing SAT-based systems. It provides a rich constraint modeling language on Scala and enables a programmer to rapidly specify problems and to experiment with different ...

This paper describes a SAT-based CSP solver Azucar. Azucar solves a finite CSP by encoding it into a SAT instance using the compact order encoding and then solving the encoded SAT instance with an external SAT solver. In the compact order encoding, each ...

Generating test cases for combinatorial testing is to find a covering array in Combinatorial Designs. In this paper, we consider the problem of finding optimal covering arrays by SAT encoding. We present two encodings suitable for modern CDCL SAT ...

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 ...

A Boolean Satisfiability Testing Problem (SAT) is a combinatorial problem to find a Boolean variable assignment which satisfies all given Boolean formulas. Recent performance improvement of SAT technologies makes SAT-based approaches applicable for ...

In this paper, we propose a new method to encode Constraint Satisfaction Problems (CSP) and Constraint Optimization Problems (COP) with integer linear constraints into Boolean Satisfiability Testing Problems (SAT). The encoding method (named order ...

Propositional satisfiability (SAT) has attracted considerable attention recently in both Computer Science and Artificial Intelligence, and a lot of algorithms have been developed for solving SAT. Each SAT solver has strength and weakness, and it is ...

In this paper, we propose a method to encode Constraint Satisfaction Problems (CSP) and Constraint Optimization Problems (COP) with integer linear constraints into Boolean Satisfiability Testing Problems (SAT) . The encoding method is basically the same ...

We present the Prolog Cafe system that translates Prolog into Java via the WAM . Prolog Cafe provides multi-threaded Prolog engines. A Prolog Cafe thread seems to be conceptually an independent Prolog evaluator and communicates with each other through ...