Algorithm

This solver uses an extension of the DPLL algorithm that is used for SAT solving. The algorithm only requires a few changes to work with finite domain SAT. The main procedure looks as follows:

Repeat until there is a result
	If there is a conflict
		If there are no active guesses
			return UNSATISFIABLE
		Else
			Do some conflict handling (undo one or more guesses and continue the search in a different direction)
	While there are unit clauses and there is no conflict
		Propagate the unassigned literal of some unit clause
	If there is no conflict
		If all literals are assigned
			return SATISFIABLE
		Else
			Choose a decision literal and propagate it (make a guess)

If there is a conflict and there are no active guesses, the formula has to be unsatisfiable and the solver can return UNSAT. If there are active guesses, the solver needs to undo one or more guesses such that the conflict is removed and continue the search in another direction. Undoing a decision is called backtracking. The number of active guesses is stored in a global variable int LEVEL.

Unit propagation is a way to simplify the formula. A unit clause is a clause where one literal is unassigned and all other literals are falsified. In such a case for the clause to be true the unassigned literal of the clause has to be set to true. An example would be the clause 1=0 v 1=1 v 2=0 v 2=2 v 3!=0 with the partial assignment 2=1, 3=0, 1!=1. One literal of the clause needs to be true, all literals except for 1=0 are false, so the assignment can be extended to 2=1, 3=0, 1=0.

If all literals are assigned and there is no conflict, the current assignment satisfies the formula and the solver can return that the formula is satisfiable.

If the formula cannot be simplified any further with unit propagation, the solver makes a guess. It chooses some unassigned literal and sets it to true. Which literal is guessed can have a big impact on search time. A satisfiable problem with one solution is solved in linear time if the solver always guesses the correct literal while it will need exponential time if the solver always chooses the wrong literal. To choose a good literal a decision heuristic is used.

Choosing a literal is described in the section Decision heuristics, conflict handling in Conflict handling and the other algorithm parts in Unit and conflict detection.

Data structures

Below is a list of the data structures used by the algorithm.

Formula

The Formula class contains the solver algorithms and stores the information necessary to solve the formula.

• Header file: Formula.h
• Implementation file: Formula.cc

In VARLIST all variables are stored, for details about the variable information see the Variable section.

  vector<Variable *> VARLIST;

CLAUSELIST stores all clauses.

  vector<Clause *> CLAUSELIST;

TIME_S contains the start time and TIME_E the end time of the solving part. This is used to measure the solving time and if a timelimit is set TIME_S is used to determine whether the solver is still within the timelimit or has to abort.

  double TIME_S;
  double TIME_E;

LEVEL stores the current decision level, that is the number of active guesses.

  int LEVEL;

BACKTRACKS, DECISIONS, UNITS and ENTAILS are counters for those events. They are only for analysis purposes and not used by the solver.

• BACKTRACKS counts the number of conflicts that occur during the solving process.
• DECISIONS is increased by 1 whenever a guess is made.
• UNITS counts the number of propagated unit literals. That is a literal from a clause where all literals except for the unit literal are falsified.
• ENTAILS counts how often the solver knows the value of a variable because all but one domain value are falsified.

  int BACKTRACKS;
  int DECISIONS;
  int UNITS;
  int ENTAILS;

UNITLIST contains the clause indices of all current unit clauses. Clauses that become unit during literal propagation are added to that list.

  list <int> UNITLIST;

UNITCLAUSE contains the index of the last propagated unit clause, -1 if the most recent propagation was a decision literal or -2 after an entailment. This is used with non-chronological backtracking to set the reason for a literal.

  int UNITCLAUSE;

CONFLICT is set to true when a conflict is detected.

  bool CONFLICT;

When a conflict occurs in some clause, CONFLICTINGCLAUSE is set to the clause id of that clause. That information is used during conflict analysis with non-chronological backtracking.

int CONFLICTINGCLAUSE;

DECSTACK is a list of all propagated decisions and unit literals. When a literal gets assigned, the current length of DECSTACK is stored in VARLIST[var]->ATOMINDEX[val]. This is used with non-chronological backtracking to determine the order of the assignments.

  vector <Literal> DECSTACK;

