Paper1: SAT-based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, Naoyuki Tamura présenté à SAT’25 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.24

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.

Paper2: A SAT-based Method for Counting All Singleton Attractors in Boolean Networks Rei Higuchi, Takehide Soh, Daniel Le Berre, Morgan Magnin, Mutsunori Banbara and Naoyuki Tamura présenté à IJCAI’25

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- 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 singleton attractors of large-scale benchmarks well established in the literature.