首页 > 其他分享 >有关子句化简(Clause simplification)的文献

有关子句化简(Clause simplification)的文献

时间：2024-01-20 18:55:19浏览次数：32  
标签：化简 doi conf dblp Clause https 子句 org

一、 2021、2022年之前化简文献

2021-2022李初明老师团队的文章《Branching Strategy Selection Approach Based on Vivification Ratio》提到了关于化简的相关文献。

 

子句简化的方法可分为预处理和中处理两种。

最有效的预处理技术包括Bounded的变体变量消除，冗余从句的添加或消除，检测附属条款，以及它们的适当组合[EB05, BW03]。

The methods of clause simplification can be categorized into pre-processing and
in-processing. The most effective pre-processing techniques include variants of Bounded
Variable Elimination, Addition or Elimination of Redundant Clauses, Detection of
Subsumed Clauses, and suitable combinations of them [EB05, BW03]. They aim
mostly at reducing the number of clauses, literals, and variables in the input for-
mula. The most effective in-processing techniques [JHB12] are Local and Recursive
Clause Minimization[BKS04, SB09], On-the-fly Clause Subsumption [HS09, HJS10],
and clause vivification [LLX+17, LXL+20] where Local and Recursive Clause Mini-
mization removes redundant literals from learnt clauses immediately after their cre-
ation, On-the-fly Clause Subsumption efficiently removes clauses subsumed by the
resolvents derived during clause learning, and clause vivification periodically detects
and removes redundant literals from clauses by unit propagation.
   
 

相关文献：

1.

