Thanks to the above modifications, input instances of the sat **problem itself (represented simply, in a way that is close to the** dimacs **format) are reduced by the** ursa **system**
to the same instances, up to renaming variables.8 Typically, reducing the size of a formula is an important objective, but a smaller number of clauses does not necessarily mean an easier formula and sometimes adding the right clauses (e.g., those corresponding to symmetry breaking**) can have a positive effect to performance of the solver. Still, guessing and adding clauses that could speed-up the solving**
process is is not performed in the current version of ursa.

6.3. **Invoking the** sat Solver. The ursa **system (currently) uses state-of-the-art** sat solvers ArgoSAT9and clasp.

10 The solvers are called directly through appropriate function calls. Alternatively, the solvers could accept inputs **through files in the standard** dimacs form11 (ursa **can be used just to translate the input problem to** sat**, without solving it).**
In that case, the solvers can be used as a black-box, and could **be replaced by any** sat solver that accepts this input format (and has an option to generate all models of the input propositional formula).

Since during the transformation to cnf **(described above) some variables are eliminated,**
it is necessary to rename all remaining variables (and update the numbers of variables). Namely, if some variables do not occur in the generated cnf**, the solver would consider as** different all models that differ only in the values of such variables. The basic, independent variables (those that correspond to independent ursa **variables) are never eliminated, even** if they don't occur in the generated formula (because their values in all models are relevant).

Along with the generated sat **instance,** ursa **can also pass to the solver the information**
on which propositional variables are independent and which **are dependent. Some** sat solvers can use this information to guide (and hopefully speed-up) the solving process. If the constraint is given by the assert_all **command, the solver is invoked to generate all**
satisfying valuations.12 When multiple invocations of the solver are used (for finding all solutions), the solving process can benefit from clauses learnt in previous invocations.

If there is a statement minimize (or maximize**) used, in the current implementation,**
the problem is solved sequentially for all values from the given range assigned to a relevant 8 **Because of the possible renaming of the variables, solving the same** sat **instance by** ursa **and by the**
underlying solver would not necessarily take the same time as the solving process can take different routes.

9ArgoSAT (http://argo.matf.bg.ac.rs/downloads.html**) is an open-source, flexible, and verified** sat solver [45, 44].

10clasp (http://www.cs.uni-potsdam.de/clasp/**) is a solver for (extended) normal logic programs [27].**
It combines high-level modelling capacities of asp **with state-of-the-art techniques from the area of** sat solving and it can be used as an asp **solver or a** sat **solver.** clasp **was a winner at the** asp **Competition**
2009 in several categories (**http://www.cs.kuleuven.be/~dtai/events/ASP-competition/Results.shtml**)
and a winner at the sat Competition 2009 (http://www.satcompetition.org/**) in categories crafted** sat
+unsat **and Crafted** sat.

11In dimacs form, the number of variables N and the number of clauses L **are given first, and are followed**
by the list of clauses. The variables are represented by natural numbers (from 1 to N**) and their negations**
are represented by corresponding negative numbers (from −1 to −N**). More details about the** dimacs **format**
can be found online: **http://www.satlib.org/Benchmarks/SAT/satformat.ps**.

12**If the solver does not have a feature for generating all satisfying valuations, a simple approach with**
blocking clauses **and successive calls to the solver can be used (a blocking clause, added to the set of initial**
clauses, consists of all literals defining one model negated **— this way, a model once generated will not be**
repeated.