July 28, 2006

Interconnected Scientific Domains

Posted in C++, Computers, Programming, SAT at 10:43 am by pmatos

Today I was just browsing some interesting C++ articles (which will be subject of later post) and I just got face-to-face with ACCU (Association for C/C++ Users) page. I went up to see the benefits of membership and not only the conferences but also the bi-monthly journals caught my attention (and the low-cost fees).

The nice thing is that I was thinking to myself: “So many people in the SAT world program in C++, are they in anyway connected to the more Professional Programming C++ community? My immediate intuitive answer was: No!” which made sense since most of the time people in the research community are worried on publishing the paper and as soon as it is sent for review, a long list of deadlines follows which brings up a lot of more work: more study, more developing, more benchmarks, more writing, more … researching! This is kind of an endless cycle and no time is left in the middle for participating in out-of-the-study-subject community conferences.

Anyway, I went on to check where are the conferences, who are the organizers and which kind of people speak at these conferences. Well, amazed I was to see a name: Oliver Kullman as a speaker for the latest ACCU’06. The name is familiar! The description confirms his identity:

Oliver Kullmann

I did my PhD at the University of Frankfurt (Germany) in Mathematics in 1997. From 1999 to 2001 I was a post-doc in the group of Stephen Cook at the University of Toronto (Canada). In 2001 then I was employed as a lecturer in the computer science department at the University of Wales Swansea, where I stayed since then. Like most researchers, I have given numerous conference talks, publish regularly in international journals and visit researchers at other places.
My research is centred around the understanding of hard computational problems, where “hard” means here something around exponential time, which is typical for most problems in hardware and software verification, in artificial intelligence and in planning and scheduling.
Especially I’m interested in the study of the so-called SAT problem, the problem of deciding whether a propositional formula (boolean variables, connected by “and”, “or” and “not”) is satisfiable or not. Several years ago I’ve written a SAT solver (which was successful at that time), and now for several years I’m developing a generative C++ library for SAT solving (supported by an EPSRC grant since February 2004).

A fellow researcher in SAT is a speaker in a C/C++ users conference. That’s great. Congrats to him!
The application of C/C++ in SAT is huge since most people use it for performance critic software like SAT solvers. The interaction of SAT researchers with C/C++ professional programming seems to be quite useful since SAT researchers spend a great deal of time programming, most of the time in C/C++. So there’s no reason why they shouldn’t try to improve their programming skills and sharing their experiences with these communities. Way to go!


September 8, 2005

SMT & Sudoku

Posted in C++, Computers, Life, Mathematics, Programming, Uncategorized at 10:21 am by pmatos

Hi all,

Inspired by my previous post I’ve decided to create SudokuSMT. A Sudoku to SMT enconding program that converts Sudoku problems into MSAT files to be solved by an SMT solved that understands these kinds of files. You can find more info on my page.

Here’s yesterdays Metro problem solved (Portuguese Ed.).

81 assignments:

var_1_1 = 3.000000
var_2_1 = 1.000000
var_3_1 = 9.000000
var_4_1 = 6.000000
var_5_1 = 8.000000
var_6_1 = 5.000000
var_7_1 = 7.000000
var_8_1 = 4.000000
var_9_1 = 2.000000
var_1_2 = 8.000000
var_2_2 = 6.000000
var_3_2 = 7.000000
var_4_2 = 4.000000
var_5_2 = 9.000000
var_6_2 = 2.000000
var_7_2 = 5.000000
var_8_2 = 3.000000
var_9_2 = 1.000000
var_1_3 = 5.000000
var_2_3 = 2.000000
var_3_3 = 4.000000
var_4_3 = 1.000000
var_5_3 = 7.000000
var_6_3 = 3.000000
var_7_3 = 8.000000
var_8_3 = 9.000000
var_9_3 = 6.000000
var_1_4 = 7.000000
var_2_4 = 8.000000
var_3_4 = 3.000000
var_4_4 = 2.000000
var_5_4 = 1.000000
var_6_4 = 6.000000
var_7_4 = 9.000000
var_8_4 = 5.000000
var_9_4 = 4.000000
var_1_5 = 6.000000
var_2_5 = 4.000000
var_3_5 = 1.000000
var_4_5 = 9.000000
var_5_5 = 5.000000
var_6_5 = 8.000000
var_7_5 = 3.000000
var_8_5 = 2.000000
var_9_5 = 7.000000
var_1_6 = 2.000000
var_2_6 = 9.000000
var_3_6 = 5.000000
var_4_6 = 7.000000
var_5_6 = 3.000000
var_6_6 = 4.000000
var_7_6 = 6.000000
var_8_6 = 1.000000
var_9_6 = 8.000000
var_1_7 = 1.000000
var_2_7 = 5.000000
var_3_7 = 2.000000
var_4_7 = 8.000000
var_5_7 = 6.000000
var_6_7 = 9.000000
var_7_7 = 4.000000
var_8_7 = 7.000000
var_9_7 = 3.000000
var_1_8 = 9.000000
var_2_8 = 7.000000
var_3_8 = 8.000000
var_4_8 = 3.000000
var_5_8 = 4.000000
var_6_8 = 1.000000
var_7_8 = 2.000000
var_8_8 = 6.000000
var_9_8 = 5.000000
var_1_9 = 4.000000
var_2_9 = 3.000000
var_3_9 = 6.000000
var_4_9 = 5.000000
var_5_9 = 2.000000
var_6_9 = 7.000000
var_7_9 = 1.000000
var_8_9 = 8.000000
var_9_9 = 9.000000

May 18, 2005

Achieved the ‘impossible’…

Posted in C++, Computers at 7:55 pm by pmatos

Lately I’ve been having very bad days and… oh well, besides I’m sick for 4 days now, my work is not going as well as I would like. I’ve been running against a semantic C++ error which I just solved 1 hour ago after about a week of searching. The error was terribly simple… I had a class hierarchy as follows:
A -> B -> C
and I had created 2 objects, and I have two objects:
A * a1 = new A();
C * a2 = new A();

I had a public getter in C:
virtual unsigned long getAttr() { return 0; }

and in B I had:
virtual unsigned long getAttr() const { return attr; }

For objects like a1 I received the value of attr and for objects like a2 I received 0. Well, after days of ill-searching (literally, since I’m sick) I found out the problem was with the definition of getAttr. Due to the missing declaration of const in C, polymorphism was not working. Adding const to the definition in C made it work. Fifteen minutes later I add a much nicer. The error resulted in “segmentation fault” without debugging options and worked ok with debugging option on. So I ran valgrind on the debugged version which after various errors and warning outputted told me (what motivated this post):

valgrind: the `impossible’ happened:
Killed by fatal signal

Isn’t this nice… :D