SOH, Takehide
宋 剛秀

ソフトウェア

• sCOP: SAT-based Constraint Programming System
  
  • http://tsoh.org/sCOP/

  • Publication (Solver Description)

    sCOP: SAT-based Constraint Programming System. Takehide Soh,
    Daniel Le Berre, Mutsunori Banbara, Naoyuki Tamura. Solver
    Descriptions of XCSP3 Competition 2018 (XCSP18), 2 pages, 2018. http://www.cril.univ-artois.fr/XCSP18/files/scop.pdf
    

• Scarab: SATソルバーを用いた制約プログラミングシステム
  
  • Scala 言語上に実装した制約プログラミングシステムです．
  • 制約記述用のドメイン特化言語を備えており，簡潔に問題を記述するこ とができ，記述した問題をSATソルバーを使って解くことができます．
  • コンパクトに実装（Scalaで1000行ほど）されており，プログラム自体の 変更も容易です．
  • http://tsoh.org/scarab/

  • 論文 (DOI, ACM DL)

    Scarab: A Rapid Prototyping Tool for SAT-based Constraint Programming Systems
    Takehide Soh, Naoyuki Tamura, and Mutsunori Banbara
    In the Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), LNCS 7962, pp. 429-436, 2013.
    

• Diet-Sugar: SATソルバーを用いたCSPソルバー
  
  • 順序符号化と対数符号化を融合したハイブリッド符号化を実現した制約 充足問題 (CSP) ソルバーです．
  • 両方の符号化を自動的に切り替え，高速にCSPを解くことが出来ます．
  • http://tsoh.org/dsugar/

  • 論文 (DOI)

    A Hybrid Encoding of CSP to SAT Integrating Order and Log Encodings
    Takehide Soh, Mutsunori Banbara, Naoyuki Tamura
    Proceedings of the 27th IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2015), to appear, IEEE Computer Society, 2015.
    

• hss: SATソルバーを用いたハミルトン閉路問題ソルバー
  
  • ハミルトン閉路問題 (HCP) を Counterexample Guided Abstraction Refinement CEGAR を使って解くHCPソルバーです．
  • http://tsoh.org/hss/

  • 論文 (DOI, ACM DL)

    Incremental SAT-based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem.
    Takehide Soh, Daniel Le Berre, Stéphanie Roussel, Mutsunori Banbara and Naoyuki Tamura.
    In: Eduardo Fermé and Joäo Leite (eds.), Proceedings of the 14th European Conference on Logics in Artificial Intelligence (JELIA 2014), 
    Lecture Notes in Artificial Intelligence, Vol.8761, pp.684-693, Springer, 2014.