@article{DBLP:journals/corr/abs-2112-06917,
  author       = {Mao Luo and
                  Chu{-}Min Li and
                  Xinyun Wu and
                  Shuolin Li and
                  Zhipeng L{\"{u}}},
  title        = {Branching Strategy Selection Approach Based on Vivification Ratio},
  journal      = {CoRR},
  volume       = {abs/2112.06917},
  year         = {2021},
  url          = {https://arxiv.org/abs/2112.06917},
  eprinttype    = {arXiv},
  eprint       = {2112.06917},
  timestamp    = {Mon, 03 Jan 2022 15:45:35 +0100},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2112-06917.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

 

@article{DBLP:journals/ijsi/LuoLWLL22,
  author       = {Mao Luo and
                  Chumin Li and
                  Xinyun Wu and
                  Shuolin Li and
                  Zhipeng Lv},
  title        = {Branching Strategy Selection Approach Based on Vivification Ratio},
  journal      = {Int. J. Softw. Informatics},
  volume       = {12},
  number       = {1},
  pages        = {131--151},
  year         = {2022},
  url          = {https://doi.org/10.21655/ijsi.1673-7288.00278},
  doi          = {10.21655/IJSI.1673-7288.00278},
  timestamp    = {Sat, 14 Jan 2023 22:47:05 +0100},
  biburl       = {https://dblp.org/rec/journals/ijsi/LuoLWLL22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
 

 2.  [EB05, BW03].

 

@inproceedings{DBLP:conf/sat/EenB05,
  author       = {Niklas E{\'{e}}n and
                  Armin Biere},
  editor       = {Fahiem Bacchus and
                  Toby Walsh},
  title        = {Effective Preprocessing in {SAT} Through Variable and Clause Elimination},
  booktitle    = {Theory and Applications of Satisfiability Testing, 8th International
                  Conference, {SAT} 2005, St. Andrews, UK, June 19-23, 2005, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {3569},
  pages        = {61--75},
  publisher    = {Springer},
  year         = {2005},
  url          = {https://doi.org/10.1007/11499107\_5},
  doi          = {10.1007/11499107\_5},
  timestamp    = {Tue, 14 May 2019 10:00:41 +0200},
  biburl       = {https://dblp.org/rec/conf/sat/EenB05.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/sat/BacchusW03,
  author       = {Fahiem Bacchus and
                  Jonathan Winter},
  editor       = {Enrico Giunchiglia and
                  Armando Tacchella},
  title        = {Effective Preprocessing with Hyper-Resolution and Equality Reduction},
  booktitle    = {Theory and Applications of Satisfiability Testing, 6th International
                  Conference, {SAT} 2003. Santa Margherita Ligure, Italy, May 5-8, 2003
                  Selected Revised Papers},
  series       = {Lecture Notes in Computer Science},
  volume       = {2919},
  pages        = {341--355},
  publisher    = {Springer},
  year         = {2003},
  url          = {https://doi.org/10.1007/978-3-540-24605-3\_26},
  doi          = {10.1007/978-3-540-24605-3\_26},
  timestamp    = {Tue, 14 May 2019 10:00:41 +0200},
  biburl       = {https://dblp.org/rec/conf/sat/BacchusW03.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
 

 3. [JHB12]

@inproceedings{DBLP:conf/cade/JarvisaloHB12,
  author       = {Matti J{\"{a}}rvisalo and
                  Marijn Heule and
                  Armin Biere},
  editor       = {Bernhard Gramlich and
                  Dale Miller and
                  Uli Sattler},
  title        = {Inprocessing Rules},
  booktitle    = {Automated Reasoning - 6th International Joint Conference, {IJCAR}
                  2012, Manchester, UK, June 26-29, 2012. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {7364},
  pages        = {355--370},
  publisher    = {Springer},
  year         = {2012},
  url          = {https://doi.org/10.1007/978-3-642-31365-3\_28},
  doi          = {10.1007/978-3-642-31365-3\_28},
  timestamp    = {Mon, 16 Sep 2019 15:30:12 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/JarvisaloHB12.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
 

 4. [HS09, HJS10]

@inproceedings{DBLP:conf/sat/HanS09,
  author       = {HyoJung Han and
                  Fabio Somenzi},
  editor       = {Oliver Kullmann},
  title        = {On-the-Fly Clause Improvement},
  booktitle    = {Theory and Applications of Satisfiability Testing - {SAT} 2009, 12th
                  International Conference, {SAT} 2009, Swansea, UK, June 30 - July
                  3, 2009. Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {5584},
  pages        = {209--222},
  publisher    = {Springer},
  year         = {2009},
  url          = {https://doi.org/10.1007/978-3-642-02777-2\_21},
  doi          = {10.1007/978-3-642-02777-2\_21},
  timestamp    = {Tue, 14 May 2019 10:00:41 +0200},
  biburl       = {https://dblp.org/rec/conf/sat/HanS09.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{DBLP:journals/ijait/HamadiJS10,
  author       = {Youssef Hamadi and
                  Sa{\"{\i}}d Jabbour and
                  Lakhdar Sais},
  title        = {Learning for Dynamic Subsumption},
  journal      = {Int. J. Artif. Intell. Tools},
  volume       = {19},
  number       = {4},
  pages        = {511--529},
  year         = {2010},
  url          = {https://doi.org/10.1142/S0218213010000303},
  doi          = {10.1142/S0218213010000303},
  timestamp    = {Tue, 12 May 2020 16:53:37 +0200},
  biburl       = {https://dblp.org/rec/journals/ijait/HamadiJS10.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
 

 5. [LLX+17, LXL+20] 

@inproceedings{DBLP:conf/ijcai/LuoLXML17,
  author       = {Mao Luo and
                  Chu{-}Min Li and
                  Fan Xiao and
                  Felip Many{\`{a}} and
                  Zhipeng L{\"{u}}},
  editor       = {Carles Sierra},
  title        = {An Effective Learnt Clause Minimization Approach for {CDCL} {SAT}
                  Solvers},
  booktitle    = {Proceedings of the Twenty-Sixth International Joint Conference on
                  Artificial Intelligence, {IJCAI} 2017, Melbourne, Australia, August
                  19-25, 2017},
  pages        = {703--711},
  publisher    = {ijcai.org},
  year         = {2017},
  url          = {https://doi.org/10.24963/ijcai.2017/98},
  doi          = {10.24963/IJCAI.2017/98},
  timestamp    = {Tue, 20 Aug 2019 16:16:54 +0200},
  biburl       = {https://dblp.org/rec/conf/ijcai/LuoLXML17.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
@article{DBLP:journals/ai/LiXLMLL20,
  author       = {Chu{-}Min Li and
                  Fan Xiao and
                  Mao Luo and
                  Felip Many{\`{a}} and
                  Zhipeng L{\"{u}} and
                  Yu Li},
  title        = {Clause vivification by unit propagation in {CDCL} {SAT} solvers},
  journal      = {Artif. Intell.},
  volume       = {279},
  year         = {2020},
  url          = {https://doi.org/10.1016/j.artint.2019.103197},
  doi          = {10.1016/J.ARTINT.2019.103197},
  timestamp    = {Mon, 26 Oct 2020 09:02:06 +0100},
  biburl       = {https://dblp.org/rec/journals/ai/LiXLMLL20.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
   
   

 

二、 后续找到的其他关于子句化简的文献

（待续）

 

标签：化简,doi,conf,dblp,Clause,https,子句,org
From： https://www.cnblogs.com/yuweng1689/p/17976984

相关文章

  • 无涯教程-SQL - INTERSECT Clause函数
    SQLINTERSECT子句用于组合两个SELECT语句，但仅返回第一个SELECT语句中与第二个SELECT语句中的行相同的行。这意味着INTERSECT仅返回两个SELECT语句返回的公共行，MySQL不支持INTERSECT运算符。INTERSECT-语法INTERSECT的基本语法如下。SELECTcolumn1[,column2]FROMt......
  • 无涯教程-SQL - EXCEPT Clause函数
    SQLEXCEPT子句用于组合两个SELECT语句，并从第一个SELECT语句返回第二个SELECT语句未返回的行，这意味着EXCEPT仅返回第二行SELECT语句中不可用的行，MySQL不支持EXCEPT运算符。EXCEPT-语法EXCEPT的基本语法如下。SELECTcolumn1[,column2]FROMtable1[,table2][WHE......
  • Leetcode LCP 02. 分式化简
    https://leetcode.cn/problems/deep-dark-fraction/description/有一个同学在学习分式。他需要将一个连分数化成最简分数，你能帮助他吗？连分数是形如上图的分式。在本题中，所有系数都是大于等于0的整数。输入的cont代表连分数的系数（cont[0]代表上图的a0，以此类推）。返回一个长度......
  • Mysql: [HY000][1093] You can't specify target table 'dupes' for update in FROM c
    错误原因在同一语句中。不能先SELECT出同一表的某些值，在Update这个表实例错误实例DELETEFROMdupesWHEREidNOTIN(SELECTMIN(id)FROMdupesGROUPBYname)正确实例DELETEFROMdupesWHEREidNOTIN(SELECT*FROM(SELECTM......
  • SQL HAVING 子句详解：在 GROUP BY 中更灵活的条件筛选
    SQLHAVING子句HAVING子句被添加到SQL中，因为WHERE关键字不能与聚合函数一起使用。HAVING语法SELECTcolumn_name(s)FROMtable_nameWHEREconditionGROUPBYcolumn_name(s)HAVINGconditionORDERBYcolumn_name(s);演示数据库以下是Northwind示例数据库中“Customers......
  • SQL HAVING 子句详解：在 GROUP BY 中更灵活的条件筛选
    SQLHAVING子句HAVING子句被添加到SQL中，因为WHERE关键字不能与聚合函数一起使用。HAVING语法SELECTcolumn_name(s)FROMtable_nameWHEREconditionGROUPBYcolumn_name(s)HAVINGconditionORDERBYcolumn_name(s);演示数据库以下是Northwind示例数据库中“Customers......
  • Mysql - Error 1055: Expression #1 of SELECT list is not in GROUP BY clause and c
    执行SQL时出现错误ERROR1055，SELECT列表不在GROUPBY语句内且存在不函数依赖GROUPBY语句的非聚合字段'edusassvc.u.nickname'这是和sql_mode=only_full_group_by不兼容的（即不支持）。分析问题1)原理层面这个错误会发生在mysql5.7版本及以上版本mysql5.7版本以上默认的sql......
  • mysql 报错which is not functionally dependent on columns in GROUP BY clause; thi
    Expression#2ofSELECTlistisnotinGROUPBYclauseandcontainsnonaggregatedcolumn'd.Id'whichisnotfunctionallydependentoncolumnsinGROUPBYclause;thisisincompatiblewithsql_mode=only_full_group_bywindow系统中，服务中找到mysql服务"......
  • 无涯教程-MySQL IN Clause函数
    您可以使用IN子句替换许多OR条件要了解IN子句,请考虑一个employee_tbl表,该表具有以下记录-mysql>SELECT*FROMemployee_tbl;+------+------+------------+--------------------+|id|name|work_date|daily_typing_pages|+------+------+------------......
  • 无涯教程-MySQL Group By Clause函数
    您可以使用GROUPBY对一列中的值进行分组,并且,如果需要,可以对该列进行计算。您可以在分组列上使用COUNT,SUM,AVG等功能。要了解GROUPBY子句,请考虑一个employee_tbl表,该表具有以下记录-mysql>SELECT*FROMemployee_tbl;+------+------+------------+-----------......

赞助商

阅读排行

网站主页关于我们联系我们网站地图

本网站内容转载自其他媒体，侵权联系[admin##ips99.com]。

Copyright © 2020-2023 IPS99 版权所有 IPS99