-
Spatial-photonic Ising machine by space-division multiplexing with physically tunable coefficients of a multi-component model
Authors:
Takumi Sakabe,
Suguru Shimomura,
Yusuke Ogura,
Ken-ichi Okubo,
Hiroshi Yamashita,
Hideyuki Suzuki,
Jun Tanida
Abstract:
This paper proposes a space-division multiplexed spatial-photonic Ising machine (SDM-SPIM) that physically calculates the weighted sum of the Ising Hamiltonians for individual components in a multi-component model. Space-division multiplexing enables tuning a set of weight coefficients as an optical parameter and obtaining the desired Ising Hamiltonian at a time. We solved knapsack problems to ver…
▽ More
This paper proposes a space-division multiplexed spatial-photonic Ising machine (SDM-SPIM) that physically calculates the weighted sum of the Ising Hamiltonians for individual components in a multi-component model. Space-division multiplexing enables tuning a set of weight coefficients as an optical parameter and obtaining the desired Ising Hamiltonian at a time. We solved knapsack problems to verify the system's validity, demonstrating that optical parameters impact the search property. We also investigated a new dynamic coefficient search algorithm to enhance search performance. The SDM-SPIM would physically calculate the Hamiltonian and a part of the optimization with an electronics process.
△ Less
Submitted 10 October, 2023;
originally announced October 2023.
-
Nagoya Termination Tool
Authors:
Akihisa Yamada,
Keiichirou Kusakari,
Toshiki Sakabe
Abstract:
This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination prover for term rewrite systems. The main features of the tool are: the first implementation of the weighted path order which subsumes most of the existing reduction pairs, and the efficiency due to the strong cooperation with external SMT solvers. We present some new ideas that contribute to the e…
▽ More
This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination prover for term rewrite systems. The main features of the tool are: the first implementation of the weighted path order which subsumes most of the existing reduction pairs, and the efficiency due to the strong cooperation with external SMT solvers. We present some new ideas that contribute to the efficiency and power of the tool.
△ Less
Submitted 26 April, 2014;
originally announced April 2014.
-
A Unified Ordering for Termination Proving
Authors:
Akihisa Yamada,
Keiichirou Kusakari,
Toshiki Sakabe
Abstract:
We introduce a reduction order called the weighted path order (WPO) that subsumes many existing reduction orders. WPO compares weights of terms as in the Knuth-Bendix order (KBO), while WPO allows weights to be computed by a wide class of interpretations. We investigate summations, polynomials and maximums for such interpretations. We show that KBO is a restricted case of WPO induced by summations…
▽ More
We introduce a reduction order called the weighted path order (WPO) that subsumes many existing reduction orders. WPO compares weights of terms as in the Knuth-Bendix order (KBO), while WPO allows weights to be computed by a wide class of interpretations. We investigate summations, polynomials and maximums for such interpretations. We show that KBO is a restricted case of WPO induced by summations, the polynomial order (POLO) is subsumed by WPO induced by polynomials, and the lexicographic path order (LPO) is a restricted case of WPO induced by maximums. By combining these interpretations, we obtain an instance of WPO that unifies KBO, LPO and POLO. In order to fit WPO in the modern dependency pair framework, we further provide a reduction pair based on WPO and partial statuses. As a reduction pair, WPO also subsumes matrix interpretations. We finally present SMT encodings of our techniques, and demonstrate the significance of our work through experiments.
△ Less
Submitted 24 April, 2014;
originally announced April 2014.
-
Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
Authors:
Naoki Nishida,
Masahiko Sakai,
Toshiki Sakabe
Abstract:
Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound w.r.t. reduction for every CTRS, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unravel…
▽ More
Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound w.r.t. reduction for every CTRS, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for a deterministic CTRS is sound w.r.t. reduction if the corresponding unraveled TRS is left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling. Finally, we show that soundness of Ohlebusch's unraveling is the weakest in soundness of the other unravelings and a transformation, proposed by Serbanuta and Rosu, for (normal) deterministic CTRSs, i.e., soundness of them respectively implies that of Ohlebusch's unraveling.
△ Less
Submitted 9 August, 2012; v1 submitted 25 June, 2012;
originally announced June 2012.
