Since 2004 Prof. Armin Biere is a Full Professor for Computer Science at the Johannes Kepler University in Linz, Austria, and chairs the Institute for Formal Models and Verification.

译文：Armin Biere教授自2004年起担任奥地利林茨约翰内斯开普勒大学计算机科学的全职教授，并担任形式模型与验证研究所的主席。

Between 2000 and 2004 he held a position as Assistant Professor within the Department of Computer Science at ETH Zürich, Switzerland. In 1999 Biere was working for a start-up company in electronic design automation after one year as Post-Doc with Edmund Clarke at CMU, Pittsburgh, USA. In 1997 Biere received a Ph.D. in Computer Science from the University of Karlsruhe, Germany.

译文：2000年至2004年，他在瑞士苏黎世联邦理工学院计算机科学系担任助理教授。1999年，Biere在美国匹兹堡CMU的Edmund Clarke做了一年博士后之后，在一家新兴的电子设计自动化公司工作。1997年，比尔获得了德国卡尔斯鲁厄大学的计算机科学博士学位。

His primary research interests are applied formal methods, more specifically formal verification of hardware and software, using model checking, propositional and related techniques.

译文：他的主要研究兴趣是应用形式化方法，更具体的是硬件和软件的形式化验证，使用模型检查、命题和相关技术。

He is the author and co-author of more than 120 papers and served on the program committee of more than 110 international conferences and workshops.译文：他是120多篇论文的作者和合著者，并在110多个国际会议和研讨会的项目委员会任职。

His most influential work is his contribution to Bounded Model Checking. Decision procedures for SAT, QBF and SMT, developed by him or under his guidance rank at the top many international competitions and were awarded 57 medals including 32 gold medals.

译文：他最具影响力的工作是他对有限模型检验的贡献。他所开发或指导的SAT、QBF和SMT决策程序，在许多国际比赛中名列前茅，获奖牌57枚，其中金牌32枚。

(Exponential) Variable State Independent Decaying Sum (VSIDS)

empirically one of the most important features of state-of-the-art solvers

no formal argument “why it works”译文：没有正式的论证"为什么它有效"

“Trying to Understand the Power of VSIDS”

reconsider simpler alternatives ------particularly variable move to front schemes (VMTF)

shows that VMTF is as good as VSIDS (and explains boths)

decision heuristics consist of

• • variable selection: which variable to assign next?
  • phase selection: assign variable to which phase (true or false)?

phase saving [PipatsrisawatDarwiche’07]

• • select phase to which variable was assigned before
  • initialized by static one-side heuristics [JeroslowWang’90]
  • very effective and thus default in state-of-the-art solvers

we consider only variable selection as decision heuristic here

• • clause based heuristics less effective (BerkMin, CMTF)                     译文：基于子句的启发式效果较差
  • same applies to literal based heuristics (using literal scores)

variable selection and decision heuristic boils down to

• • compute and maintain heuristic scores for variables
  • select variable with highest score

how to compute scores

• • static or dynamic
  • bump variables: when to increase scores and by how much
  • rescore variables: when to decrease scores and by how much
  • state-of-the-art: VSIDS (from Chaff)

               more precisely the exponential variant (EVSIDS) of MiniSAT!

data structures for finding decision variables

• • eager or lazy update of “order”
  • state-of-the-art: priority queue of variables ordered by score (MiniSAT)

zero order scheme = static scores

• • computed for instance once during preprocessing
  • still needs search for “best” unassinged variable
  • only total orders considered so far

first order schemes = dynamic but state less

• • for instance: score = pos occs × neg occs
  • independent of how search reached current branch / search node
  • might be quite expensive to compute / update (linear in CNF size)

second order schemes: variable score depends on history of search

• • first order + learning ⇒ second order
  • but can also be used to speed up search for “best” variable
  • goal is logarithmic or even constant algorithm for variable selection

Siege SAT solver [Ryan’04] used variable move to front (VMTF)

• • bumped variables moved to head of doubly linked list
  • search for unassigned variable starts at head
  • variable selection is an online sorting algorithm of scores
  • classic “move-to-front” strategy achieves good amortized complexity

original implementation severely restricted

• • only moved a subset of bumped variables
  • details about caching the search not described no source code published either
  • not exactly the same as VSIDS

as consequence VMTF not used in state-of-the-art solvers

译文：因此，VMTF不用于最先进的解决方案

floating point scores

• • allows fine grained rescore at every conflict
  • consider multiplying by f = 0.9 every score at each conflict

actually, instead of updating scores of all variables (at every conflict)

• • only increase score of bumped variables by g ⁱ
  • with i the conflict-index, and g = 1/ f
  • non-bumped variables not touched

priority queue of variables ordered by score

• • implemented as binary heap with update (bump and bubble up)
  • lazy assigned variable removal
    • remove largest score variable from heap until unassigned one found
    • put unassigned variables not on the heap back (logarithmic complexity)

normalized VSIDS (NVSIDS) ∈ [0,1] as (theoretical) model [Biere’08] + video

Summary Variable Scoring Schemes

fast simple implementation for caching searches（缓存搜索） in VMTF [Biere’15]

