Back to Index

KCNFS and WalkQBF Integration

After studying and understanding the SAT problem I began to work on the development of a QBF solver for certain kind of Random Formulas. I made team with Yannet Interian, and together we built a QBF solver from the ideas I will explain now.

The general idea was to integrate a SAT Solver and a MINSAT solver together to minimize the Universal Part of a QBF Formula and then send a sub-formula generated from the Universal Assignment and the Existential Part to a SAT solver to prove the unsatisfatibility of the whole formula.

After testing some ideas using shell scripts and separate components we decided to fuse the components together in a unique application. The first step was to understand the data structures and components of KCNFS (A SAT Solver well known for been good at solving random SAT formulas).

KCNFS is a SAT solver written on C. It has the following data structures that work as linked lists to keep the information of the given SAT formula. The Struct CNF keeps the information of each clause from the original formula and is used to iterate through the clauses when solving the SAT problem. The important part here was the integration of KCNFS with WalkQBF. At the beginning WalkQBF was writing text files and then calling KCNFS to solve the files using a shell script but it was not an elegant solution so we fuse them in a unique program translating the clauses found on WalkQBF to the KCNFS data structures direct on memory.

In order to make this idea work the data structures of KCNFS should be visible to WalkQBF. So a new file: k-qbf.h was created. This header contains all the shared resources for both programs: WalkQBF and KCNFS.

k-qbf.h has the two basic KCNFS data structures and also contains the main variables an arrays used to solve a SAT problem in KCNFS.

In k-qbf.h you also can find the function mainKCNFS(int). This function has all the code necessary to run KCNFS. We will talk about the main modifications make to this function later. It is original name was main and it was the main method of the file kcnfs.c.

The function ExitSubformula in walkQBF.c was modified to make it fill the KCNFS’ data structures. Looking at the new code you will notice that there are some new variables and the presence of a preprocessor variable called DEBUG_SUBFORMULAS_OUTPUT. This variable can be defined on the file k-qbf.h in order to output the generated sub-formulas to files. (This is the original way that WalkQBF used to output the sub-formula to files)

In order to fill the KCNFS’ data structures I changed the line fprintf(fp," %d ",aux); for the code in the function readcnf(char*) of kcnfs.c that reads the CNF file into KCNFS. Also the line where the 0, that indicates the end of a clause, is read was changed for [_myc++] = 0; so it can completely fill the KCNFS’ data structure as it was reading from the data file but it was instead read from memory.

If you look to the old and new code and put some attention on the readcnf(char*) function of kcnfs.c you will notice that it now is completely embedded into the function that generates the sub-formulas.

Now if you see the function minsatWalk(int) in walkQBF.c you will notice that after calling the function ExitSubformula(int) it will call the function mainKCNFS(int). This will ensure that the formula is outputted to the KCNFS’ data structures before calling the KCNFS algorithm.

mainKCNFS(int) is the shared main method of KCNFS. The main changes here are the following:

• All the data is cleaned before processing the data structures (this is done to let the algorithm begin from zero at each iteration)
• The arguments parsing is not used (all the code is commented)
• readcnf(char*) is not anymore used since the data structures are filled before calling mainKCNFS.

Understanding the KCNFS Main Linked List

k-qbf.h has two main data structures that are filled in the reading process of KCNFS. The one that has all the information of the clauses: _ssat and the one that stores the information of the clauses in a special way: _wcl.

_ssat is easy to understand. It keeps all the information of the clauses in a linked list. It creates a linked list using the Struct CNF as nodes.

_wcl keeps the information in a different way. It stores in a linked list pointers to linked lists of struct cnf. So those clauses can be interpreted in a different way. In fact, every node has some portion of the totality of the clauses of the sub-formula. The code that fills this structure was pasted without modifications into the walkQBF code.

Tests of Functionality

Finally I present some tests so you can see the results of merging the two programs.

Output of WalkQBF:

Subformula file:

Output after calling $kcnfs subformula-1.cnf

Output calling $walkQBF –f Ql2k3alpha2.00rho1.0-10-1.cnf –N 200

A Final Fix

Finally, KCNFS was originally designed to run only one formula at a time. It uses some dynamic memory management and after some long time runs, we discovered that it was wasting some memory that was not been correctly freed by the program. In order to verify and find this common C bug, the tool called Valgrind was used to search and find the memory leaks. After this important fix was done, the integration with WalkQBF was complete.

 Back to Index