Who are you ?
Data Mining logo

X-MiniSAT : SAT Solver

Projects

Links

Related Events

CRIL logo CNRS logo ANR logo

Introduction

This web page is dedicated to our CDCL-Based SAT solver, named X-MiniSAT. It is based on MiniSAT 2.2 enhanced by different relevent-based learned clauses deletion strategies. Our motivation takes its source from a simple observation on the remarkable performances of both random and size-bounded reduction strategies. In [JLSS'2014], we proposed a new reduction strategy, called Size-Bounded Randomized strategy (in short SBR), that combines maintaing short clauses (of size bounded by k), while deleting randomly clauses of size greater than k. This strategy allows us to select longer clauses that are important for solvng some classes of instances. Reinforced by the impressive performance of keeping short clauses, we propose several new dynamic variants. Their design follows an intuitive simple idea: short learned clauses with literals assigned most often at the top of the current branch of the search tree are considered as relevant.

X-MiniSAT

X-MiniSAT is a CDCL SAT solver based on MiniSAT 2.2. Each version of X-MiniSAT is obtained by instantiating X to one of the relevent-based clauses learning deletion strategy described above. Two categories of strategies are defined. Static strategies set the activity of a given learned clause only when it is derived by conflict analysis. Its activity remains unchanged in the subsequent search. For dynamic strategies, the activity of a given learned clause is updated each time such a clause is the reason of a unit propagated literal. The learned clauses database is reduced in the same way as in MiniSAT. The clauses with smaller activities (or weight) are preferred than those with greater activities.The different implementations of X-MiniSAT are made avaibale below. They can also be obtained by adding few lines of codes to MiniSAT 2.2.

Static

X = SBR(k)
At each conflict, the activity of a learned clause c is set to its size if |c|<=k, otherwise it is set to k+rand(), where rand() randomly generates a real value 0<=w<1. (Download SBR(k)-MiniSAT)
X = Size
At each conflict, the activity of the learned clause c is set to its size. (Download Size-MiniSAT)
X = Rand
At each conflict, the activity of a learned clause c is set to a random real value 0<=w<1. (Download Rand-MiniSAT)
X = FIFO
The learned clauses are managed using a queue. Each time a reduction is performed, the oldest clauses are deleted. (Download FIFO-MiniSAT)

Dynamic

X = SizeD
at each conflict, the activity of the learned clause c is set to its size. During search, suppose that c is propagated at the decision level d. The new activity of c is set to d only if d<=|c|. (Download SizeD-MiniSAT)
X = Size(k)D
the initial activity of c is set as follows: if |c|<=k then A(c)=|c|, otherwise A(c)=k+|c|. Each time, a learned clause c is the reason of a unit propagated literal at decision level d, its activity is updated as follows: if k+d<A(c) then A(c)=k+d. Download Size(k)D-MiniSAT)
X = RelD
Let I be a partial interpretation leading to a conflict at decision level d and c its associated learned clause. The activity of c is initially set to A(c)=sum(i×|c^i|) for 1<=i<=d, where c^i is the set of literals of c assigned at level i. During search, each time c is the reason of a unit propagated literal, and if its new activity w.r.t. the current interpretation is better, the activity of c is updated. A clause c is considered better than a clause c' if A(c)<A(c'). (Download RelD-MiniSAT)

X-Glucose

X-Glucose is a CDCL SAT solver based on one of the state-of-the-art SAT solver Glucose that uses LBD (Literal Block Distance) to predict the most relevant learned clauses. The following versions are obtained from Glucose 3.0 by subtituting LBD with SBR(k) (static) and Size(k)D (dynamic). The following versions are made available only for the evaluation purposes. Our paper [1] is submitted to the SAT 2014 international conference. It is currently under review.

Static

X = SBR(k)
Each time a learned clause c is derived, it receives A(c)=|c| if |c|<=k, otherwise A(c)=k+random(n), where n is the number of variables and random(n) return a positive integer between 1 and n. The activity of c remains unchanged during search. (Download SBR(k)-Glucose)

Dynamic

X = Size(k)D
When a learned clause c is derived, its activity is set as follows: A(c)=|c| if |c|<k, otherwise A(c)=k+|c|. At each conflict, the activity of the learned clauses involved in the derivation of the asserting clause is updated as follows: let d be the conflict decision level, if k+d<A(c) then A(c)=k+d. (Download Size(k)D-Glucose)

X-ManySAT

X-ManySAT is a portfolio-based paralell SAT solver based on ManySAT. ManySAT uses a portfolio of complementary SAT solvers (with clauses sharing), obtained through a careful variation on the main components of CDCL-Based SAT solvers (e.g. Restarts, clauses learning, heuristics). The design of X-ManySAT follows the idea of building a portfolio with orthognal strategies. In X-ManySAT, such orthogonal strategies are obtained thanks to a carfull combination our different learned clauses deletion strategies with the other components of CDCL-Based SAT solvers. The sources of X-ManySAT will be available soon.

Publications

Saïd Jabbour, Jerry Lonlac, Lakhdar Sais and Yakoub Salhi
Revisiting the Learned Clauses Database Reduction Strategies. In coRR, arXiv:1402.1956, February 2014.

Aknowledgment

Our research has been supported by the French ANR Agency under the TUPLES project "Tractability for Understanding and Pushing forward the Limits of Efficient Solvers", the IUT de Lens and University of Artois. We also thank the authors of MiniSAT and Glucose for putting the source code available.