Here are some links about the issues related to the use of RequestMapping (PostMapping, GetMapping etc) : Stack Exchange Link
The main issue is when a client (e.g. through Apache HTTP client) sends requests to a servlet with the relevant parameters (here be careful where parameter is posted: in the header or the body, see here and here) the servlet will receive/process the parameters according to a pre-agreement...
Spring framework provides useful functionality and annotations (e.g. PostMapping) to automate/shorten all content negotiation related stuff. See here.
Monday, October 2, 2017
Tuesday, August 15, 2017
Spring MVC Apps with Eclipse and Maven
If you are not a long time developer of Java servlet applications with Spring tools, it is exhausting to go around and spot what is necessary for developing a dynamic Web application with Eclipse by using Spring MVC. Of course if your application development goes hand to hand with maven development/configuration, it will be great.
Here is a great starter for this (note : based on crunchify tutorial):
- You first create a dynamic Web project in Eclipse (see here)
- Then you convert the project to Maven project from (right click) Configure/Convert to Maven Project
- Create a Spring configuration file (usually yourproject-servlet.xml). Here you can also use annotation driven view resolving rather than a URL-based. To do that just add "
- Generate a deployment a descriptor (web.xml) and configure this file. As it is with other servlets this file provides the mapping (among other info) between URLs and servlets. Spring maps the URLs to DispatcherServlet. If you are using Eclipse and started your project as a dynamic Web project, sometimes this file is not generated. But fear not! You can generate a stub file by right clicking your project and choosing Java EE Tools --> Generate Deployment Descriptor Stub ...
- Define your Spring controllers.
- Compiling through Maven : Run as / Maven Build
- Running through Eclipse (make sure you installed Tomcat as a server in Eclipse): Run as / Run on Server.
Monday, July 24, 2017
Bitmasking
This is a good post about bitmasking (efficient way of representing subsets of a set) :
https://www.quora.com/What-is-bitmasking-What-kind-of-problems-can-be-solved-using-it
https://www.quora.com/What-is-bitmasking-What-kind-of-problems-can-be-solved-using-it
Tuesday, December 10, 2013
Hashing Strings with md5 from Linux console
Sometimes, I needed to generate md5 hash of a given string from Linux console. Here is how this can done: echo -n "your text" | md5sum
Stay tuned...
Stay tuned...
Tuesday, March 5, 2013
MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [4]
Variable MUSes
An alternative way of explaining inconsistencies in a formula is Variable MUSes (VMUSes) [1]. In plain words, a variable MUS of an unsatisfiable formula F is a subset of variables of F, denoted as Var(F), that defines all variables in an unsatisfiable formula and none of its proper subsets is so. In order to define VMUSes, the concept of induced formula is used. Given a formula F, a formula induced by a variable set V is subformula of F, denoted as F|v, and is the following F|v = {c | c ∈ F and Var(c)}. The set F|v is basically the set of clauses from F, that contains only the variables in V.
By using the notions defined above, a subformula F|v of a given F is said to be a VMUS if the following conditions hold:
- F is UnSAT and V ⊆Var(F)
- F|v is unSAT
- For any V' ⊂ V, F|v' is SAT
[1] presents two variations of VMUSes:
References
[1] A. Belov, A. Ivrii, A. Matsliah and J. Marques-Silva, On Efficient Computation of Variable MUSes, SAT 2012.
An alternative way of explaining inconsistencies in a formula is Variable MUSes (VMUSes) [1]. In plain words, a variable MUS of an unsatisfiable formula F is a subset of variables of F, denoted as Var(F), that defines all variables in an unsatisfiable formula and none of its proper subsets is so. In order to define VMUSes, the concept of induced formula is used. Given a formula F, a formula induced by a variable set V is subformula of F, denoted as F|v, and is the following F|v = {c | c ∈ F and Var(c)}. The set F|v is basically the set of clauses from F, that contains only the variables in V.
By using the notions defined above, a subformula F|v of a given F is said to be a VMUS if the following conditions hold:
- F is UnSAT and V ⊆Var(F)
- F|v is unSAT
- For any V' ⊂ V, F|v' is SAT
[1] presents two variations of VMUSes:
- Interesting VMUS (IVMUS)
- Group VMUS (GVMUS)
References
[1] A. Belov, A. Ivrii, A. Matsliah and J. Marques-Silva, On Efficient Computation of Variable MUSes, SAT 2012.
Monday, March 4, 2013
MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [3]
Coming Back to MUSes and MSSes...
The computation of minimal unsatisfiable subformulas attracted a lot of interest in the recent years. There are several motivations behind this increased interest. First, the complexity (e.g. size) of problems solved by SAT solvers increased a lot recently. For instance, abstraction-refinement model checkers need better abstractions that will help speed up the process. Second, understanding the reasons of conflicts/inconsistencies in a CNF formula requires concise descriptions that are comprehensible by developers. Third, similar to relationship between explanations and relaxations of CSP problems, there is a duality between MUSes and maximally satisfiable subformulas (MSS) and this duality avails the (possible) uses of MSSes. A detailed overview is provided in [1] and [2].
Given a CNF formula F, a minimal unsatisfiable subformula C is a subset of clauses from F (C ⊆ F) that is unsatisfiable and removal of a clause c from C makes C \ {c} satisfiable. The minimum unsatisfiable subformula is one such subformula that has minimum cardinality. The computation of minimum unsatisfiable subformula is given as ∑2-complete in [3]. An important point here related to computation of MUSes from MSSes, in an analogy to computation of explanations from relaxations as discussed in the previous post, is the following from [1]: because computing SAT is in NP (i.e. relatively easy) and UnSAT is CoNP, MSSes are computed first....
However, in general it is not enough to obtain one MUS to explain inconsistencies as there might be many of them. Moreover, the number of clauses contained in a MUS (i.e. inconsistency explanation) can be large leading to a situation the developer can not comprehend or can not understand the reason accurately. Thus several variations of MUS computations have been proposed to make MUSes more concise. I will discuss two of them in here leaving some others to future posts. The first one has been introduced in [1], optimized in [4] and [5]. We will call High-level MUS in what follows. The second one is presented in [6] and we will call it Variable MUS.
High-level MUSes
I am going to discuss High-Level MUSes here with a chronological approach, i.e. towards most recent paper...
[1] In some applications of SAT such as model checking and formal equivalence verification (FEV), MUSes are usually low-level projections (are generated from) of some high-level statements written in a more expressive (and presumably more compact) notation such as first-order logic. Thus one is interested in finding MUSes that are closer to these high-level statements. In order to explain how High-level MUSes are obtained, we first need to explain the concept "selector-variable". A boolean variable v is a selector variable that implies a clause C, v → C (i.e. -v ∨ C). It can be used to enable (by assigning true) or disable (by assigning false) the clause C.
By using selector variables we can identify each clause or group them. In particular, the set of clauses that are associated with the same high-level statement can be marked with the same selector variable. Given a set of clauses {c1,c2,c3,c4} and a set of selector variables F={v1,v2}, consider the following CNF encoding:
-v1 ∨ c1
-v2 ∨ c2
-v2 ∨ c3
-v1 ∨ c4
This encoding can effectively associate {c1,c4} with v1 and {c2,c3} with v2.
[2] focuses on finding one high-level MUS even though the approach can be used for standard MUS extraction. It provides two algorithms: resolution-based MUS extraction and selector-variable based MUS extraction. In general the algorithm first finds a clause-level non-minimal unsatisfiable subformula that contains a part of a projection of an interesting clause (i.e. an equisatisfiable formula obtained by Tseitin transformation) and then tries to squeeze it to minimal. I won't provide the details of algorithms but just present the High-Level MUS definition in the paper. Given a formula F = f1 ∧ f2 ... ∧ fn where each f is a propositional formula and a propositional formula R (called remainder), a high-level MUS, denoted as UC(F,R), imply the following conditions:
- F ∧ R is UnSAT,
- it is a subset of F, i.e. UC(F,R) ⊆ F
- UC(F,R) ∧ R is UnSAT
Here each f ∈ F is called an interesting constraint.
In the next post, I will discuss Variable MUSes...
References:
[1] Mark H. Liffiton and Karem A. Sakallah, "Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints", Journal of Automated Reasoning, 2008
[2] Éric Grégoire, Bertrand Mazure, Cédric Piette, "On Approaches to Explaining Infeasibility of Sets of Boolean Clauses", 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), 2008
[3] Anupam Gupta, "Learning Abstractions for Model Checking", PhD Thesis, CMU, 2006
[4] Alexander Nadel, "Boosting Minimal Unsatisfiable Core Extraction", Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design
[5] V. Ryvchinm, O. Strichman, "Faster Extraction of High-Level Minimal Unsatisfiable Cores", Proceedings of the 14th international conference on Theory and application of satisfiability testing (SAT), 2011.
[6] A. Belov, A. Ivrii, A. Matsliah, J. Marques-Silva, "On efficient computation of variable MUSes", Proceedings of the 15th international conference on Theory and Applications of Satisfiability Testing(SAT), 2011.
The computation of minimal unsatisfiable subformulas attracted a lot of interest in the recent years. There are several motivations behind this increased interest. First, the complexity (e.g. size) of problems solved by SAT solvers increased a lot recently. For instance, abstraction-refinement model checkers need better abstractions that will help speed up the process. Second, understanding the reasons of conflicts/inconsistencies in a CNF formula requires concise descriptions that are comprehensible by developers. Third, similar to relationship between explanations and relaxations of CSP problems, there is a duality between MUSes and maximally satisfiable subformulas (MSS) and this duality avails the (possible) uses of MSSes. A detailed overview is provided in [1] and [2].
Given a CNF formula F, a minimal unsatisfiable subformula C is a subset of clauses from F (C ⊆ F) that is unsatisfiable and removal of a clause c from C makes C \ {c} satisfiable. The minimum unsatisfiable subformula is one such subformula that has minimum cardinality. The computation of minimum unsatisfiable subformula is given as ∑2-complete in [3]. An important point here related to computation of MUSes from MSSes, in an analogy to computation of explanations from relaxations as discussed in the previous post, is the following from [1]: because computing SAT is in NP (i.e. relatively easy) and UnSAT is CoNP, MSSes are computed first....
However, in general it is not enough to obtain one MUS to explain inconsistencies as there might be many of them. Moreover, the number of clauses contained in a MUS (i.e. inconsistency explanation) can be large leading to a situation the developer can not comprehend or can not understand the reason accurately. Thus several variations of MUS computations have been proposed to make MUSes more concise. I will discuss two of them in here leaving some others to future posts. The first one has been introduced in [1], optimized in [4] and [5]. We will call High-level MUS in what follows. The second one is presented in [6] and we will call it Variable MUS.
High-level MUSes
I am going to discuss High-Level MUSes here with a chronological approach, i.e. towards most recent paper...
[1] In some applications of SAT such as model checking and formal equivalence verification (FEV), MUSes are usually low-level projections (are generated from) of some high-level statements written in a more expressive (and presumably more compact) notation such as first-order logic. Thus one is interested in finding MUSes that are closer to these high-level statements. In order to explain how High-level MUSes are obtained, we first need to explain the concept "selector-variable". A boolean variable v is a selector variable that implies a clause C, v → C (i.e. -v ∨ C). It can be used to enable (by assigning true) or disable (by assigning false) the clause C.
By using selector variables we can identify each clause or group them. In particular, the set of clauses that are associated with the same high-level statement can be marked with the same selector variable. Given a set of clauses {c1,c2,c3,c4} and a set of selector variables F={v1,v2}, consider the following CNF encoding:
-v1 ∨ c1
-v2 ∨ c2
-v2 ∨ c3
-v1 ∨ c4
This encoding can effectively associate {c1,c4} with v1 and {c2,c3} with v2.
[2] focuses on finding one high-level MUS even though the approach can be used for standard MUS extraction. It provides two algorithms: resolution-based MUS extraction and selector-variable based MUS extraction. In general the algorithm first finds a clause-level non-minimal unsatisfiable subformula that contains a part of a projection of an interesting clause (i.e. an equisatisfiable formula obtained by Tseitin transformation) and then tries to squeeze it to minimal. I won't provide the details of algorithms but just present the High-Level MUS definition in the paper. Given a formula F = f1 ∧ f2 ... ∧ fn where each f is a propositional formula and a propositional formula R (called remainder), a high-level MUS, denoted as UC(F,R), imply the following conditions:
- F ∧ R is UnSAT,
- it is a subset of F, i.e. UC(F,R) ⊆ F
- UC(F,R) ∧ R is UnSAT
Here each f ∈ F is called an interesting constraint.
In the next post, I will discuss Variable MUSes...
References:
[1] Mark H. Liffiton and Karem A. Sakallah, "Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints", Journal of Automated Reasoning, 2008
[2] Éric Grégoire, Bertrand Mazure, Cédric Piette, "On Approaches to Explaining Infeasibility of Sets of Boolean Clauses", 20th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), 2008
[3] Anupam Gupta, "Learning Abstractions for Model Checking", PhD Thesis, CMU, 2006
[4] Alexander Nadel, "Boosting Minimal Unsatisfiable Core Extraction", Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design
[5] V. Ryvchinm, O. Strichman, "Faster Extraction of High-Level Minimal Unsatisfiable Cores", Proceedings of the 14th international conference on Theory and application of satisfiability testing (SAT), 2011.
[6] A. Belov, A. Ivrii, A. Matsliah, J. Marques-Silva, "On efficient computation of variable MUSes", Proceedings of the 15th international conference on Theory and Applications of Satisfiability Testing(SAT), 2011.
Thursday, February 28, 2013
MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [2]
Now we start for minimal unsatisfiable subformulas (MUSes) which I categorize unsatisfiability driven as given in the first post. They are sometimes called as minimal unsatisfiable cores in the literature. I believe the research on computing MUSes made the relation between explanations and relaxations (relaxations in short) in CSP research more prominent. I can not say that one triggered/inspired the other as I do not have enough chronological information...
Explanations and Relaxations in CSP
Relaxations[1] are used to explain the reasons (culprits) of inconsistencies and to (optimally) resolve those inconsistencies in over-constrained CSP problems. Given a CSP problem with a set of user constraints C and background constraints B (hard constraints), explanations and relaxations are sets of constraints CE ⊆ ℘C and CR ⊆ ℘C respectively. An explanation R ∈ CE is (subset) minimal if the following conditions hold:
In very short terms, the relation between explanations and relaxations is the following: the complement of each hitting set of all minimal relaxations is one maximal relaxation. A constructive way of computing explanations is to check the consistency of B ∪ C and iteratively remove one constraint until an unconsistency is obtained. Thus relaxations are computed first. More details are available at [1].
We stop here with CSP explanations and relaxations and start with SAT MUSes in the next post...
References:
[1] Ulrich Junker, "QUICKXPLAIN: Preferred Explanations and Relaxations for Over-Constrained Problems", Proceedings of the Nineteenth National Conference on Artificial Intelligence (AAAI), 2004
Explanations and Relaxations in CSP
Relaxations[1] are used to explain the reasons (culprits) of inconsistencies and to (optimally) resolve those inconsistencies in over-constrained CSP problems. Given a CSP problem with a set of user constraints C and background constraints B (hard constraints), explanations and relaxations are sets of constraints CE ⊆ ℘C and CR ⊆ ℘C respectively. An explanation R ∈ CE is (subset) minimal if the following conditions hold:
- R = {ci, ... , cn} is unsatisfiable
- Removal of a constraint c from R is satisfiable, i.e. R \ {c} is consistent.
- R = {ci,...,cn} is satisfiable
- Addition of a constraint c to R makes the formula unsatisfiable, i.e. let c ∉ R, the formula R ∪ c is inconsistent.
In very short terms, the relation between explanations and relaxations is the following: the complement of each hitting set of all minimal relaxations is one maximal relaxation. A constructive way of computing explanations is to check the consistency of B ∪ C and iteratively remove one constraint until an unconsistency is obtained. Thus relaxations are computed first. More details are available at [1].
We stop here with CSP explanations and relaxations and start with SAT MUSes in the next post...
References:
[1] Ulrich Junker, "QUICKXPLAIN: Preferred Explanations and Relaxations for Over-Constrained Problems", Proceedings of the Nineteenth National Conference on Artificial Intelligence (AAAI), 2004
Subscribe to:
Posts (Atom)