TIMELIMIT, RESTARTS, LOG, WATCH and heuristic are set according to the options the user chooses.

• TIMELIMIT is set with the option -time sec, where sec is the time limit in seconds.
• RESTARTS is set with the -restarts num option. The solver restarts (starts over but keeps learned clauses) after every num backtracks. If RESTARTS is 0, the solver never restarts.
• LOG is set to true with the -verbose option.
• WATCH is set to true with -wl. If WATCH is set to true, the solver uses the Watched Literals algorithm.
• heuristic can be set for example with -vsids. For a list of available options see mvl-solver. Heuristic is an enum that contains the possible choices for a decision heuristic. It is defined in the file Global.h.

  int TIMELIMIT;
  int RESTARTS;
  bool LOG;
  bool WATCH;
  Heuristic heuristic;

Variable

The Variable class is used to store information per variable. It stores the variable number, the domain size and, if the variable is completely assigned, the value of the variable. It also uses arrays to store information for every variable domain value.

• Header file: Variable.h
• Implementation file: Variable.cc

VAR and DOMAINSIZE are the id of the variable and the initial domain size. VAL contains the value that is assigned to the variable or -1 if no value was assigned so far.

  int VAR;
  int VAL;
  int DOMAINSIZE;

To store information per literal, arrays are used. Every array entry contains information for a different domain value.

ATOMINDEX is used to determine the order at which the literals got assigned. Literals with a smaller ATOMINDEX value were assigned earlier. The assignment order of the literals is used for non-chronological backtracking.

  int * ATOMINDEX;

ATOMLEVEL contains the decision level where the atom got assigned. It is used in undoTheory to determine which assignments need to be undone.

  int * ATOMLEVEL;

ATOMASSIGN[val] stores the current literal assignment for the domain value val. It contains 1 if the value is set to true, -1 if the value is set to false or 0 if the literal is unassigned.

  int * ATOMASSIGN;

ATOMCNTPOS and ATOMCNTNEG are used by the implemented bookkeeping decision heuristic and explained here.

  int * ATOMCNTPOS;
  int * ATOMCNTNEG;

VSIDS_SCORE and VSIDS_SCORE_NEG are needed for the VSIDS decision heuristic and explained here.

  double * VSIDS_SCORE;
  double * VSIDS_SCORE_NEG;

CLAUSEID stores the reason why a literal was falsified. That reason is used for non-chronological backtracking.

  int * CLAUSEID;

ATOMWATCHPOS and ATOMWATCHNEG store the clause ids of all clauses that watch the corresponding literal. They are only used with watched literals.

  VARRECORD ** ATOMWATCHPOS;
  VARRECORD ** ATOMWATCHNEG;

ATOMRECPOS and ATOMRECNEG are used by the bookkeeping approach for unit and conflict detection (no watched literals). Those fields then contain the clause ids of all clauses where the literal occurs.

  vector<int> * ATOMRECPOS;
  vector<int> * ATOMRECNEG;

VARRECORD is a struct to create a double linked list of clause numbers. Every node contains a clause number and a pointer to the next and previous VARRECORD. If there is no next or previous element, the pointer is set to NULL.

  struct VARRECORD
{
  int c_num;
  VARRECORD * next;
  VARRECORD * prev;
};

Clause

The clause class stores information per clause.

• Header file: Clause.h
• Implementation file: Clause.cc

The vector ATOM_LIST stores the literals of the clause.

  vector <Literal> ATOM_LIST;

NumUnAss and LEVEL are used by the bookkeeping approach for unit and conflict detection. NumUnAss stores the number of unassigned atoms in the clause with regard to the current assignment and LEVEL contains the decision level at which the clause got satisfied or -1 if the clause is not satisfied yet.

  int NumUnAss;
  int LEVEL;

With watched literals, two literals of every clause are watched. Those literals are stored in a Literal array of length two.

  Literal WATCHED[2];

Literal

A literal has a variable and a value. If EQUAL is true, the literal is VAR=VAL. Otherwise the literal is VAR!=VAL.

• Header file: Literal.h

  int VAR;
  int VAL;
  bool EQUAL;