SatBox: Reuse of SAT Solvers

The Davis-Putnam-Logemann-Loveland (DPLL) method is one of the major practical methods for the satisfiability (SAT) problem of propositional logic. In the last decade, many techniques are proposed to increase the high performance of SAT solvers. A great effort by the SAT community has been made to present these SAT techniques clearly and neatly so that it will be easier for people to implement them in other search/reasoning systems. However, it is still a great challenge to implement these SAT techniques as efficient as the top SAT solvers, as it involves a lot of complicated details and needs a lot of fine-tuning. To meet this challenge, we started the SatBox project. SatBox is a set of library functions which can be used in any backtrack search system to support propositional variable abstraction, boolean constraint propagation, conflict-direct learning and intelligent back-jumping. Satbox can do everything as in the standard DPLL method except the splitting rule. As a result, SatBox is not a complete search tool but a tool for partial model construction. All the state-of-the-arts SAT solvers can be modified easily to implement these library functions and support such an interface, so that any progress made in the development of SAT solvers can be brought into Satbox.

The code of SatBox1.0 based on SATO

Most Basic Functions Provided in SatBox

• void satbox_init ();
  Initialize Satbox with the maximum number of propositional variables, i.e., the value of max_atom, to be used in Satbox. This value will help Satbox to use memory wisely. For some applications, we do not know the exact value of max_atom; in this case, we need to provide a high estimate.
• void satbox_input_clause (int literal_array[], int size);
  Insert an input clause into Satbox, where size tells how many literals (represented by an integer) in the array literal_array. This function should be called before any calling of the next function.
• int satbox_decide_true (int literal, int output[]);
  Increase the search level by one, assert an unassigned literal to be true, and then do boolean constraint propagation (BCP). During BCP, if a conflict is found, Satbox will do conflict analysis, generate a lemma and keep it, backtrack to a level dictated by the lemma, and then do BCP again. If another conflict is found, the same process is repeated once again. If no backtrack is possible, 0 is returned by satbox_decide_true; otherwise 1 is returned, along with more information in output: the first element of output is the current level maintained by Satbox; the second element is the number of new literals assigned true at the current level; the rest elements are those literals. This function should be called before the calling of the next two functions. If this function is called for the first time, BCP will be called first on the input clauses and the function will return 0 if a conflict is found among the input clauses.
• int satbox_assert_true (int literal, int output[]);
  Do the same as satbox_decide_true, except that the search level will not be increased. The returned values by this function and in output have the same meaning as those of satbox_decide_true. This function is useful when the decision procedures for other theories have forced some literals to be true.
• int satbox_insert_clause (int literal_array[], int size, int output[]);
  Insert a clause into SatBox after the search has started (i.e., after satbox_decide_true is called), where size tells how many literals in the array literal_array. Satbox checks the newly inserted clause to see if it is one of the following two cases: (a) It is a conflict at the current level. If yes, backtrack and do BCP. (b) It is a unit clause at the current level. If yes, do BCP. The returned values by this function and in output are the same as those of satbox_decide_true.
• int satbox_insert_lemma (int literal_array[], int size, int output[]);
  Insert a lemma into Satbox. This function works in the same way as satbox_insert_clause, with the only exception that Satbox may delete this lemma later if the space is a concern.

Most Basic Functions Required by SatBox

• void weight_add1_satbox ( int literal );
  Satbox uses this function to tell the outside world that literal appeared in the newly generated lemma inside Satbox.
• int dpllt_reason_satbox ( int literal, int literal_array[] );
  Satbox uses this function to get the reason why literal is assigned true by satbox_assert_true. Here, the reason is a list of literals which contributed to the assignment of literal. This list of literals is stored in literal_array and the size of the list is returned by this function.

Example of Using SatBox

Here is an implementation of the standard DPLL method using SatBox. The only missing functions are read_one_clause, which reads a clause from the input, and select_next_literal, which returns the next splitting literal.

   int DPLL ()
   {
     int literal, result, literal_array[100], output[1000];

     satbox_init(1000); // assuming at most 1000 variables
     while (read_one_clause(literal_array, &size)) {
       if (size == 0) return UNSATISFIABLE; // an empty input clause is found.
       satbox_input_clause(literal_array, size);
     }

     while (true) {
       literal = select_next_literal();
       if (literal == 0) return SATISFIABLE; // no more unassigned literals
       result = satbox_decide_true(literal, output);
       if (result == 0) return UNSATISFIABLE; // no backtrack available
     }       
   }