#约束求解#

蔡少伟　264天前　北京

以谱系看待研究方向，可以帮助我们系统地思考研究领域。 比如， 有精确求解器， 就有近似求解器， 有海量并行求解器， 就有轻量并行求解器， 有面向大规模问题的求解器， 就有面向小规模问题的求解器， 有大算力求解器， 就有小算力求解器，。。。 还可以正反看方向，比如， AI模型辅助求解器， 求 ...全文

蔡少伟　334天前　北京

我在2023年约束求解公开课讲 SAT编码和CDCL算法，2个多小时。 SAT问题，即命题逻辑可满足性问题，是数理逻辑的基础问题。 编码部分包括：组合问题的编码和时序问题的编码。 CDCL算法是SAT问题最主要的求解算法，介绍了其原理，关键技术，关键实现。 这个视频当中对CDCL算法的讲解是比较全面的一次。 ...全文

蔡少伟　296天前　

7个半小时以后，要在中国运筹学会的会议介绍约束求解和形式化方法，很认真地思考应该怎么讲。 有点像讲相声的人希望观众听得懂那个梗。。。以小学生交作业的态度认真过了PPT，可以睡觉了。 #约束求解# #形式化方法#

蔡少伟　450天前　北京

我这两年一直在呼吁，求解器性能要突破，不能停留在雕琢串行算法上（虽然核心算法很重要），这样不是说不可能突破，但是期望时间有点远，因为目前核心算法的研究并不是百花齐放，而是集中在个别成熟的方法上进行增量修改，而想提出新的方法又太依赖神奇的想法。如果要在串行算法上做研究，我们需要的是 ...全文

蔡少伟　593天前　北京

『约束求解器是什么？』🔗 约束求解器简介，分类，和应用场景。 转自 晞德求索 #求解器# #约束求解# 专栏 · 约束求解

蔡少伟　609天前　北京

贺飞老师为大家分享了并发程序验证中的约束求解问题。贺老师首先介绍了基于偏序的符号编码，定义并重点介绍了顺序一致性理论以及相应的算法，此外还提到了围绕弱内存模型的相关工作。 编辑校对 | Hana #约束求解#

Teunnnn　59天前　青岛

“以时间为约向无解题求解”

蔡少伟　640天前　北京

感谢图灵教育和人民邮电出版社的新年礼物！2023年，好好写程序，好好读TAOCP！ 当然，也要尽快把Decision Procedures译完。最近两年对教学突然来激情了，讲了很多约束求解的讲座，以及约束求解训练营，约束求解研究生课程。我发现没有合适的中文教材。自己写教材是个太大的任务，当务之急先翻译一本用 ...全文

蔡少伟　608天前　北京

陈振邦 老师为大家分享了面向符号执行的约束求解。 陈老师首先说明了符号执行的背景、发展历程、以及面临的挑战，然后介绍了两个面向符号执行约束求解方向的工作，一是利用约束求解器中的更多信息来改进符号执行，二是将符号执行期间收集或推断的信息传递给约束求解器，最后进行了总结，希望更紧密地协 ...全文

唯爱大脸妹的方老壳　320天前　重庆

求解 如何忘掉心中的那个她 #约束求解#

蔡少伟　719天前　北京

#约束求解# 2022秋《约束求解》研究生课程讲义分享 目前已经分享了 “约束模型”和“SAT求解基础与CDCL算法”两个部分，会陆续更新。🔗 专栏 · 约束求解

蔡少伟　787天前　北京

#约束求解# #求解器# #EDA# 从朋友传来SAT和MaxSAT比赛捷报。 SAT 2022比赛，我们团队获得并行主赛道冠军，遥遥领先其他求解器。我们设计了一种新型轻量级并行方法，突破了原有方法。这个值得截图。 此外， 我们在串行主赛道获得了亚军（和冠军求解个数相同，慢了几秒惜败）。不截图了。 MaxSAT 2 ...全文