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...
Tuesday, December 10, 2013
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
MaxSAT and Minimally Unsatisfiable Subformulas (Cores) [1]
I have been recently reading a lot about computation of some satisfiable/unsatisfiable subformulas from a given CNF SAT formula. There are many different problem definitions that represent these computations (respective subformulas). I will try to summarize all of them to the extent of my knowledge while trying to give some usecases and respective references. I am going to start first with satisfiability driven subformula computations. The available solvers may be considered as satisfiability-based, unsatisfiability-based or some other techniques [1,3]...
The general name of computing maximum number of satisfiable clauses from a given formula F is MaxSAT. In MaxSAT, we try to find a subset of clauses C ⊆ F such that the followings hold:
p wcnf 3 3 8
1 -1 2
1 -1 3
8 1 2 3
Weighted MaxSAT associates each clause with a weight that is greater than or equal to 1. A WMaxSAT solver tries to find a subformula that has the maximum sum of weights of clauses that are satisfiable (Note here: I think Wiki definition is a bit misleading here...). With weighted MaxSAT one can introduce an ordering between clauses (and thus the high level problem components). There is also a variant in which there are hard clauses. This is a slightly different version of partial MaxSAT with soft clauses having variable weights.
MaxSAT is an active area of research so different variants are proposed every now and then. Many efficient techniques have been/are proposed already...
Stay tuned...
References :
[1] http://en.wikipedia.org/wiki/Maximum_satisfiability_problem
[2] http://maxsat.ia.udl.cat/requirements/
[3] T. Alsinet, F. Manya, J. Planes, "Improved Exact Solvers for Weighted Max-SAT", In Proceedings of Eighth International Conference on Theory and Applications of Satisfiability Testing 2005. NOTE for this paper : For instance, a MaxSAT solver may try to find a truth assignment that minimizes the sum of weights of unsatis ed clauses
The general name of computing maximum number of satisfiable clauses from a given formula F is MaxSAT. In MaxSAT, we try to find a subset of clauses C ⊆ F such that the followings hold:
- C is satisfiable
- There is no other satisfiable subset C' ⊆ F such that |C'| > |C|.
p wcnf 3 3 8
1 -1 2
1 -1 3
8 1 2 3
Weighted MaxSAT associates each clause with a weight that is greater than or equal to 1. A WMaxSAT solver tries to find a subformula that has the maximum sum of weights of clauses that are satisfiable (Note here: I think Wiki definition is a bit misleading here...). With weighted MaxSAT one can introduce an ordering between clauses (and thus the high level problem components). There is also a variant in which there are hard clauses. This is a slightly different version of partial MaxSAT with soft clauses having variable weights.
MaxSAT is an active area of research so different variants are proposed every now and then. Many efficient techniques have been/are proposed already...
Stay tuned...
References :
[1] http://en.wikipedia.org/wiki/Maximum_satisfiability_problem
[2] http://maxsat.ia.udl.cat/requirements/
[3] T. Alsinet, F. Manya, J. Planes, "Improved Exact Solvers for Weighted Max-SAT", In Proceedings of Eighth International Conference on Theory and Applications of Satisfiability Testing 2005. NOTE for this paper : For instance, a MaxSAT solver may try to find a truth assignment that minimizes the sum of weights of unsatis ed clauses
Wednesday, January 23, 2013
Latex (Tex live) update on Macosx
I recently had a problem with my Latex distribution. I was missing a package and as you may probably know, there are so many Tex distributions and it is difficult to keep up-to-date the installation. Updates work for a year and then you need to install tex distribution once more if you want to get new packages that were not there or updated for the new distribution. In these cases, manual installation could be helpful... What I did for manual installation:
- Copied the .sty file to /usr/local/texlive/2010/texmf-dist/tex/latex (note that this may change in your system)
- Ran texhash (with sudo).
Good luck...
- Copied the .sty file to /usr/local/texlive/2010/texmf-dist/tex/latex (note that this may change in your system)
- Ran texhash (with sudo).
Good luck...
Sunday, January 13, 2013
Two's complement, bitwise operations, old school info:)
When I was playing with a Java library, I realized that I need to refresh some prehistoric information. The bitwise operations in Java :
http://www.leepoint.net/notes-java/data/expressions/bitops.html
Then I found myself looking integer representations in binary formats (4Bytes) that are useful to understand the effects of bitwise operations:
http://en.wikipedia.org/wiki/Two%27s_complement
Stay tuned...
http://www.leepoint.net/notes-java/data/expressions/bitops.html
Then I found myself looking integer representations in binary formats (4Bytes) that are useful to understand the effects of bitwise operations:
http://en.wikipedia.org/wiki/Two%27s_complement
Stay tuned...
Subscribe to:
Posts (Atom)
