arXiv subjects

Takahisa Toda

Publications and source records attributed to Takahisa Toda.

7 recordsLinked to original sources

arXiv2025

Quantitative Verification of Fairness in Tree Ensembles

This work focuses on quantitative verification of fairness in tree ensembles. Unlike traditional verification approaches that merely return a single counterexample when the fairness is violated, quantitative verification estimates the ratio of all counterexamples and characterizes the regions where they occur, which is important information for diagnosing and mitigating bias. To date, quantitative verification has been explored almost exclusively for deep neural networks (DNNs). Representative methods, such as DeepGemini and FairQuant, all build on the core idea of Counterexample-Guided Abstraction Refinement, a generic framework that could be adapted to other model classes. We extended the framework into a model-agnostic form, but discovered two limitations: (i) it can provide only lower bounds, and (ii) its performance scales poorly. Exploiting the discrete structure of tree ensembles, our work proposes an efficient quantification technique that delivers any-time upper and lower bounds. Experiments on five widely used datasets demonstrate its effectiveness and efficiency. When applied to fairness testing, our quantification method significantly outperforms state-of-the-art testing techniques.

cs.LG↗

arXiv2022

ZDD-Based Algorithmic Framework for Solving Shortest Reconfiguration Problems

This paper proposes an algorithmic framework for various reconfiguration problems using zero-suppressed binary decision diagrams (ZDDs), a data structure for families of sets. In general, a reconfiguration problem checks if there is a step-by-step transformation between two given feasible solutions (e.g., independent sets of an input graph) of a fixed search problem such that all intermediate results are also feasible and each step obeys a fixed reconfiguration rule (e.g., adding/removing a single vertex to/from an independent set). The solution space formed by all feasible solutions can be exponential in the input size, and indeed many reconfiguration problems are known to be PSPACE-complete. This paper shows that an algorithm in the proposed framework efficiently conducts the breadth-first search by compressing the solution space using ZDDs, and finds a shortest transformation between two given feasible solutions if exists. Moreover, the proposed framework provides rich information on the solution space, such as the connectivity of the solution space and all feasible solutions reachable from a specified one. We demonstrate that the proposed framework can be applied to various reconfiguration problems, and experimentally evaluate their performances.

cs.DS↗

arXiv2020

Exact Method for Generating Strategy-Solvable Sudoku Clues

A Sudoku puzzle often has a regular pattern in the arrangement of initial digits and it is typically made solvable with known solving techniques, called strategies. In this paper, we consider the problem of generating such Sudoku instances. We introduce a rigorous framework to discuss solvability for Sudoku instances with respect to strategies. This allows us to handle not only known strategies but also general strategies under a few reasonable assumptions. We propose an exact method for determining Sudoku clues for a given set of clue positions that is solvable with a given set of strategies. This is the first exact method except for a trivial brute-force search. Besides the clue generation, we present an application of our method to the problem of determining the minimum number of strategy-solvable Sudoku clues. We conduct experiments to evaluate our method, varying the position and the number of clues at random. Our method terminates within $1$ minutes for many grids. However, as the number of clues gets closer to $20$, the running time rapidly increases and exceeds the time limit set to $600$ seconds. We also evaluate our method for several instances with $17$ clue positions taken from known minimum Sudokus to see the efficiency for deciding unsolvability.

cs.DS↗

arXiv2015

Implementing Efficient All Solutions SAT Solvers

All solutions SAT (AllSAT for short) is a variant of propositional satisfiability problem. Despite its significance, AllSAT has been relatively unexplored compared to other variants. We thus survey and discuss major techniques of AllSAT solvers. We faithfully implement them and conduct comprehensive experiments using a large number of instances and various types of solvers including one of the few public softwares. The experiments reveal solver's characteristics. Our implemented solvers are made publicly available so that other researchers can easily develop their solver by modifying our codes and compare it with existing methods.

cs.DS↗

arXiv2011

On Separating Families of Bipartitions

In this paper, we focus on families of bipartitions, i.e. set partitions consisting of at most two components. We say that a family of bipartitions is a separating family for a set $S$ if every two elements in $S$ can be separated by some bipartition. Furthermore, we call a separating family minimal if no proper subfamily is a separating family. We characterize the set of all minimal separating families of maximum size for arbitrary set $S$ as the set of all spanning trees on $S$ and enumerate minimal separating families of maximum size. Furthermore, we enumerate separating families of arbitrary size, which need not be minimal.

math.CO↗

arXiv2010

On Partitioning Colored Points

P. Kirchberger proved that, for a finite subset $X$ of $\mathbb{R}^{d}$ such that each point in $X$ is painted with one of two colors, if every $d+2$ or fewer points in $X$ can be separated along the colors, then all the points in $X$ can be separated along the colors. In this paper, we show a more colorful theorem.

math.CO↗

arXiv2010

Multi-convex sets in real projective spaces and their duality

We study intersections of projective convex sets in the sense of Steinitz. In a projective space, an intersection of a nonempty family of convex sets splits into multiple connected components each of which is a convex set. Hence, such an intersection is called a multi-convex set. We derive a duality for saturated multi-convex sets: there exists an order anti-isomorphism between nonempty saturated multi-convex sets in a real projective space and those in the dual projective space. In discrete geometry and computational geometry, these results allow to transform a given problem into a dual problem which sometimes is easier to solve. This will be pursued in a later paper.

math.MG↗