Explaining the causes of infeasibility of Boolean formulas has many practical applications in electronic design automation and formal verification of hardware.Furthermore,a minimum explanation of infeasibility that ex...Explaining the causes of infeasibility of Boolean formulas has many practical applications in electronic design automation and formal verification of hardware.Furthermore,a minimum explanation of infeasibility that excludes all irrelevant information is generally of interest.A smallest-cardinality unsatisfiable subset called a minimum unsatisfiable core can provide a succinct explanation of infea-sibility and is valuable for applications.However,little attention has been concentrated on extraction of minimum unsatisfiable core.In this paper,the relationship between maximal satisfiability and mini-mum unsatisfiability is presented and proved,then an efficient ant colony algorithm is proposed to derive an exact or nearly exact minimum unsatisfiable core based on the relationship.Finally,ex-perimental results on practical benchmarks compared with the best known approach are reported,and the results show that the ant colony algorithm strongly outperforms the best previous algorithm.展开更多
The minimal unsatisfiability problem is considered of the prepositional formulas in CNF which in the case of variablesx 1,?,x n consist ofn +k clauses including it,x 1 V ? Vx n and ?x 1 V ? V ?x n It is shown that whe...The minimal unsatisfiability problem is considered of the prepositional formulas in CNF which in the case of variablesx 1,?,x n consist ofn +k clauses including it,x 1 V ? Vx n and ?x 1 V ? V ?x n It is shown that whenk ?4 the minimal unsatisfiability problem can be solved in polynomial time.展开更多
In this paper we investigate the complexity of several problems concerning 2CNF formulas. At first, we show that the minimal unsatisfiability problem for 2CNF formulas can be solved in linear time. Then we prove that ...In this paper we investigate the complexity of several problems concerning 2CNF formulas. At first, we show that the minimal unsatisfiability problem for 2CNF formulas can be solved in linear time. Then we prove that the problem determining if a 2CNF formula can be transformed to a minimal unsatisfiable formula is also solvable in linear time. Thirdly, we show the polynomial solvability of the satisfiability problem for symmetric monotone formulas in which all clauses has length 2 or ? n - k ( n is the ...展开更多
Objective: This study aims to use reflective theory and critical emancipatory theory to explore nurses' communicative role with unsatisfied clients.Methods: This paper begins with the broad issue, and the analysis...Objective: This study aims to use reflective theory and critical emancipatory theory to explore nurses' communicative role with unsatisfied clients.Methods: This paper begins with the broad issue, and the analysis will engage Smyth's cycle, which includes describing, analyzing,exploring, and reconstructing.Results: Critical emancipatory reflection is essential to make changes in the professional practice of nursing, because it is of primary importance for the professional learning and development of a nurse.Conclusions: Critical emancipatory reflection helps a nurse to analyze the constraints, including historical, sociocultural, political, and personal aspects.展开更多
Climate change continues to pose a threat to the sustainability of water resources while, water need is increasing. In spite of the efforts made by the state authorities to build water infrastructure, a large majority...Climate change continues to pose a threat to the sustainability of water resources while, water need is increasing. In spite of the efforts made by the state authorities to build water infrastructure, a large majority of the population is not having access to drinking water. In this study, Water Evaluation and Planning (WEAP) model was used to model the current situation of water supply and demands, to create scenarios for future water demands and supply. The results show that, in contrast to the livestock sector, which has a zero DNS, huge deficits are observed in reference scenario. These unsatisfied demands (DNS) are dominated by deficits in rice irrigation. The analysis of the evolution of demand according to the growth scenarios has shown that the deficits already observed in the reference scenario will reach 100.45 × 10<sup>6</sup> m<sup>3</sup> in 2040. To mitigate the effects of such deficits, water management optimization measures have been proposed. Strengthening the water supply to urban centers from the creation of dams could considerably reduce the observed deficits. These results are an important decision support tool for sustainable water resource management in the Lobo watershed. However, these strategies to improve access to water depend on the government’s political will on water and economic opportunities.展开更多
Background The mechanisms responsible for the occurrence of a kissing unsatisfied （KUS） result after classical crush stenting remain unclear. The present study aimed at analyzing the mechanisms and clinical signific...Background The mechanisms responsible for the occurrence of a kissing unsatisfied （KUS） result after classical crush stenting remain unclear. The present study aimed at analyzing the mechanisms and clinical significance of KUS. Methods Two hundred and thirteen patients with true bifurcation lesions treated with classical crush stenting and final kissing balloon inflation （FKBI） were assigned to upper, middle, and lower groups according to the position of the side branch re-wiring assessed by visual estimation, quantitative coronary analysis （QCA） and intravascular ultrasound （IVUS）. Angiographic follow-up was indexed at 12 months. Results The upper group was characterized by a larger bifurcation angle of 55.53°±25.25° （P=0,030） and a longer procedural time （42.43±23.92） minutes （P=0.015）. The overall rate of KUS by visual estimation was 10.48%, with 5.4% in the upper group, 3.9% in middle group, and 36.1% in lower group （P 〈0.001）. For the diagnosis of KUS, visual inspection demonstrated a good correlation with both QCA and IVUS. Smaller stent diameter was the main reason for KUS in the upper group, while extra-stent side wire location, or re-wire in a low position was the main mechanism attributed to KUS in the lower group. The Lower group had more restenosis, with most restenotic lesions at a lower position of the side branch ostium. KUS （HR 1.652, 95% Cl 1.332-2.088, P 〈0.001） and re-wiring position （HR 2.341, 95% Cl 1.780-4.329, P 〈0.001） were two independent predictors of side branch restenosis. Re-wiring position （OR 0.458, 95%C/0.336-0.874, P=0.001） and side stent expansion （OR 3.122, 95%C/2.883-5.061, P=0.014） were factors predicting the findings of KUS. Conclusions Side wire outside side stents resulted in more KUS and restenosis. Different restenotic lesion types reflected individual mechanisms contributing to the development of plaque proliferation.展开更多
Partial Maximum Boolean Satisfiability （Partial Max-SAT or PMSAT） is an optimization variant of Boolean satisfiability （SAT） problem, in which a variable assignment is required to satisfy all hard clauses and a ma...Partial Maximum Boolean Satisfiability （Partial Max-SAT or PMSAT） is an optimization variant of Boolean satisfiability （SAT） problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many reaHife problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis- Putnam-Logemann-Loveland （DPLL） procedure and Branch and Bound （B^B） algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007~2011 Max-SAT evaluations, emphasizing on the most promising research directions.展开更多
基金the National Natural Science Foundation of China (No.60603088)
文摘Explaining the causes of infeasibility of Boolean formulas has many practical applications in electronic design automation and formal verification of hardware.Furthermore,a minimum explanation of infeasibility that excludes all irrelevant information is generally of interest.A smallest-cardinality unsatisfiable subset called a minimum unsatisfiable core can provide a succinct explanation of infea-sibility and is valuable for applications.However,little attention has been concentrated on extraction of minimum unsatisfiable core.In this paper,the relationship between maximal satisfiability and mini-mum unsatisfiability is presented and proved,then an efficient ant colony algorithm is proposed to derive an exact or nearly exact minimum unsatisfiable core based on the relationship.Finally,ex-perimental results on practical benchmarks compared with the best known approach are reported,and the results show that the ant colony algorithm strongly outperforms the best previous algorithm.
基金Project supported by the National Natural Science Foundation of China (Grant No. 19771045)Nationl High-Tech R&D Project (863) (Grant No. 863-306-ET06-01-2).
文摘The minimal unsatisfiability problem is considered of the prepositional formulas in CNF which in the case of variablesx 1,?,x n consist ofn +k clauses including it,x 1 V ? Vx n and ?x 1 V ? V ?x n It is shown that whenk ?4 the minimal unsatisfiability problem can be solved in polynomial time.
文摘In this paper we investigate the complexity of several problems concerning 2CNF formulas. At first, we show that the minimal unsatisfiability problem for 2CNF formulas can be solved in linear time. Then we prove that the problem determining if a 2CNF formula can be transformed to a minimal unsatisfiable formula is also solvable in linear time. Thirdly, we show the polynomial solvability of the satisfiability problem for symmetric monotone formulas in which all clauses has length 2 or ? n - k ( n is the ...
文摘Objective: This study aims to use reflective theory and critical emancipatory theory to explore nurses' communicative role with unsatisfied clients.Methods: This paper begins with the broad issue, and the analysis will engage Smyth's cycle, which includes describing, analyzing,exploring, and reconstructing.Results: Critical emancipatory reflection is essential to make changes in the professional practice of nursing, because it is of primary importance for the professional learning and development of a nurse.Conclusions: Critical emancipatory reflection helps a nurse to analyze the constraints, including historical, sociocultural, political, and personal aspects.
文摘Climate change continues to pose a threat to the sustainability of water resources while, water need is increasing. In spite of the efforts made by the state authorities to build water infrastructure, a large majority of the population is not having access to drinking water. In this study, Water Evaluation and Planning (WEAP) model was used to model the current situation of water supply and demands, to create scenarios for future water demands and supply. The results show that, in contrast to the livestock sector, which has a zero DNS, huge deficits are observed in reference scenario. These unsatisfied demands (DNS) are dominated by deficits in rice irrigation. The analysis of the evolution of demand according to the growth scenarios has shown that the deficits already observed in the reference scenario will reach 100.45 × 10<sup>6</sup> m<sup>3</sup> in 2040. To mitigate the effects of such deficits, water management optimization measures have been proposed. Strengthening the water supply to urban centers from the creation of dams could considerably reduce the observed deficits. These results are an important decision support tool for sustainable water resource management in the Lobo watershed. However, these strategies to improve access to water depend on the government’s political will on water and economic opportunities.
文摘Background The mechanisms responsible for the occurrence of a kissing unsatisfied （KUS） result after classical crush stenting remain unclear. The present study aimed at analyzing the mechanisms and clinical significance of KUS. Methods Two hundred and thirteen patients with true bifurcation lesions treated with classical crush stenting and final kissing balloon inflation （FKBI） were assigned to upper, middle, and lower groups according to the position of the side branch re-wiring assessed by visual estimation, quantitative coronary analysis （QCA） and intravascular ultrasound （IVUS）. Angiographic follow-up was indexed at 12 months. Results The upper group was characterized by a larger bifurcation angle of 55.53°±25.25° （P=0,030） and a longer procedural time （42.43±23.92） minutes （P=0.015）. The overall rate of KUS by visual estimation was 10.48%, with 5.4% in the upper group, 3.9% in middle group, and 36.1% in lower group （P 〈0.001）. For the diagnosis of KUS, visual inspection demonstrated a good correlation with both QCA and IVUS. Smaller stent diameter was the main reason for KUS in the upper group, while extra-stent side wire location, or re-wire in a low position was the main mechanism attributed to KUS in the lower group. The Lower group had more restenosis, with most restenotic lesions at a lower position of the side branch ostium. KUS （HR 1.652, 95% Cl 1.332-2.088, P 〈0.001） and re-wiring position （HR 2.341, 95% Cl 1.780-4.329, P 〈0.001） were two independent predictors of side branch restenosis. Re-wiring position （OR 0.458, 95%C/0.336-0.874, P=0.001） and side stent expansion （OR 3.122, 95%C/2.883-5.061, P=0.014） were factors predicting the findings of KUS. Conclusions Side wire outside side stents resulted in more KUS and restenosis. Different restenotic lesion types reflected individual mechanisms contributing to the development of plaque proliferation.
基金supported by the Research Center of College of Computer and Information Sciences at King Saud University, Saudi Arabia
文摘Partial Maximum Boolean Satisfiability （Partial Max-SAT or PMSAT） is an optimization variant of Boolean satisfiability （SAT） problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many reaHife problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis- Putnam-Logemann-Loveland （DPLL） procedure and Branch and Bound （B^B） algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007~2011 Max-SAT evaluations, emphasizing on the most promising research directions.
