DROPS

Document

Short Paper

DOI: 10.4230/LIPIcs.CP.2021.5

Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper)

Authors: Shaowei Cai, Chuan Luo, Xindi Zhang, and Jian Zhang

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract

This work is dedicated to improving local search solvers for the Boolean satisfiability (SAT) problem on structured instances. We propose a construct-and-cut (CnC) algorithm based on unit propagation, which is used to produce initial assignments for local search. We integrate our CnC initialization procedure within several state-of-the-art local search SAT solvers, and obtain the improved solvers. Experiments are carried out with a benchmark encoded from a spectrum repacking project as well as benchmarks encoded from two important mathematical problems namely Boolean Pythagorean Triple and Schur Number Five. The experiments show that the CnC initialization improves the local search solvers, leading to better performance than state-of-the-art SAT solvers based on Conflict Driven Clause Learning (CDCL) solvers.

Cite as

Shaowei Cai, Chuan Luo, Xindi Zhang, and Jian Zhang. Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 5:1-5:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{cai_et_al:LIPIcs.CP.2021.5,
  author =	{Cai, Shaowei and Luo, Chuan and Zhang, Xindi and Zhang, Jian},
  title =	{{Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{5:1--5:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.5},
  URN =		{urn:nbn:de:0030-drops-152969},
  doi =		{10.4230/LIPIcs.CP.2021.5},
  annote =	{Keywords: Satisfiability, Local Search, Unit Propagation, Mathematical Problems}
}

Document

DOI: 10.4230/OASIcs.ICCSW.2015.87

Automatic Transformation of Raw Clinical Data Into Clean Data Using Decision Tree Learning Combining with String Similarity Algorithm

Authors: Jian Zhang

Published in: OASIcs, Volume 49, 2015 Imperial College Computing Student Workshop (ICCSW 2015)

Abstract

It is challenging to conduct statistical analyses of complex scientific datasets. It is a timeconsuming process to find the relationships within data for whether a scientist or a statistician. The process involves preprocessing the raw data, the selection of appropriate statistics, performing analysis and providing correct interpretations, among which, the data pre-processing is tedious and a particular time drain. In a large amount of data provided for analysis, there is not a standard for recording the information, and some errors either of spelling, typing or transmission. Thus, there will be many expressions for the same meaning in the data, but it will be impossible for analysis system to automatically deal with these inaccuracies. What is needed is an automatic method for transforming the raw clinical data into data which it is possible to process automatically. In this paper we propose a method combining decision tree learning with the string similarity algorithm, which is fast and accuracy to clinical data cleaning. Experimental results show that it outperforms individual string similarity algorithms and traditional data cleaning process.

Cite as

Jian Zhang. Automatic Transformation of Raw Clinical Data Into Clean Data Using Decision Tree Learning Combining with String Similarity Algorithm. In 2015 Imperial College Computing Student Workshop (ICCSW 2015). Open Access Series in Informatics (OASIcs), Volume 49, pp. 87-94, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{zhang:OASIcs.ICCSW.2015.87,
  author =	{Zhang, Jian},
  title =	{{Automatic Transformation of Raw Clinical Data Into Clean Data Using Decision Tree Learning Combining with String Similarity Algorithm}},
  booktitle =	{2015 Imperial College Computing Student Workshop (ICCSW 2015)},
  pages =	{87--94},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-000-2},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{49},
  editor =	{Schulz, Claudia and Liew, Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICCSW.2015.87},
  URN =		{urn:nbn:de:0030-drops-54850},
  doi =		{10.4230/OASIcs.ICCSW.2015.87},
  annote =	{Keywords: Raw Clinical Data, Decision Tree Learning, String Similarity Algorithm}
}

Search Results

Documents authored by Zhang, Jian

Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper)

Abstract

Cite as

Automatic Transformation of Raw Clinical Data Into Clean Data Using Decision Tree Learning Combining with String Similarity Algorithm

Abstract

Cite as

Thanks for your feedback!

Could not send message