4.1 Constraints in BSEC Problem
Figure 4.1 is an example to illustrate how the conflict constraints work on the SAT solving process, Before the example, let’s recall the basic idea in SAT solving. The DPLL-based algorithm, introduced in section 2.2, is the core of most start-of-art SAT engines.
The procedure of DPLL-based algorithm is illustrated as follows:
1. Trace from the clause with minimum number of literals, especially in unit clause Assign value to variable v, and push v into assignment queue
2. Use v to apply implication on other clauses
If variable u could be implied by v, then push u into assignment queue
3. While size of assignment queue is equal to the number of variables, return SAT if implication v0 6= v in assignment queue, return UNSAT
In DPLL-based algorithm, the assignment queue is used to record the assigned vari-ables. Since all clauses in a SAT problem must be satisfable and the problem can be satis-fiable. DPLL-based algorithm starts from the clause with minimum number of literals. If one variable v could be assigned the specific value, the variable could be pushed into the as-signment and propagated to other clauses. The procedure would continue to assigned other variables. If all variables have been assigned, the problem is satisfiable. If one implied variable conflicts the results in assignment queue, the problem is unsatisfiable.
V1 Figure 4.1: An example to illusrtate constraint in SAT solving
Figure 4.1(a) is the sample example and Figure 4.1(b) is the truth table of V5and V6 in sample circuit. From the truth table, it implies that the logic value of V7is stuck at 0. If the circuit is modeled as a SAT problem and target V7 = 1, the SAT engine is expected to return an unsatisfiable answer. Table 4.1 lists the clauses of the sample circuit in Figure 4.1(a).
Table 4.1: Clauses for Figure 4.1 1 ¬V5+ V1 8 V4+ V2 2 ¬V5+ V4 9 ¬V3+ ¬V1
3 V5+ ¬V1+ ¬V4 10 V3+ V1 4 ¬V6+ V2 11 ¬V7+ V5
5 ¬V6+ V3 12 ¬V7+ V6 6 V6+ V2+ V3 13 V7+ ¬V5+ ¬V6
7 ¬V4+ ¬V2 14 V7
The procedure is used to solve the SAT problem, as follows:
• step1: start from unit clause 14, imply V7 = 1, push V7into assignment queue
• step2: process V7, imply V5 = 1 in clause 11 and imply V6 = 1 in clause 12, push V5 and V6into assignment queue
• step3: process V5, imply V1 = 1 in clause 1 and imply V4 = 1 in clause 2, push V1 and V4into assignment queue
• step4: process V6, imply V2 = 1 in clause 4 and imply V3 = 1 in clause 5, push V2 and V3into assignment queue
• step5: process V1, imply V3 = 0 ←→ conflict with V3 = 1, return UNSAT.
In the procedure, it requires five steps to prove the SAT problem in Table 4.1 is unsat-isfiable. Although the five steps seems not heavy, it would be difficult as solving larger circuits. Conflict constraints are one way to speedup the proof. From the truth table in
Figure 4.1, it is clearly to observe that the V5 = 1 and V6 = 1 can not happen at the same time. we call that (V5, V6) is a conflict constraint in the sample circuit and add the conflict constraint as a conflict clause after original SAT problem. Since (V5, V6) means V5 = 1 and V6 = 1 can not happen at the same time, it indicates V5 = 0 and V6 = 0 may occur in the circuit. As a result, the clause of (V5, V6) can be written as ¬V5+ ¬V6 and added as 15th clause after original SAT problem. The solving procedure of new SAT problem is as follows,
• step1: start from unit clause 14, imply V7 = 1, push V7into assignment queue
• step2: process V7, imply V5 = 1 in clause 11 and imply V6 = 1 in clause 12, push V5 and V6into assignment queue
• step3: process V5, imply V1 = 1 in clause 1 and imply V4 = 1 in clause 2, imply V6 = 0 in clause 15 ←→ conflict with V6 = 1, return UNSAT.
Compare with solving the original SAT problem, the SAT problem with a conflict straint only requires 3 steps of proof. The example illustrates the power of conflict con-straints. Since the BSEC problem is a combinational SAT problem and the solving process is similar to the BCP procedure, and the conflict constraints will also help SAT solving.
One way to find out conflict constraints in BSEC is to list the truth table for all internal signals and discover the unhappen situation in the truth table. However, it is impossible to enumerate all input combination to construct such truth table as in Figure 4.1(b). The alternative method is to construct the relaxed Boolean function of each signal, as mention in section 3.2. Since the number of combination of internal signals is quite large, in this work, we only extract the information on flip-flops. The detail explanation is introduced in section 2.1.
The previous work in [20] is the first study of applying a support-confidence algorithm named Apriori to explore the implication constraints among 3 internal nodes (a·b→c) for SAT solving. However, in this work, we do not mine constraints directly from data. Instead, we propose a new learning algorithm which modifies the notion of support-confidence with impurity measures [28] to infer the relaxed Boolean functions for each FF state at different timeframes. Later, conflict constraints will be derived by composing two relaxed Boolean
functions.
DEFINITION (Conflict Constraint)
A state-pair (pi,qj), where i, j denote the timeframes and j > i > 0, in a finite state ma-chine M is a conflict constraint if and only if ∀k > i, qk+j−i can never appear after pk appears in M for all input sequences.
Such constraints can be used to early stop the random walk during the SAT solving process, and their effectiveness will be demonstrated through our experiments later. The proposed method to exploit conflict constraint is introduced in the following section.