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:

• C is satisfiable
• There is no other satisfiable subset C' ⊆ F such that |C'| > |C|.

Notice that if F is satisfiable then C = F. Depending on the problem that F encodes, several MaxSAT variants have been proposed. I will discuss two of them: Partial MaxSAT and Weighted MaxSAT. In partial MaxSAT we have soft clauses (relaxable) and hard clauses (non-relaxable). A PMaxSAT solver tries to find the maximum number of satisfiable soft clauses while making sure hard clauses are satisfiable. According to MaxSAT'13 competition a PMaxSAT CNF is specified as : "p wcnf nbvar nbclauses top"[2] where nbvar is the variable number, nbclauses is the number of clauses and top is the weight of hard clauses. Soft clauses have the weight of 1. Example:
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

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...

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...

Why my "touch" lights works without touching?

I have a nice touch light that I had bought some time ago. It works with a simple voltage change logic but recently started switching automatically (better to say unexpectedly). I started googling whether there are some other people having the same problem and I found out it is a well known problem.
Here is one of the useful links : 
http://boards.straightdope.com/sdmb/showthread.php?t=551416

I hope you also find it useful.

Passing command line arguments to MacOSX Applications with GUI and more

Several days back, I was working on a Latex document by using Texworks. The people who used Texworks would know that it is quite useful editor with simple but smart features. One of the main drawbacks of Texworks is (perhaps it is the same for most of Latex editors) it is quite difficult to configure the colors of various components such as background. Background color is quite important as it covers most of the editor surface (and so effects the eyes)... \\

From that point I started looking for ways of changing background color of Texworks and came by this link here : http://www.latex-community.org/forum/viewtopic.php?f=56&t=6921
It explains how to modify the background color of Texworks (which is a Qt application) by playing with some qt parameters... But I had to pass the parameters (i.e. CSS file) to Texworks from command line (which is an Application in my MacOSX). Then I found this link which explains a very simple way of doing it : http://hints.macworld.com/article.php?story=20080809181956219

That didn't finish the story yet :) Then I started pondering around the colors, their effects on us... Which colors are more relaxing, disturbing, natural etc etc. Here is a good link that discusses the issue. It seems the tones of green and blue are more relaxing...

Stay tuned.

Simple image processing with Java

Java has a rich set of libraries for manipulating images. I just use very basic features for the time being and I wanted to put a note here for the newcomers like me. To my understanding, Java uses a protocol when loading a resource (url = getClass().getResource(fileName)) and images "should" be considered as resources (ImageIO.read(url)). Of course there can be other ways of doing it but here is a summary to load resources to Java projects in Eclipse and a piece of code to play with images in Java:
1. http://stackoverflow.com/questions/8960381/runnable-jars-missing-buttons/9278270#9278270
2. http://www.coderanch.com/t/338329/GUI/java/draw-lines-without-change-background

Stay tuned ...

Four key factors in food selection

I recently got a present book from a very "sweet" person in my life. As you can understand from the way I describe the person who gave it to me the book is about foods. It is called "The 150 Healthiest Foods on Earth". I started reading the book and at the very beginning, it came a very important point where four main factors used in the quality rating of foods are listed. I just wanted to list them in this entry:
- Omega-3 fats
- Fiber
- Antioxidants
- Glycemic index