Boolean Satis?ability
with Transitivity Constraints
Randal E.Bryant
Miroslav N.V elev
Carnegie Mellon University
June,2000
CMU-CS-00-101
School of Computer Science
Carnegie Mellon University
Pittsburgh,PA15213
Supported,in part,by the Semiconductor Research Corporation under contract00-DC-684
Keywords:Formal veri?cation,Boolean satis?ability,Decision procedures
Abstract
We consider a variant of the Boolean satis?ability problem where a subset of the propositional variables appearing in formula sat encode a symmetric,transitive,binary relation over ele-ments.Each of these relational variables,,for,expresses whether or not the relation holds between elements and.The task is to either?nd a satisfying assignment to sat that also satis?es all transitivity constraints over the relational variables(e.g.,), or to prove that no such assignment exists.Solving this satis?ability problem is the?nal and most dif?cult step in our decision procedure for a logic of equality with uninterpreted functions.This procedure forms the core of our tool for verifying pipelined microprocessors.
To use a conventional Boolean satis?ability checker,we augment the set of clauses expressing sat with clauses expressing the transitivity constraints.We consider methods to reduce the number of such clauses based on the sparse structure of the relational variables.
To use Ordered Binary Decision Diagrams(OBDDs),we show that for some sets,the OBDD representation of the transitivity constraints has exponential size for all possible variable orderings. By considering only those relational variables that occur in the OBDD representation of sat,our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satis?ability problem.
1Introduction
Consider the following variant of the Boolean satis?ability problem.We are given a Boolean
formula sat over a set of variables.A subset symbolically encodes a binary relation
over elements that is re?exive,symmetric,and transitive.Each of these relational variables,
,where,expresses whether or not the relation holds between elements and .Typically,will be“sparse,”containing much fewer than the possible variables. Note that when for some value of and of,this does not imply that the relation does not hold between elements and.It simply indicates that sat does not directly depend on the
relation between elements and.
A transitivity constraint is a formula of the form
(1) where equals when and equals when.Let denote the set of all transitivity constraints that can be formed from the relational variables.Our task is to?nd an assignment that satis?es sat,as well as every constraint in.Goel, et al.[GSZAS98]have shown this problem is NP-hard,even when sat is given as an Ordered Binary Decision Diagram(OBDD)[Bry86].Normally,Boolean satis?ability is trivial given an OBDD representation of a formula.
We are motivated to solve this problem as part of a tool for verifying pipelined microprocessors
[VB99].Our tool abstracts the operation of the datapath as a set of uninterpreted functions and uninterpreted predicates operating on symbolic data.We prove that a pipelined processor has behavior matching that of an unpipelined reference model using the symbolic?ushing technique developed by Burch and Dill[BD94].The major computational task is to decide the validity of a formula ver in a logic of equality with uninterpreted functions[BGV99a,BGV99b].Our decision procedure transforms ver?rst by replacing all function application terms with terms over a set of domain variables.Similarly,all predicate applications are replaced by formulas over a set of newly-generated propositional variables.The result is a formula ver containing equations of the form,where.Each of these equations is then encoded by introducing a relational variable,similar to the method proposed by Goel,et al.[GSZAS98].The result of the translation is a propositional formula ver expressing the veri?cation condition over both the relational variables and the propositional variables appearing in ver.Let sat denote ver,the complement of the formula expressing the translated veri?cation condition.To capture the transitivity of equality,e.g.,that, we have transitivity constraints of the form.Finding a satisfying assignment to sat that also satis?es the transitivity constraints will give us a counterexample to the original veri?cation condition ver.On the other hand,if we can prove that there are no such assignments, then we have proved that ver is universally valid.
We consider three methods to generate a Boolean formula trans that encodes the transitivity
constraints.The direct method enumerates the set of chord-free cycles in the undirected graph having an edge for each relational variable.This method avoids introducing addi-tional relational variables but can lead to a formula of exponential size.The dense method uses
relational variables for all possible values of and such that.We can then
axiomatize transitivity by forming constraints of the form for all distinct values of,,and.This will yield a formula that is cubic in.The sparse method augments with additional relational variables to form a set of variables,such that the resulting graph is chordal [Rose70].We then only require transitivity constraints of the form such that .The sparse method is guaranteed to generate a smaller formula than the
dense method.
To use a conventional Boolean Satis?ability(SA T)procedure to solve our constrained satis?a-bility problem,we run the checker over a set of clauses encoding both sat and trans.The latest
version of the FGRASP SA T checker[M99]was able to complete all of our benchmarks,although the run times increase signi?cantly when transitivity constraints are enforced.
When using Ordered Binary Decision Diagrams to evaluate satis?ability,we could generate
OBDD representations of sat and trans and use the APPLY algorithm to compute an OBDD representation of their conjunction.From this OBDD,?nding satisfying solutions would be trivial. We show that this approach will not be feasible in general,because the OBDD representation of trans can be intractable.That is,for some sets of relational variables,the OBDD representation of the transitivity constraint formula trans will be of exponential size regardless of the variable
ordering.The NP-completeness result of Goel,et al.shows that the OBDD representation of trans may be of exponential size using the ordering previously selected for representing sat as an OBDD.This leaves open the possibility that there could be some other variable ordering that would yield ef?cient OBDD representations of both sat and trans.Our result shows that transitivity constraints can be intrinsically intractable to represent with OBDDs,independent of the structure of sat.
We present experimental results on the complexity of constructing OBDDs for the transitivity constraints that arise in actual microprocessor veri?cation.Our results show that the OBDDs can indeed be quite large.We consider two techniques to avoid constructing the OBDD representation of all transitivity constraints.The?rst of these,proposed by Goel,et al.[GSZAS98],generates implicants(cubes)of sat and rejects those that violate the transitivity constraints.Although this method suf?ces for small benchmarks,we?nd that the number of implicants generated for our larger benchmarks grows unacceptably large.The second method determines which relational variables actually occur in the OBDD representation of sat.We can then apply one of our three techniques for encoding the transitivity constraints in order to generate a Boolean formula for the transitivity constraints over this reduced set of relational variables.The OBDD representation of this formula is generally tractable,even for the larger benchmarks.
2Benchmarks
Our benchmarks[VB99]are based on applying our veri?er to a set of high-level microprocessor designs.Each is based on the DLX RISC processor described by Hennessy and Patterson[HP96]: 1DLX-C:is a single-issue,?ve-stage pipeline capable of fetching up to one new instruction every clock cycle.It implements six instruction types:register-register,register-immediate,
Circuit Domain Propositional Equations 1DLX-C
134237
2558118 2DLX-CA-t
2DLX-CC
2570143 min.
avg.
max.
To create more challenging benchmarks,we generated variants of the circuits that require en-forcing transitivity in the veri?cation.For example,the normal forwarding logic in the Execute stage of1DLX-C must determine whether to forward the result from the Memory stage instruc-tion as either one or both operand(s)for the Execute stage instruction.It does this by comparing the two source registers ESrc1and ESrc2of the instruction in the Execute stage to the destination register MDest of the instruction in the memory stage.In the modi?ed circuit,we changed the by-pass condition ESrc1MDest to be ESrc1MDest ESrc1ESrc2ESrc2MDest. Given transitivity,these two expressions are equivalent.For each pipeline,we introduced four such modi?cations to the forwarding logic,with different combinations of source and destination registers.These modi?ed circuits are named1DLX-C-t,2DLX-CA-t,and2DLX-CC-t.
To study the problem of counterexample generation for buggy circuits,we generated105vari-ants of2DLX-CC,each containing a small modi?cation to the control logic.Of these,5were found to be functionally correct,e.g.,because the modi?cation caused the processor to stall un-necessarily,yielding a total of100benchmark circuits for counterexample generation.
Table1gives some statistics for the benchmarks.The number of domain variables ranges between13and25,while the number of equations ranges between27and143.The veri?cation condition formulas ver also contain between42and77propositional variables expressing the operation of the control logic.These variables plus the relational variables comprise the set of variables in the propositional formula sat.The circuits with modi?cations that require en-forcing transitivity yield formulas containing up to19additional equations.The?nal three lines summarize the complexity of the100buggy variants of2DLX-CC.We apply a number of sim-pli?cations during the generation of formula sat,and hence small changes in the circuit can yield signi?cant variations in the formula complexity.
3Graph Formulation
Our de?nition of(Equation1)places no restrictions on the length or form of the tran-sitivity constraints,and hence there can be an in?nite number.We show that we can construct a graph representation of the relational variables and identify a reduced set of transitivity constraints that,when satis?ed,guarantees that all possible transitivity constraints are satis?ed.By introduc-ing more relational variables,we can alter this graph structure,further reducing the number of transitivity constraints that must be considered.
For variable set,de?ne the undirected graph as containing a vertex for,and an edge for each variable.For an assignment of Boolean values to the relational variables,de?ne the labeled graph to be the graph with each edge labeled as a 1-edge when,and as a0-edge when.
A path is a sequence of vertices having edges between successive elements. That is,each element of the sequence()denotes a vertex:,while each successive pair of elements and()forms an edge We consider each edge for to also be part of the path.A cycle is a path of the form.
Proposition1An assignment to the variables in violates transitivity if and only if some cycle in contains exactly one0-edge.
Proof:If.Suppose there is such a cycle.Letting be the vertex at one end of the0-edge,we can trace around the cycle,giving a sequence of vertices,where is the vertex at the other end of the0-edge.The assignment has for,and, and hence it violates Equation1.
Only If.Suppose the assignment violates a transitivity constraint given by Equation1.Then, we construct a cycle of vertices such that only edge is a0-edge.
A path is said to be acyclic when for all.A cycle
is said to be simple when its pre?x is acyclic.
Proposition2An assignment to the variables in violates transitivity if and only if some simple cycle in contains exactly one0-edge.
Proof:The“if”portion of this proof is covered by Proposition1.The“only if”portion is proved by induction on the number of variables in the antecedent of the transitivity constraint (Equation1.)That is,assume a transitivity constraint containing variables in the antecedent is violated and that all other violated constraints have at least variables in their antecedents.If there are no values and such that and,then the cycle is simple. If such values and exist,then we can form a transitivity constraint:
This transitivity constraint contains fewer than variables in the antecedent,but it is also violated. This contradicts our assumption that there is no violated transitivity constraint with fewer than variables in the antecedent.
De?ne a chord of a simple cycle to be an edge that connects two vertices that are not adjacent in the cycle.More precisely,for a simple cycle,a chord is an edge in such that,with,and either or.A cycle is said to be chord-free if it is simple and has no chords.
Proposition3An assignment to the variables in violates transitivity if and only if some chord-free cycle in contains exactly one0-edge.
Proof:The“if”portion of this proof is covered by Proposition1.The“only if”portion is proved by induction on the number of variables in the antecedent of the transitivity constraint (Equation1.)Assume a transitivity constraint with variables is violated,and that no transitivity constraint with fewer variables in the antecedent is violated.If there are no values of and such that there is a variable with and either or,then the corresponding cycle is chord-free.If such values of and exist,then consider the two cases illustrated in Figure 1,where0-edges are shown as dashed lines,1-edges are shown as solid lines,and the wavy lines
0-Edge1-Edge
Figure1:Case Analysis for Proposition3.0-Edges are shown as dashed lines.When a cycle rep-resenting a transitivity violation contains a chord,we can?nd a smaller cycle that also represents a transitivity violation.
represent sequences of1-edges.Case1:Edge is a0-edge(shown on the left).Then the transitivity constraint:
is violated and has fewer than variables in its antecedent.Case2:Edge is a1-edge(shown on the right).Then the transitivity constraint:
is violated and has fewer than variables.Both cases contradict our assumption that there is no violated transitivity constraint with fewer than variables in the antecedent.
Each length cycle yields constraints,given by the following clauses.Each clause is derived by expressing Equation1as a disjunction.
(2)
For a set of relational variables,we de?ne trans to be the conjunction of all transitivity constraints for all chord-free cycles in the graph.
Theorem1An assignment to the relational variables will satisfy all of the transitivity con-straints given by Equation1if and only if it satis?es trans.
This theorem follows directly from Proposition3and the encoding given by Equation2.
3.1Enumerating Chord-Free Cycles
To enumerate the chord-free cycles of a graph,we exploit the following properties.An acyclic path is said to have a chord when there is an edge in such that
with,and either or.We classify a chord-free path as terminal when
is in,and as extensible otherwise.
Proposition4A path is chord-free and terminal if and only if the cycle
is chord-free.
This follows by noting that the conditions imposed on a chord-free path are identical to those for a chord-free cycle,except that the latter includes a closing edge.
A proper pre?x of path is a path such that. Proposition5Every proper pre?x of a chord-free path is chord-free and extensible.
Clearly,any pre?x of a chord-free path is also chord-free.If some pre?x with were terminal,then any attempt to add the edge would yield either a simple cycle (when),some other cycle(when for some),or a path having
as a chord.
Given these properties,we can enumerate the set of all chord-free paths by breadth?rst expan-sion.As we enumerate these paths,we also generate,the set of all chord-free cycles.De?ne
to be the set of all extensible,chord-free paths having vertices,for.
Initially we have,and.Given set,we generate set and add some cycles of length to.For each path,we consider the path for each edge in.When for some,we classify the path as cyclic.When there is an edge in for some,we classify the path as having a chord.When there is an edge in,we add the cycle to.Otherwise,we add the path to.
After generating all of these paths,we can use the set to generate the set of all chord-free cycles.For each terminal,chord-free cycle having vertices,there will be members of—each of the edges of the cycle can serve as the closing edge,and a cycle can traverse the closing edge in either direction.To generate the set of clauses given by Equation2,we simply need to choose one element of for each closing edge,e.g.,by considering only cycles for which.
As Figure2indicates,there can be an exponential number of chord-free cycles in a graph. In particular,this?gure illustrates a family of graphs with vertices.Consider the cycles passing through the diamond-shaped faces as well as the edge along the bottom.For each diamond-shaped face,a cycle can pass through either the upper vertex or the lower vertex.Thus there are such cycles.In addition,the edges forming the perimeter of each face create a chord-free cycle,giving a total of chord-free cycles.
The columns labeled“Direct”in Table2show results for enumerating the chord-free cycles for our benchmarks.For each correct microprocessor,we have two graphs:one for which transitivity constraints played no role in the veri?cation,and one(indicated with a“t”at the end of the name) modi?ed to require enforcing transitivity constraints.We summarize the results for the transitivity
1DLX-C78286858
37953484268204
1182,3939,5721726972,091 2DLX-CA-t3002,3006,900
2DLX-CC3002,3006,900
1432,1368,3641938582,574 min.2311,5404,620
avg.3002,3006,900
max.2992,2926,877
1205601,680
402293,0567798294
6307,14021,420
8465,7721,472,1842064081,224
2,01641,664124,992
3.2Adding More Relational Variables
Enumerating the transitivity constraints based on the variables in runs the risk of generating a Boolean formula of exponential size.We can guarantee polynomial growth by considering a larger set of relational variables.In general,let be some set of relational variables such that, and let trans be the transitivity constraint formula generated by enumerating the chord-free cycles in the graph.
Theorem2If is the set of relational variables in sat and,then the formula sat trans is satis?able if and only if sat trans is satis?able.
We introduce a series of lemmas to prove this theorem.For a propositional formula over a set of variables and an assignment,de?ne the valuation of under,denoted ,to be the result of evaluating formula according to assignment.We?rst prove that we can extend any assignment over a set of relational variables to one over a superset of these variables yielding identical valuations for both transistivity constraint formulas.
Lemma1For any sets of relational variables and such that,and for any assignment ,such that trans,there is an assignment such that trans
Proof:We consider the case where.The general statement of the proposition then holds by induction on.
De?ne assignment to be:
Graph has a path of1-edges from node to node.
otherwise
We consider two cases:
1.If,then any cycle in through must contain a0-edge other than
.Hence adding this edge does not introduce any transitivity violations.
2.If,then there must be some path of1-edges between nodes and in
.In order for the introduction of1-edge to create a transitivity violation,there must also be some path between nodes and in containing exactly one0-edge.But then we could concatenate paths and to form a cycle in containing exactly one0-edge,implying that trans.We conclude therefore that adding 1-edge does not introduce any transitivity violations.
Lemma2For and for any assignment,such that trans,we also have trans
Proof:We note that any cycle in must be present in and have the same edge labeling.Thus,if has no cycle with a single0-edge,then neither does.
We now return to the proof of Theorem2.
Proof:Suppose that sat trans is satis?able,i.e.,there is some assignment such that sat trans.Then by Lemma1we can?nd an assignment such that trans.Furthermore,since the construction of by Lemma1preserves the values assigned to all variables in,and these are the only relational variables occurring in sat,we can conclude that sat.Therefore sat trans is satis?able.
Suppose on the other hand that sat trans is satis?able,i.e.,there is some assignment such that sat trans.Then by Lemma2we also have trans,and hence sat trans is satis?able.
Our goal then is to add as few relational variables as possible in order to reduce the size of the transitivity formula.We will continue to use our path enumeration algorithm to generate the transitivity formula.
3.3Dense Enumeration
For the dense enumeration method,let denote the set of variables for all values of and such that.Graph is a complete,undirected graph.In this graph, any cycle of length greater than three must have a chord.Hence our algorithm will enumerate transitivity constraints of the form,for all distinct values of,,and. The graph has edges and chord-free cycles,yielding a total of
transitivity constraints.
The columns labeled“Dense”in Table2show the complexity of this method for the benchmark circuits.For the smaller graphs1DLX-C,1DLX-C-t,and,this method yields more clauses than direct enumeration of the cycles in the original graph.For the larger graphs,however, it yields fewer clauses.The advantage of the dense method is most evident for the mesh graphs, where the cubic complexity is far superior to exponential.
3.4Sparse Enumeration
We can improve on both of these methods by exploiting the sparse structure of.Like the dense method,we want to introduce additional relational variables to give a set of variables such that the resulting graph becomes chordal[Rose70].That is,the graph has the property that every cycle of length greater than three has a chord.
Chordal graphs have been studied extensively in the context of sparse Gaussian elimination.In fact,the problem of?nding a minimum set of additional variables to add to our set is identical to the problem of?nding an elimination ordering for Gaussian elimination that minimizes the amount of?ll-in.Although this problem is NP-complete[Yan81],there are good heuristic solutions.In
Circuit sat trans sat Ratio
Satis?able?Secs.Satis?able?Secs.
N3 1.4 1DLX-C-t N9
2DLX-CA N1,275
Y3N.A.
N5,035 2.0 2DLX-CC-t N15,003
Full Y10.2
Buggy Y125 2.3
2DLX-CC Y2,18669.4
Table3:Performance of FGRASP on Benchmark Circuits.Results are given both without and with transitivity constraints.
particular,our implementation proceeds as a series of elimination steps.On each step,we remove some vertex from the graph.For every pair of distinct,uneliminated vertices and such that the graph contains edges and,we add an edge if it does not already exist.The original graph plus all of the added edges then forms a chordal graph.To choose which vertex to eliminate on a given step,our implementation uses the simple heuristic of choosing the vertex with minimum degree.If more than one vertex has minimum degree,we choose one that minimizes the number of new edges added.
The columns in Table2labeled“Sparse”show the effect of making the benchmark graphs chordal by this method.Observe that this method gives superior results to either of the other two methods.In our implementation we have therefore used the sparse method to generate all of the transitivity constraint formulas.
4SAT-Based Decision Procedures
Most Boolean satis?ability(SA T)checkers take as input a formula expressed in clausal form. Each clause is a set of literals,where a literal is either a variable or its complement.A clause denotes the disjunction of its literals.The task of the checker is to either?nd an assignment to the variables that satis?es all of the clauses or to determine that no such assignment exists.We can solve the constrained satis?ability problem using a conventional SA T checker by generating a set of clauses trans representing trans and a set of clauses sat representing the formula sat. We then run the checker on the combined clause set sat trans to?nd satisfying solutions to
sat trans.
In experimenting with a number of Boolean satis?ability checkers,we have found that FGRASP [MS99]has the best overall performance.The most recent version can be directed to periodically restart the search using a randomly-generated variable assignment[M99].This is the?rst SA T checker we have tested that can complete all of our benchmarks.All of our experiments were
conducted on a336MHz Sun UltraSPARC II with1.2GB of primary memory.
As indicated by Table3,we ran FGRASP on clause sets sat and trans sat,i.e.,both with-out and with transitivity constraints.For benchmarks1DLX-C,2DLX-CA,and2DLX-CC, the formula sat is unsatis?able.As can be seen,including transitivity constraints increases the run time signi?cantly.For benchmarks1DLX-C-t,2DLX-CA-t,and2DLX-CC-t,the for-mula sat is satis?able,but only because transitivity is not enforced.When we add the clauses for trans,the formula becomes unsatis?able.For the buggy circuits,the run times for sat range from under1second to over36minutes.The run times for trans sat range from less than one second to over12hours.In some cases,adding transitivity constraints actually decreased the CPU time(by as much as a factor of5),but in most cases the CPU time increased(by as much as a factor of69).On average(using the geometric mean)adding transitivity constraints increased the CPU time by a factor of2.3.We therefore conclude that satis?ability checking with transitivity constraints is more dif?cult than conventional satis?ability checking,but the added complexity is not overwhelming.
5OBDD-Based Decision Procedures
A simple-minded approach to solving satis?ability with transitivity constraints using OBDDs would be to generate separate OBDD representations of trans and sat.We could then use the A PPLY operation to generate an OBDD for trans sat,and then either?nd a satisfying assignment or determine that the function is unsatis?able.We show that for some sets of relational variables,the OBDD representation of trans can be too large to represent and manipulate.In our experiments,we use the CUDD OBDD package with dynamic variable reordering by sifting.
5.1Lower Bound on the OBDD Representation of trans
We prove that for some sets,the OBDD representation of trans may be of exponential size for all possible variable orderings.As mentioned earlier,the NP-completeness result proved by Goel,et al.[GSZAS98]has implications for the complexity of representing trans as an OBDD.They showed that given an OBDD sat representing formula sat,the task of?nding a satisfying assignment of sat that also satis?es the transitivity constraints in is NP-complete in the size of sat.By this,assuming,we can infer that the OBDD representa-tion of trans may be of exponential size when using the same variable ordering as is used in sat.Our result extends this lower bound to arbitrary variable orderings and is independent of the vs.problem.
Let denote a planar mesh consisting of a square array of vertices.For example, Figure3shows the graph for.Being a planar graph,the edges partition the plane into faces. As shown in Figure3we label these for.There are a total of
such faces.One can see that the set of edges forming the border of each face forms a chord-free cycle of.As shown in Table2,many other cycles are also chord-free,e.g.,the perimeter of any rectangular region having height and width greater than1,but we will consider only the cycles
Figure3:Mesh Graph.
corresponding to single faces.
De?ne to be a set of relational variables corresponding to the edges in.trans
is then an encoding of the transitivity constraints for these variables.
Theorem3Any OBDD representation of trans must have vertices.
To prove this theorem,consider any ordering of the variables representing the edges in. Let denote those in the?rst half of the ordering,and denote those in the second half.We can then classify each face according to the four edges forming its border:
A:All are in.
B:All are in.
C:Some are in,while others are in.These are called“split”faces.
Observe that we cannot have a type A face adjacent to a type B face,since their shared edge cannot be in both and.Therefore there must be split faces separating any region of type A faces from any region of type B faces.
For example,Figure4shows three possible partitionings of the edges of and the resulting classi?cation of the faces.If we let,,and denote the number of faces of each respective type, we see that we always have.In particular,a minimum value for is achieved when the partitioning of the edges corresponds to a partitioning of the graph into a region of type A faces and a region of type B faces,each having nearly equal size,with the split faces forming the boundary between the two regions.
a = 11,
b = 9,
c = 5a = 10, b = 10, c = 5 a = 10, b = 5, c = 10 Figure4:Partitioning Edges into Sets(solid)and(dashed).Each face can then be classi?e
d as typ
e A(all solid),B(all dashed),or C(mixed).
Lemma3For any partitioning of the edges of mesh graph into equally-sized sets and, there must be at least split faces.
Note that this lower bound is somewhat weak—it seems clear that we must have. However,this weaker bound will suf?ce to prove an exponential lower bound on the OBDD size.
Proof:Our proof is an adaptation of a proof by Leighton[Lei92,Theorem1.21]that has a bisection bandwidth of at least.That is,one would have to remove at least edges to split the graph into two parts of equal size.
Observe that has vertices and edges.These edges are split so that
are in and are in.
Let denote the planar dual of.That is,it contains a vertex for each face of ,and edges between pairs of vertices such that the corresponding faces in have a common edge.In fact,one can readily see that this graph is isomorphic to.
Partition the vertices of into sets,,and according to the types of their correspond-ing faces.Let,,and denote the number of elements in each of these sets.Each face of has four bordering edges,and each edge is the border of at most two faces.Thus,as an upper bound on,we must have,giving,and similarly for.In addition,since a face of type A cannot be adjacent in to one of type B,no vertex in can be adjacent in
to one in.
Consider the complete,directed,bipartite graph having as edges the set, i.e.,a total of edges.Given the bounds:,,and
,the minimum value of is achieved when either and
,or vice-versa,giving a lower bound:
We can embed this bipartite graph in by forming a path from vertex to vertex, where either and,or vice-versa.By convention,we will use the path that?rst follows vertical edges to and then follows horizontal edges to.We must have at least one vertex in along each such path,and therefore removing the vertices in would cut all paths.
For each vertex,we can bound the total number of paths passing through it by separately considering paths that enter from the bottom,the top,the left,and the right.For those entering from the bottom,there are at most source vertices and destination vertices,giving at most paths.This quantity is maximized for, giving an upper bound of.A similar argument shows that there are at most
paths entering from the top of any vertex.For the paths entering from the left,there are at most source vertices and destinations,giving at most
paths.This quantity is maximized when,giving an upper bound of.This bound also holds for those paths entering from the right.Thus,removing a single vertex would cut at most paths.
Combining the lower bound on the number of paths,the upper bound on the number of paths cut by removing a single vertex,and the fact that we are removing vertices,we have:
We can rewrite as.Observing that
for all values of,we have:
A set of faces is said to be edge independent when no two members of the set share an edge.
Lemma4For any partitioning of the edges of mesh graph into equally-sized sets and, there must be an edge-independent set of split faces containing at least elements.
Proof:Classify the parity of face as“even”when is even,and as“odd”otherwise. Observe that no two faces of the same parity can have a common edge.Divide the set of split faces into two subsets:those with even parity and those with odd.Both of these subsets are edge independent,and one of them must have at least1/2of the elements of the set of all split faces.
We can now complete the proof of Theorem3Proof:Suppose there is an edge-independent set of split faces.For each split face,choose one edge in and one edge in bordering that face.
For each value,de?ne assignment(respectively,),to the variables representing edges in(resp.,)as follows.For an edge that is not part of any of the split faces,de?ne (resp.,).For an edge that is part of a split face,but it was not one of the ones chosen specially,let(resp.,).For an edge that is the chosen variable in face,
let(resp.,).This will give us an assignment to all of the variables that evaluates to1.That is,for each independent,split face,we will have two1-edges when and four1-edges when.All other cycles in the graph will have at least two0-edges.
On the other hand,for any such that the assignment will cause an evaluation to0,because for any face where,all but one edge will be assigned value1. Thus,the set of assignments forms an OBDD fooling set,as de?ned in[Bry91], implying that the OBDD must have at least vertices.
We have seen that adding relational variables can reduce the number of cycles and therefore simplify the transitivity constraint formula.This raises the question of how adding relational vari-ables affects the BDD representation of the transitivity constraints.Unfortunately,the exponential lower bound still holds.
Corollary1For any set of relational variables such that,any OBDD representation of trans must contain vertices.
The extra edges in introduce complications,because they create cycles containing edges from different faces.As a result,our lower bound is weaker.
De?ne a set of faces as vertex independent if no two members share a vertex.
Lemma5For any partitioning of the edges of mesh graph into equal-sized sets and, there must be a vertex-independent set of split faces containing at least elements.
Proof:Partition the set of split faces into four sets:EE,EO,OE,and OO,where face is assigned to a set according to the values of and:
EE:Both and are even.
EO:is even and is odd.
OE:is odd and is even.
OO:Both and are odd.
Each of these sets is vertex independent.At least one of the sets must contain at least of the elements.Since there are at least split faces,one of the sets must contain at least vertex-independent split faces.
We can now prove Corollary1.
Proof:For any ordering of the variables in,partition them into two sets and such that those in come before those in,and such the number of variables that are in are
equally split between and.Suppose there is a vertex-independent set of split faces.For each value,we de?ne assignments to the variables in and to the variables in.These assignments are de?ned as they are in the proof of Theorem3with the addition that each variable in is assigned value0.Consider the set of assignments for all values.The only cycles in that can have less than two0-edges will be those corresponding to the perimeters of split faces.As in the proof of Theorem3,the set
forms an OBDD fooling set,as de?ned in[Bry91],implying that the OBDD must have at least vertices.
Our lower bounds are fairly weak,but this is more a re?ection of the dif?culty of proving lower bounds.We have found in practice that the OBDD representations of the transitivity con-straint functions arising from benchmarks tend to be large relative to those encountered during the evaluation of sat.For example,although the OBDD representation of trans for benchmark 1DLX-C-t is just2,692nodes(a function over42variables),we have been unable to construct the OBDD representations of this function for either2DLX-CA-t(178variables)or2DLX-CC-t (193variables)despite running for over24hours.
5.2Enumerating and Eliminating Violations
Goel,et al.[GSZAS98]proposed a method that generates implicants(cubes)of the function sat from its OBDD representation.Each implicant is examined and discarded if it violates a transitivity constraint.In our experiments,we have found this approach works well for the normal,correctly-designed pipelines(i.e.,circuits1DLX-C,2DLX-CA,and2DLX-CC)since the formula sat is unsatis?able and hence has no implicants.For all100of our buggy circuits,the?rst implicant generated contained no transitivity violation and hence was a valid counterexample.
For circuits that do require enforcing transitivity constraints,we have found this approach im-practical.For example,in verifying1DLX-C-t by this means,we generated253,216implicants, requiring a total of35seconds of CPU time(vs.0.2seconds for1DLX-C).For benchmarks 2DLX-CA-t and2DLX-CC-t,our program ran for over24hours without having generated all of the implicants.By contrast,circuits2DLX-CA and2DLX-CC can be veri?ed in11and29 seconds,respectively.Our implementation could be improved by making sure that we generate only implicants that are irredundant and prime.In general,however,we believe that a veri?er that generates individual implicants will not be very robust.The complex control logic for a pipeline can lead to formulas sat containing very large numbers of implicants,even when transitivity plays only a minor role in the correctness of the design.
5.3Enforcing a Reduced Set of Transitivity Constraints
One advantage of OBDDs over other representations of Boolean functions is that we can readily determine the true support of the function,i.e.,the set of variables on which the function depends. This leads to a strategy of computing an OBDD representation of sat and intersecting its support with to give a set of relational variables that could potentially lead to transitivity violations. We then augment these variables to make the graph chordal,yielding a set of variables and
1、人称代词顺口溜：人称代词有两类，一类主格一类宾；主格代词本领大，一切动作由它发；宾格代词不动脑，介动之后跟着跑。 2、物主代词顺口溜：物主代词不示弱，带着‘白勺’来捣乱；形容词性物主代，抓住名词不放松； 1、人称代词的主格在句子中作主语或主语补语。一般在句首，动词前。 例如：John waited a while but eventually he went home. 约翰等了一会儿，最后他回家了。 John hoped the passenger would be Mary and indeed it was she. 约翰希望那位乘客是玛丽，还真是她。 说明：在复合句中，如果主句和从句主语相同，代词主语要用在从句中，名词主语用在主句中。在电话用语中常用主格。 例如：When he arrived, John went straight to the bank. 约翰一到就直接去银行了。 I wish to speak to Mary. This is she. 我想和玛丽通话，我就是玛丽。 2、人称代词的宾格在句中作宾语或表语，在动词或介词后。 例如：Do you know him？(作宾语) 你认识他吗？ Who is knocking at the door？It’s me. (作表语) 是谁在敲门？是我。 说明：单独使用的人称代词通常用宾格，即使它代表主语时也是如此。 例如：I like English. Me too. 我喜欢英语。我也喜欢。 3、注意：在动词be 或to be 后的人称代词视其前面的名词或代词而定。 例如：I thought it was she.我以为是她。(主格----主格) I thought it to be her.(宾格----宾格) I was taken to be she.我被当成了她。(主格----主格) They took me to be her.他们把我当成了她。(宾格----宾格) 4、人称代词并列时的排列顺序 1）单数人称代词并列作主语时，其顺序为： 第二人称→第三人称→第一人称 即you and I he/she/it and I you, he/she/it and I 顺口溜：第一人称最谦虚，但若错误责任担，第一人称学当先。 例如：It was I and John that made her angry. 2）复数人称代词作主语时，其顺序为： 第一人称→第二人称→第三人称 即we and you you and they we, you and they
With的用法全解 with结构是许多英语复合结构中最常用的一种。学好它对学好复合宾语结构、不定式复合结构、动名词复合结构和独立主格结构均能起很重要的作用。本文就此的构成、特点及用法等作一较全面阐述，以帮助同学们掌握这一重要的语法知识。 一、 with结构的构成 它是由介词with或without+复合结构构成，复合结构作介词with或without的复合宾语，复合宾语中第一部分宾语由名词或代词充当，第二部分补足语由形容词、副词、介词短语、动词不定式或分词充当，分词可以是现在分词，也可以是过去分词。With结构构成方式如下： 1. with或without-名词/代词+形容词； 2. with或without-名词/代词+副词； 3. with或without-名词/代词+介词短语； 4. with或without-名词/代词 +动词不定式； 5. with或without-名词/代词 +分词。 下面分别举例： 1、 She came into the room，with her nose red because of cold.（with+名词+形容词，作伴随状语）
2、 With the meal over ， we all went home.（with+名词+副词，作时间状语） 3、The master was walking up and down with the ruler under his arm。（with+名词+介词短语，作伴随状语。） The teacher entered the classroom with a book in his hand. 4、He lay in the dark empty house，with not a man ，woman or child to say he was kind to me.（with+名词+不定式，作伴随状语）He could not finish it without me to help him.（without+代词 +不定式，作条件状语） 5、She fell asleep with the light burning.（with+名词+现在分词，作伴随状语） Without anything left in the with结构是许多英 语复合结构中最常用的一种。学好它对学好复合宾语结构、不定式复合结构、动名词复合结构和独立主格结构均能起很重要的作用。本文就此的构成、特点及用法等作一较全面阐述，以帮助同学们掌握这一重要的语法知识。 二、with结构的用法 with是介词，其意义颇多，一时难掌握。为帮助大家理清头绪，以教材中的句子为例，进行分类，并配以简单的解释。在句子中with结构多数充当状语，表示行为方式，伴随情况、时间、原因或条件（详见上述例句）。 1.带着，牵着…… (表动作特征)。如： Run with the kite like this.
精神分裂症的病因及发病机理 精神分裂症病因：尚未明，近百年来的研究结果也仅发现一些可能的致病因素。（一）生物学因素1．遗传遗传因素是精神分裂症最可能的一种素质因素。国内家系调查资料表明：精神分裂症患者亲属中的患病率比一般居民高6.2倍，血缘关系愈近，患病率也愈高。双生子研究表明：遗传信息几乎相同的单卵双生子的同病率远较遗传信息不完全相同 的双卵双生子为高，综合近年来11项研究资料：单卵双生子同病率（56.7%），是双卵双生子同病率（12.7%）的4.5倍，是一般人口患难与共病率的35-60倍。说明遗传因素在本病发生中具有重要作用，寄养子研究也证明遗传因素是本症发病的主要因素，而环境因素的重要性较小。以往的研究证明疾病并不按类型进行遗传，目前认为多基因遗传方式的可能性最大，也有人认为是常染色体单基因遗传或多源性遗传。Shields发现病情愈轻，病因愈复杂，愈属多源性遗传。高发家系的前瞻性研究与分子遗传的研究相结合，可能阐明一些问题。国内有报道用人类原癌基因Ha-ras-1为探针，对精神病患者基因组进行限止性片段长度多态性的分析，结果提示11号染色体上可能存在着精神分裂症与双相情感性精神病有关的DNA序列。2．性格特征：约40%患者的病前性格具有孤僻、冷淡、敏感、多疑、富于幻想等特征，即内向
型性格。3．其它：精神分裂症发病与年龄有一定关系，多发生于青壮年，约1/2患者于20～30岁发病。发病年龄与临床类型有关，偏执型发病较晚，有资料提示偏执型平均发病年龄为35岁，其它型为23岁。80年代国内12地区调查资料：女性总患病率（7.07%。）与时点患病率（5.91%。）明显高于男性（4.33%。与3.68%。）。Kretschmer在描述性格与精神分裂症关系时指出：61%患者为瘦长型和运动家型，12.8%为肥胖型，11.3%发育不良型。在躯体疾病或分娩之后发生精神分裂症是很常见的现象，可能是心理性生理性应激的非特异性影响。部分患者在脑外伤后或感染性疾病后发病；有报告在精神分裂症患者的脑脊液中发现病毒性物质；月经期内病情加重等躯体因素都可能是诱发因素，但在精神分裂症发病机理中的价值有待进一步证实。（二）心理社会因素1．环境因素①家庭中父母的性格，言行、举止和教育方式（如放纵、溺爱、过严）等都会影响子女的心身健康或导致个性偏离常态。②家庭成员间的关系及其精神交流的紊乱。③生活不安定、居住拥挤、职业不固定、人际关系不良、噪音干扰、环境污染等均对发病有一定作用。农村精神分裂症发病率明显低于城市。2．心理因素一般认为生活事件可发诱发精神分裂症。诸如失学、失恋、学习紧张、家庭纠纷、夫妻不和、意处事故等均对发病有一定影响，但这些事件的性质均无特殊性。因此，心理因素也仅属诱发因
with的用法大全----四级专项训练with结构是许多英语复合结构中最常用的一种。学好它对学好复合宾语结构、不定式复合结构、动名词复合结构和独立主格结构均能起很重要的作用。本文就此的构成、特点及用法等作一较全面阐述，以帮助同学们掌握这一重要的语法知识。 一、 with结构的构成 它是由介词with或without+复合结构构成，复合结构作介词with或without的复合宾语，复合宾语中第一部分宾语由名词或代词充当，第二部分补足语由形容词、副词、介词短语、动词不定式或分词充当，分词可以是现在分词，也可以是过去分词。With结构构成方式如下： 1. with或without-名词/代词+形容词; 2. with或without-名词/代词+副词; 3. with或without-名词/代词+介词短语; 4. with或without-名词/代词+动词不定式; 5. with或without-名词/代词+分词。 下面分别举例：
1、 She came into the room，with her nose red because of cold.(with+名词+形容词，作伴随状语) 2、 With the meal over ， we all went home.(with+名词+副词，作时间状语) 3、The master was walking up and down with the ruler under his arm。(with+名词+介词短语，作伴随状语。) The teacher entered the classroom with a book in his hand. 4、He lay in the dark empty house，with not a man ，woman or child to say he was kind to me.(with+名词+不定式，作伴随状语) He could not finish it without me to help him.(without+代词 +不定式，作条件状语) 5、She fell asleep with the light burning.(with+名词+现在分词，作伴随状语) 6、Without anything left in the cupboard， she went out to get something to eat.(without+代词+过去分词，作为原因状语) 二、with结构的用法 在句子中with结构多数充当状语，表示行为方式，伴随情况、时间、原因或条件(详见上述例句)。
with用法归纳 （1）“用……”表示使用工具，手段等。例如： ①We can walk with our legs and feet. 我们用腿脚行走。 ②He writes with a pencil. 他用铅笔写。 （2）“和……在一起”，表示伴随。例如： ①Can you go to a movie with me? 你能和我一起去看电影'>电影吗？ ②He often goes to the library with Jenny. 他常和詹妮一起去图书馆。 （3）“与……”。例如： I’d like to have a talk with you. 我很想和你说句话。 （4）“关于，对于”，表示一种关系或适应范围。例如： What’s wrong with your watch? 你的手表怎么了？ （5）“带有，具有”。例如： ①He’s a tall kid with short hair. 他是个长着一头短发的高个子小孩。 ②They have no money with them. 他们没带钱。 （6）“在……方面”。例如： Kate helps me with my English. 凯特帮我学英语。 （7）“随着，与……同时”。例如： With these words, he left the room. 说完这些话，他离开了房间。 [解题过程] with结构也称为with复合结构。是由with+复合宾语组成。常在句中做状语，表示谓语动作发生的伴随情况、时间、原因、方式等。其构成有下列几种情形： 1.with+名词(或代词)+现在分词 此时，现在分词和前面的名词或代词是逻辑上的主谓关系。 例如:1)With prices going up so fast, we can't afford luxuries. 由于物价上涨很快，我们买不起高档商品。（原因状语） 2)With the crowds cheering, they drove to the palace. 在人群的欢呼声中，他们驱车来到皇宫。（伴随情况） 2.with+名词(或代词)+过去分词 此时，过去分词和前面的名词或代词是逻辑上的动宾关系。
独立主格篇 独立主格，首先它是一个“格”，而不是一个“句子”。在英语中任何一个句子都要有主谓结构，而在这个结构中，没有真正的主语和谓语动词，但又在逻辑上构成主谓或主表关系。独立主格结构主要用于描绘性文字中，其作用相当于一个状语从句，常用来表示时间、原因、条件、行为方式或伴随情况等。除名词/代词+名词、形容词、副词、非谓语动词及介词短语外，另有with或without短语可做独立主格，其中with可省略而without不可以。*注：独立主格结构一般放在句首，表示原因时还可放在句末；表伴随状况或补充说明时，相当于一个并列句，通常放于句末。 一、独立主格结构： 1. 名词/代词+形容词 He sat in the front row, his mouth half open. Close to the bank I saw deep pools, the water blue like the sky. 靠近岸时，我看见几汪深池塘，池水碧似蓝天。 2. 名词/代词+现在分词 Winter coming, it gets colder and colder. The rain having stopped, he went out for a walk.
The question having been settled, we wound up the meeting. 也可以The question settled, we wound up the meeting. 但含义稍有差异。前者强调了动作的先后。 We redoubled our efforts, each man working like two. 我们加倍努力，一个人干两个人的活。 3. 名词/代词+过去分词 The job finished, we went home. More time given, we should have done the job much better. *当表人体部位的词做逻辑主语时，不及物动词用现在分词，及物动词用过去分词。 He lay there, his teeth set, his hands clenched, his eyes looking straight up. 他躺在那儿，牙关紧闭，双拳紧握，两眼直视上方。 4. 名词/代词+不定式 We shall assemble at ten forty-five, the procession to start moving at precisely eleven. We divided the work, he to clean the windows and I to sweep the floor.
精神分裂症的发病原因是什么 精神分裂症是一种精神病，对于我们的影响是很大的，如果不幸患上就要及时做好治疗，不然后果会很严重，无法进行正常的工作和生活，是一件很尴尬的事情。因此为了避免患上这样的疾病，我们就要做好预防，今天我们就请广州协佳的专家张可斌来介绍一下精神分裂症的发病原因。 精神分裂症是严重影响人们身体健康的一种疾病，这种疾病会让我们整体看起来不正常，会出现胡言乱语的情况，甚至还会出现幻想幻听，可见精神分裂症这种病的危害程度。 (1)精神刺激：人的心理与社会因素密切相关，个人与社会环境不相适应，就产生了精神刺激，精神刺激导致大脑功能紊乱，出现精神障碍。不管是令人愉快的良性刺激，还是使人痛苦的恶性刺激，超过一定的限度都会对人的心理造成影响。 (2)遗传因素：精神病中如精神分裂症、情感性精神障碍，家族中精神病的患病率明显高于一般普通人群，而且血缘关系愈近，发病机会愈高。此外，精神发育迟滞、癫痫性精神障碍的遗传性在发病因素中也占相当的比重。这也是精神病的病因之一。 (3)自身：在同样的环境中，承受同样的精神刺激，那些心理素质差、对精神刺激耐受力低的人易发病。通常情况下，性格内向、心胸狭窄、过分自尊的人，不与人交往、孤僻懒散的人受挫折后容易出现精神异常。 (4)躯体因素：感染、中毒、颅脑外伤、肿瘤、内分泌、代谢及营养障碍等均可导致精神障碍，。但应注意，精神障碍伴有的躯体因素，并不完全与精神症状直接相关，有些是由躯体因素直接引起的，有些则是以躯体因素只作为一种诱因而存在。 孕期感染。如果在怀孕期间，孕妇感染了某种病毒，病毒也传染给了胎儿的话，那么，胎儿出生长大后患上精神分裂症的可能性是极其的大。所以怀孕中的女性朋友要注意卫生，尽量不要接触病毒源。 上述就是关于精神分裂症的发病原因，想必大家都已经知道了吧。患上精神分裂症之后，大家也不必过于伤心，现在我国的医疗水平是足以让大家快速恢复过来的，所以说一定要保持良好的情绪。
with用法小结 一、with表拥有某物 Mary married a man with a lot of money . 马莉嫁给了一个有着很多钱的男人。 I often dream of a big house with a nice garden . 我经常梦想有一个带花园的大房子。 The old man lived with a little dog on the lonely island . 这个老人和一条小狗住在荒岛上。 二、with表用某种工具或手段 I cut the apple with a sharp knife . 我用一把锋利的刀削平果。 Tom drew the picture with a pencil . 汤母用铅笔画画。 三、with表人与人之间的协同关系 make friends with sb talk with sb quarrel with sb struggle with sb fight with sb play with sb work with sb cooperate with sb I have been friends with Tom for ten years since we worked with each other, and I have never quarreled with him . 自从我们一起工作以来，我和汤姆已经是十年的朋友了，我们从没有吵过架。 四、with 表原因或理由 John was in bed with high fever . 约翰因发烧卧床。 He jumped up with joy . 他因高兴跳起来。 Father is often excited with wine . 父亲常因白酒变的兴奋。 五、with 表“带来”，或“带有,具有”，在…身上，在…身边之意
精神分裂症的病因是什么 精神分裂症是一种精神方面的疾病，青壮年发生的概率高，一般 在16～40岁间，没有正常器官的疾病出现，为一种功能性精神病。 精神分裂症大部分的患者是由于在日常的生活和工作当中受到的压力 过大，而患者没有一个良好的疏导的方式所导致。患者在出现该情况 不仅影响本人的正常社会生活，且对家庭和社会也造成很严重的影响。 精神分裂症常见的致病因素： 1、环境因素：工作环境比如经济水平低低收入人群、无职业的人群中，精神分裂症的患病率明显高于经济水平高的职业人群的患病率。还有实际的生活环境生活中的不如意不开心也会诱发该病。 2、心理因素：生活工作中的不开心不满意，导致情绪上的失控，心里长期受到压抑没有办法和没有正确的途径去发泄，如恋爱失败， 婚姻破裂，学习、工作中不愉快都会成为本病的原因。 3、遗传因素：家族中长辈或者亲属中曾经有过这样的病人，后代会出现精神分裂症的机会比正常人要高。 4、精神影响：人的心里与社会要各个方面都有着不可缺少的联系，对社会环境不适应，自己无法融入到社会中去，自己与社会环境不相
适应，精神和心情就会受到一定的影响，大脑控制着人的精神世界， 有可能促发精神分裂症。 5、身体方面：细菌感染、出现中毒情况、大脑外伤、肿瘤、身体的代谢及营养不良等均可能导致使精神分裂症，身体受到外界环境的 影响受到一定程度的伤害，心里受到打击，无法承受伤害造成的痛苦，可能会出现精神的问题。 对于精神分裂症一定要配合治疗，接受全面正确的治疗，最好的 疗法就是中医疗法加心理疗法。早发现并及时治疗并且科学合理的治疗，不要相信迷信，要去正规的医院接受合理的治疗，接受正确的治 疗按照医生的要求对症下药，配合医生和家人，给病人创造一个良好 的治疗环境，对于该病的康复和痊愈会起到意想不到的效果。
comparison的用法解析大全 comparison的意思是比较，比喻，下面我把它的相关知识点整理给大家，希望你们会喜欢！ 释义 comparison n. 比较;对照;比喻;比较关系 [ 复数 comparisons ] 词组短语 comparison with 与…相比 in comparison adj. 相比之下;与……比较 in comparison with 与…比较，同…比较起来 by comparison 相比之下，比较起来 comparison method 比较法 make a comparison 进行比较 comparison test 比较检验 comparison theorem 比较定理 beyond comparison adv. 无以伦比 comparison table 对照表 comparison shopping 比较购物;采购条件的比较调查 paired comp arison 成对比较 同根词 词根： comparing adj. comparative 比较的;相当的 comparable 可比较的;比得上的 adv. comparatively 比较地;相当地 comparably 同等地;可比较地 n.
comparative 比较级;对手 comparing 比较 comparability 相似性;可比较性 v. comparing 比较;对照(compare的ing形式) 双语例句 He liked the comparison. 他喜欢这个比喻。 There is no comparison between the two. 二者不能相比。 Your conclusion is wrong in comparison with their conclusion. 你们的结论与他们的相比是错误的。 comparison的用法解析大全相关文章： 1.by的用法总结大全
介词With 复合结构讲解及练习 with复合结构的作用：with复合结构在句子中作状语，表示原因、时间、条件、伴随、方式等. 1）We sat on the dry grass with our backs to the wall.（作伴随状语） 2）She could not leave with her painful duty unfulfilled.（作原因状语） 3）He lay in bed with his head covered.（作方式状语） 4）Jack soon fell asleep with the light still burning.（作伴随状语） 5）I won't be able to go on holiday with my mother being ill.（作原因状语） 6）He sat with his arms clasped around his knees.（作方式状语） 注：with复合结构在句子中还可以作定语，阅读下面的句子。 1）There was a letter for Lanny with a Swiss stamp on it.（作定语修饰letter） 2）It was a vast stretch of country with cities in the distance.（作定语修饰a stretch of country）1) with +宾语+ 现在（短分词语） When mother went into the house, she found her baby was sleeping in bed, with his lips moving. 当妈妈走进房子的时候，她发现自己的孩子正睡在床上，嘴唇一直在动。 My aunt lives in the room with the windows facing south. 我姑妈住在那间窗户朝南开的房间。 With winter coming on，it's time to buy warm clothes 2)with +宾语+ 过去分词（短语） With more and more forests damaged ,some animals and plants are facing the danger of dying out. 由于越来越多的森林遭到破坏，一些动植物正面临着灭绝的危险。 With his legs broken, he had to lie in bed for a long time. 他双腿都断了，只得长时间躺在床上。 3) with +宾语+ 不定式（短语） * With so many children to look after, the nurse is busy all the time. 有这么多的孩子需要照顾，保育员一直都很忙。 *With a lot of papers to correct, M r. Li didn’t attend the party. 李老师有许多试卷需要批改，所以没有参加聚会。 4) with +宾语+ 副词 * You should read with the radio off. 在看书的时候应该把收音机关掉。 * With the temperature up, we had to open all the windows. 气温上升，我们不得不打开所有的窗户。 5) with +宾语+形容词 *With the window open, I felt a bit cold. 窗户开着，我感到有点冷。 * It was cold outside , the boy ran into the room with his nose red. 外面天气很冷，那个男孩跑进了屋子时，鼻子红红的。 6) with +宾语+ 介词短语 * The woman with a baby in her arms is getting on the bus. 怀里抱着婴儿的那位妇女正在上车。 * John starts to work very clearly in the morning and goes on working until late in the afternoon with a break at midday . 约翰早上开始工作，中午稍作休息后又接着工作到下午稍晚些时候。
with[wIT] prep.1.与…(在)一起，带着：Come with me. 跟我一起来吧。/ I went on holiday with my friend. 我跟我朋友一起去度假。/ Do you want to walk home with me? 你愿意和我一道走回家吗 2.(表带有或拥有)有…的，持有，随身带着：I have no money with me. 我没有带钱。/ He is a man with a hot temper. 他是一个脾气暴躁的人。/ We bought a house with a garden. 我们买了一座带花园的房子。/ China is a very large country with a long history. 中国是一个具有历史悠久的大国。3.(表方式、手段或工具)以，用：He caught the ball with his left hand. 他用左手接球。/ She wrote the letter with a pencil. 她用铅笔写那封信。4.(表材料或内容)以，用：Fill the glass with wine. 把杯子装满酒。/ The road is paved with stones. 这条路用石头铺砌。5.(表状态)在…的情况下，…地：He can read French with ease. 他能轻易地读法文。/ I finished my homework though with difficulty. 虽然有困难，我还是做完了功课。6.(表让步)尽管，虽然：With all his money, he is unhappy. 尽管他有钱，他并不快乐。/ With all his efforts, he lost the match. 虽然尽了全力，他还是输了那场比赛。7.(表条件)若是，如果：With your permission, I’ll go. 如蒙你同意我就去。8.(表原因或理由)因为，由于：He is tired with work. 他工作做累了。/ At the news we all jumped with joy. 听到这消息我们都高兴得跳了起来。9.(表时间)当…的时候，在…之后：With that remark, he left. 他说了那话就离开了。/ With daylight I hurried there to see what had happened. 天一亮我就去那儿看发生了什么事。10. (表同时或随同)与…一起，随着：The girl seemed to be growing prettier with each day. 那女孩好像长得一天比一天漂亮。11.(表伴随或附带情况)同时：I slept with the window open. 我开着窗户睡觉。/ Don’t speak with your mouth full. 不要满嘴巴食物说话。12.赞成，同意：I am with you there. 在那点上我同你意见一致。13.由…照看，交…管理，把…放在某处：I left a message for you with your secretary. 我给你留了个信儿交给你的秘书了。/ The keys are with reception. 钥匙放在接待处。14 (表连同或包含)连用，包含：The meal with wine came to ￡8 each. 那顿饭连酒每人8英镑。/ With preparation and marking a teacher works 12 hours a day. 一位老师连备课带批改作业每天工作12小时。15. (表对象或关系)对，关于，就…而言，对…来说：He is pleased with his new house. 他对他的新房子很满意。/ The teacher was very angry with him. 老师对他很生气。/ It’s the same with us students. 我们学生也是这样。16.(表对立或敌对)跟，以…为对手：The dog was fighting with the cat. 狗在同猫打架。/ He’s always arguing with his brother. 他老是跟他弟弟争论。17.(在祈使句中与副词连用)：Away with him! 带他走！/ Off with your clothes! 脱掉衣服！/ Down with your money! 交出钱来！ 【用法】1.表示方式、手段或工具等时(=以，用)，注意不要受汉语意思的影响而用错搭配，如“用英语”习惯上用in English，而不是with English。2.与某些抽象名词连用时，其作用相当于一个副词：with care=carefully 认真地/ with kindness=kindly 亲切地/ with joy=joyfully 高兴地/ with anger=angrily 生气地/ with sorrow=sorrowfully 悲伤地/ with ease=easily 容易地/ with delight=delightedly 高兴地/ with great fluency =very fluently 很流利地3.表示条件时，根据情况可与虚拟语气连用：With more money I would be able to buy it. 要是钱多一点，我就买得起了。/ With better equipment, we could have finished the job even sooner. 要是设备好些，我们完成这项工作还要快些。4.比较with 和as：两者均可表示“随着”，但前者是介词，后者是连词：He will improve as he grows older. 随着年龄的增长，他会进步的。/ People’s ideas change with the change of the times. 时代变了，人们的观念也会变化。5.介词with和to 均可表示“对”，但各自的搭配不同，注意不要受汉语意思的影响而用错，如在kind, polite, rude, good, married等形容词后通常不接介词with而接to。6.复合结构“with+宾语+宾语补足语”是一个很有用的结构，它在句中主要用作状语，表示伴随、原因、时间、条件、方式等；其中的宾语补足语可以是名词、形容词、副词、现在分词、过去分词、不定式、介词短语等：I went out with the windows open. 我外出时没有关窗户。/ He stood before his teacher with his head down. 他低着头站在老师面前。/ He was lying on the bed with all his clothes on. 他和衣躺在床上。/ He died with his daughter yet a schoolgirl. 他去世时，女儿还是个小学生。/ The old man sat there with a basket beside her. 老人坐在那儿，身边放着一个篮子。/ He fell asleep with the lamp burning. 他没熄灯就睡着了。/ He sat there with his eyes closed. 他闭目坐在那儿。/ I can’t go out with all these clothes to wash. 要洗这些衣服，我无法出去了。这类结构也常用于名词后作定语：The boy with nothing on is her son. 没穿衣服的这个男孩子是她儿子。 （摘自《英语常用词多用途词典》金盾出版社） - 1 -
精神分裂症应该怎么治疗 1、坚持服药治疗 服药治疗是最有效的预防复发措施临床大量统计资料表明，大多数精神分裂症的复发与自行停药有关。坚持维持量服药的病人复发率为40%。而没坚持维持量服药者复发率高达80%。因此，病人和家属要高度重视维持治疗。 2、及时发现复发的先兆，及时处理 精神分裂症的复发是有先兆的，只要及时发现，及时调整药物和剂量，一般都能防止复发，常见的复发先兆为：病人无原因出现睡眠不好、懒散、不愿起床、发呆发愣、情绪不稳、无故发脾气、烦躁易怒、胡思乱想、说话离谱，或病中的想法又露头等。这时就应该及时就医，调整治疗病情波动时的及时处理可免于疾病的复发。 3、坚持定期门诊复查 一定要坚持定期到门诊复查，使医生连续地、动态地了解病情，使病人经常处于精神科医生的医疗监护之下，及时根据病情变化调整药量。通过复查也可使端正人及时得到咨询和心理治疗解除病人在生活、工作和药物治疗中的各种困惑，这对预防精神分裂症的复发也起着重要作用。 4、减少诱发因素 家属及周围人要充分认识到精神分裂症病人病后精神状态的薄弱性，帮助安排好日常的生活、工作、学习。经常与病人谈心，帮助病人正确对待疾病，正确对待现实生活，帮助病人提高心理承受能力，学会对待应激事件的方法，鼓励病人增强信心，指导病人充实生活，使病人在没有心理压力和精神困扰的环境中生活。 首先是性格上的改变，塬本活泼开朗爱玩的人，突然变得沉默寡言，独自发呆，不与人交往，爱干净的人也变的不注意卫生、生活
懒散、纪律松弛、做事注意力不集中，总是和患病之前的性格完全 相悖。 再者就是语言表达异常，在谈话中说一些无关的谈话内容，使人无法理解。连最简单的话语都无法准确称述，与之谈话完全感觉不 到重心。 第三个就是行为的异常，行为怪异让人无法理解，喜欢独处、不适意的追逐异性，不知廉耻，自语自笑、生活懒散、时常发呆、蒙 头大睡、四处乱跑，夜不归宿等。 还有情感上的变化，失去了以往的热情，开始变的冷淡、对亲人不关心、和友人疏远，对周围事情不感兴趣，一点消失都可大动干戈。 最后就是敏感多疑，对任何事情比较敏感，精神分裂症患者，总认为有人针对自己。甚至有时认为有人要害自己，从而不吃不喝。 但是也有的会出现难以入眠、容易被惊醒或睡眠不深，整晚做恶梦或者长睡不醒的现象。这些都有可能是患上了精神分裂症。 1.加强心理护理 心理护理是家庭护理中的重要方面，由于社会上普遍存在对精神病人的歧视和偏见，给病人造成很大的精神压力，常表现为自卑、 抑郁、绝望等，有的病人会因无法承受压力而自杀。家属应多给予 些爱心和理解，满足其心理需求，尽力消除病人的悲观情绪。病人 生活在家庭中，与亲人朝夕相处，接触密切，家属便于对病人的情感、行为进行细致的观察，病人的思想活动也易于向家属暴露。家 属应掌握适当的心理护理方法，随时对病人进行启发与帮助，启发 病人对病态的认识，帮助他们树立自信，以积极的心态好地回归社会。 2.重视服药的依从性 精神分裂症病人家庭护理的关键就在于要让病人按时按量吃药维持治疗。如果不按时服药，精神病尤其是精神分裂症的复发率很高。精神病人在医院经过一系统的治疗痊愈后，一般需要维持2~3年的
动名词是一种兼有动词和名词特征的非谓语动词。它可以支配宾语，也能被副词修饰。动名词有时态和语态的变化。 解释：动词的ing形式如果是名词，这个词称动名词。 特征：动词原形+ing构成，具有名词，动词一些特征 一、动名词的作用 动名词具有名词的性质，因此在句中可以作主语、表语、宾语、定语等。 1、作主语 Reading is an art. 读书是一种艺术。 Climbing mountains is really fun. 爬山是真有趣。 Working in these conditions is not a pleasure but a suffer. 在这种工作条件下工作不是愉快而是痛苦。 动名词作主语，有时先用it作形式主语，把动名词置于句末。这种用法在习惯句型中常用。如： It is no use/no good crying over spilt milk. 洒掉的牛奶哭也没用。 It is a waste of time persuading such a person to join us. 劝说这样的人加入真是浪费时间。 It was hard getting on the crowded street car. 上这种拥挤的车真难。 It is fun playing with children. 和孩子们一起玩真好。 There is no joking about such matters. 对这种事情不是开玩笑。 动名词作主语的几种类型 动名词可以在句子中充当名词所能充当的多种句子成分。在这里仅就动名词在句子中作主语的情况进行讨论。 动名词作主语有如下几种常见情况： 1. 直接位于句首做主语。例如： Swimming is a good sport in summer. 2. 用it 作形式主语，把动名词(真实主语)置于句尾作后置主语。 动名词做主语时，不太常用it 作先行主语，多见于某些形容词及名词之后。例如： It is no use telling him not to worry. 常见的能用于这种结构的形容词还有：better，wonderful，enjoyable，interesti ng，foolish，difficult，useless，senseless，worthwhile，等。 注意：important，essential，necessary 等形容词不能用于上述结构。 3. 用于“There be”结构中。例如： There is no saying when he'll come.很难说他何时回来。 4. 用于布告形式的省略结构中。例如： No smoking ( =No smoking is allowed (here) ). （禁止吸烟） No parking. （禁止停车） 5. 动名词的复合结构作主语
介词with的用法大全 With是个介词，基本的意思是“用”，但它也可以协助构成一个极为多采多姿的句型，在句子中起两种作用；副词与形容词。 with在下列结构中起副词作用： 1.“with+宾语+现在分词或短语”，如： (1) This article deals with common social ills, with particular attention being paid to vandalism. 2.“with+宾语+过去分词或短语”，如： (2) With different techniques used, different results can be obtained. (3) The TV mechanic entered the factory with tools carried in both hands. 3.“with+宾语+形容词或短语”，如： (4) With so much water vapour present in the room, some iron-made utensils have become rusty easily. (5) Every night, Helen sleeps with all the windows open. 4.“with+宾语＋介词短语”，如： (6) With the school badge on his shirt, he looks all the more serious. (7) With the security guard near the gate no bad character could do any thing illegal. 5.“with+宾语＋副词虚词”，如： (8) You cannot leave the machine there with electric power on. (9) How can you lock the door with your guests in? 上面五种“with”结构的副词功能，相当普遍，尤其是在科技英语中。 接着谈“with”结构的形容词功能，有下列五种： 一、“with+宾语+现在分词或短语”，如： (10) The body with a constant force acting on it. moves at constant pace. (11) Can you see the huge box with a long handle attaching to it ? 二、“with+宾语+过去分词或短语” (12) Throw away the container with its cover sealed. (13) Atoms with the outer layer filled with electrons do not form compounds. 三、“with+宾语+形容词或短语”，如： (14) Put the documents in the filing container with all the drawers open.