• • doubly linked list does not have positions as an ordered array
  • bump = move-to-front = dequeue then insertion at the head

time-stamp list entries with insertion time 译文：带有插入时间的时间戳列表条目

• • maintained invariant: all variables right of next-search are assigned
  • requires update to next-search while unassigning variables 译文：在不分配变量时，需要对next搜索进行更新

solved SAT competition 2014 application track instances (ordered by time)

solved SAT competition 2014 application track instances (ordered by time)

SAT'16 Competition Application Benchmarks (sorted by percentage run−time)

Conclusion Part I

surveyed and classified variable selection / scoring schemes

译文：调查和分类变量选择/评分方案

• • came up with a new one ACIDS (as well as SUM)
  • EVSIDS, VMTF, ACIDS comparable in performance
  • with a generic fast queue implementation 译文：使用一个通用的快速队列实现

VMTF was considered to be obsolete 译文：VMTF被认为是过时的

• • can be made effective (with less code than EVSIDS)
  • needs proper optimized implementation: time-stamping with insertion-time
  • VMTF might be easier to reason about in proof complexity 译文：在证明复杂性方面，VMTF可能更容易推理

threads to validity 线程的有效性

• • unclear whether VMTF only works in combination with Glucose restarts see also our POS’15 paper and talk in Part II of this talk
  • benchmark selection in recent SAT competitions highly controversial

Splatz: SAT solver only based on VMTF

        http://fmv.jku.at/splatz

Evaluating CDCL Restart Schemes [POS’15 paper with Andreas Frohlich] ¨

• • simplifies Glucose style restart schemes
  • evaluation shows clear benefits but also weaknesses

Lingeling actually barely won

• • only for long time limit of 5000 seconds
  • for 900 seconds: no chance

two main reasons

• • selected benchmark biased towards decendants of Glucose / MiniSAT
  • but Glucose restarts are important for many (selected) benchmarks              译文：但是Glucose的重新启动对许多(选定的)基准是重要的

the POS’15 paper is about lessons learned while

• • porting the Glucose restart scheme to Lingeling
  • and simplifying by using exponential moving averages (EMA)

original longer slide set at http://fmv.jku.at/biere/talks/Biere-POS15-talk.pdf

Miter （斜接）

hyper-binary resolve multiple binary clauses in “parallel”:

thus “in principle” hyper-binary resolution can simulate structural hashing

but we do not know how to implement it fast (without having the circuit and including equivalence literal substitution)

Software Architecture of our Boolector SMT Solver

Solving Miters with CDCL Requires Restarts

译文：用CDCL解决Miters需要重新启动

trivial miters of identical circuits

• • equivalence = bimplication (two implications aka binary clauses)
  • equivalences are reused recursively and thus order of learning important
  • best solved by “finding” and applying equivalences bottom-up

point of Yakau Novikov at our predecessor Dagstuhl meeting in 2015

• • assume first implication a → b is learned
  • w.l.o.g. a assigned before b
  • then a was assigned to 1 and b to 0
  • after learning first implication, b is flipped and both a and b are assigned to 1
  • in order to learn b → a we have to assign b to 1 and a to 0
  • thus without unassigning a we can not learn the second implication

so frequent restarts are useful here

• • triggered by Glucose restart style schedules (as discused in Part II)
  • actually phase saving is also counter productive here (tried to fix it without success)
  • still not perfect, dedicated preprocessing faster

Challenges Part III

how to do equivalence checking on the CNF level

• • (even) more efficient implementation of hyper-binary resolution
  • partial solution [HeuleBiere-LPAR’13]
    • blocked clause decomposition
    • SAT sweeping

another (unpublished) partial solution:

• • simple-probing in Lingeling
  • simulates structural hashing on the CNF level
  • eager equivalent literal substitution
  • fails after preprocessing (bounded variable elimination)

recover / use circuit structure

• • locality
  • direction (inputs)
  • functional dependencies (might get lost during preprocessing)

Arithmetic Reasoning Hard for CDCL 译文：CDCL的算术推理很困难

Commutativity of Bit-Vector Multiplication 译文：位向量乘法的交换性

Arithmetic Circuit Equivalence Checking译文：算术电路等价性检验

Challenge Part IV

Problem

• • Tseitin encoding of the miter of a multiplier with itself but with inputs swapped.译文：乘法器的斜接编码，它本身与输入交换。

Conjecture 猜想

• • Refuting the resulting CNF requires exponential resolution proofs (and thus CDCL too).译文：反驳由此产生的CNF需要指数分辨率的证明(因此CDCL也需要)

Research Question

• • Determine proof systems with polynomial proofs for this problem.译文：为这个问题确定多项式证明的证明系统

decision heuristics

• • new empirical insights: VMTF simpler and as good as VSIDS
  • can we prove why these work?

restarts

• • simplified Glucose restart scheme, showed that it somehow works
  • clearly not where we want it to be (machine learning necessary?)

miters

• • CDCL implementations do not learn the right clauses
  • fast restarts partially fix it, can we prove that?

arithmetic reasoning  计算推理

• • need stronger proof systems? 译文：需要更强大的证明系统吗?
  • can we prove that?