Class: MiniSat::Solver

Inherits:
Object
  • Object
show all
Defined in:
ext/minisat/minisat.c

Instance Method Summary collapse

Instance Method Details

#<<(var_or_lit_or_ary) ⇒ Object

Almost same as Solver#add_caluse. This method receives Array of Variable or Literal.

solver << a          # equivalent to solver.add_clause(a)
solver << [a, b, -c] # equivalent to solver.add_clause(a, b, -c)



272
273
274
275
276
277
278
279
280
281
282
 
# File 'ext/minisat/minisat.c', line 272

static VALUE solver_add_clause_2(VALUE rslv, VALUE rcls)
{
    if(TYPE(rcls) == T_DATA
       && RDATA(rcls)->dfree == (RUBY_DATA_FUNC)value_free) {
      return solver_add_clause(1, &rcls, rslv);
    }
    else {
      rcls = rb_convert_type(rcls, T_ARRAY, "Array", "to_ary");
      return solver_add_clause(RARRAY_LEN(rcls), RARRAY_PTR(rcls), rslv);
    }
}

#[](var) ⇒ Boolean

Returns a value of specified variable if the SAT is satisfied. Raises an exception if not.

Returns:

  • (Boolean) 


292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
 
# File 'ext/minisat/minisat.c', line 292

static VALUE solver_ref_var(VALUE rslv, VALUE rvar)
{
    csolver *cslv;
    cvariable *cvar;

    Data_Get_Struct(rslv, csolver, cslv);
    if(CLASS_OF(rvar) != rb_cVariable) {
        rb_raise(rb_eTypeError,
                 "wrong argument type %s (expected Variable)",
                 rb_obj_classname(rvar));
    }
    check_model_available(cslv->result, 0);
    Data_Get_Struct(rvar, cvariable, cvar);
    switch(wrap_solver_ref_var(cslv->solver, cvar->value)) {
        case 0: return Qfalse;
        case 1: return Qtrue;
    }

    return Qnil;
}

#add_clause(var, lit, ...) ⇒ Object

Adds clause consisting of the literals to the SAT and returns solver itself. If Variables are passed, they are handled as its positive Literal. The SAT may be automatically proved to be always unsatisfiable just after the clause added. In the case, solver.solved? becomes to return true.

solver.add_clause(a, b, -c)  # add clause: (a or b or not c)



242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
 
# File 'ext/minisat/minisat.c', line 242

static VALUE solver_add_clause(int argc, VALUE *argv, VALUE rslv)
{
    csolver *cslv;
    int *lits;

    Data_Get_Struct(rslv, csolver, cslv);
    lits = ALLOCA_N(int, argc);
    convert_lits(lits, argc, argv, rslv);
    if(!wrap_solver_add_clause(cslv->solver, lits, argc)) {
        cslv->result = UNSATISFIABLE;
    }
    else {
        cslv->result = NOT_SOLVED_YET;
        cslv->clause_count++;
    }

    return rslv;
}

#clause_size ⇒ Integer

Returns the count of added clauses.

Returns:

  • (Integer) 


386
387
388
389
390
391
392
393
 
# File 'ext/minisat/minisat.c', line 386

static VALUE solver_clause_size(VALUE rslv)
{
    csolver *cslv;

    Data_Get_Struct(rslv, csolver, cslv);

    return LONG2NUM(cslv->clause_count);
}

#new_var ⇒ Variable

Returns new variable for constructing SAT formula. Raises an exception when the SAT is already prove to be always unsatisfiable.

Returns:



211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
 
# File 'ext/minisat/minisat.c', line 211

static VALUE solver_new_var(VALUE rslv)
{
    csolver *cslv;
    cvariable *cvar;
    VALUE rvar;

    Data_Get_Struct(rslv, csolver, cslv);
    check_model_available(cslv->result, 1);
    rvar =
      Data_Make_Struct(rb_cVariable, cvariable, value_mark, value_free, cvar);
    cvar->value = wrap_solver_new_var(cslv->solver);
    cvar->solver = rslv;
    cslv->result = NOT_SOLVED_YET;
    if(OBJ_TAINTED(rslv)) OBJ_TAINT(rvar);

    return rvar;
}

#satisfied? ⇒ Boolean

Returns true if the SAT is satisfied, or false if not.

Returns:

  • (Boolean) 


461
462
463
464
465
466
467
468
 
# File 'ext/minisat/minisat.c', line 461

static VALUE solver_satisfied_p(VALUE rslv)
{
    csolver *cslv;

    Data_Get_Struct(rslv, csolver, cslv);

    return (cslv->result == SATISFIED ? Qtrue : Qfalse);
}

#simplify_db ⇒ Boolean

Detects conflicts independent of the assumptions. This is useful when the same SAT is solved many times under some different assumptions.

Returns:

  • (Boolean) 


348
349
350
351
352
353
354
355
356
357
358
359
360
361
 
# File 'ext/minisat/minisat.c', line 348

static VALUE solver_simplify_db(VALUE rslv)
{
    csolver *cslv;

    Data_Get_Struct(rslv, csolver, cslv);

    check_model_available(cslv->result, 0);
    if(!wrap_solver_simplify_db(cslv->solver)) {
        cslv->result = UNSATISFIABLE;
        return Qfalse;
    }

    return Qtrue;
}

#solve ⇒ Boolean

Determines whether the SAT is satisfiable or not. Returns true if the SAT is satisfied, false otherwise.

Returns:

  • (Boolean) 


321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
 
# File 'ext/minisat/minisat.c', line 321

static VALUE solver_solve(int argc, VALUE *argv, VALUE rslv)
{
    csolver *cslv;
    int *lits;

    Data_Get_Struct(rslv, csolver, cslv);
    lits = ALLOCA_N(int, argc);
    convert_lits(lits, argc, argv, rslv);
    if(wrap_solver_solve(cslv->solver, lits, argc)) {
        cslv->result = SATISFIED;
        return Qtrue;
    }
    else {
        cslv->result =
          argc == 0 ? UNSATISFIABLE : UNSATISFIABLE_UNDER_ASSUMPTIONS;
        return Qfalse;
    }
}

#solved? ⇒ Boolean

Returns true if the SAT is solved, or false if not.

Returns:

  • (Boolean) 


445
446
447
448
449
450
451
452
 
# File 'ext/minisat/minisat.c', line 445

static VALUE solver_solved_p(VALUE rslv)
{
    csolver *cslv;

    Data_Get_Struct(rslv, csolver, cslv);

    return (cslv->result != NOT_SOLVED_YET ? Qtrue : Qfalse);
}

#to_s ⇒ String

Creates a printable version of solver.

p solver  #=> #<MiniSat::Solver:0xb7d3c1d0 not solved yet>
p solver  #=> #<MiniSat::Solver:0xb7d3c1d0 satisfied>
p solver  #=> #<MiniSat::Solver:0xb7d3c1d0 unsatisfiable>

Returns:

  • (String) 


405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
 
# File 'ext/minisat/minisat.c', line 405

static VALUE solver_to_s(VALUE rslv)
{
    const char *cname = rb_obj_classname(rslv);
    const char *msg = NULL;
    char *buf;
    csolver *cslv;
    VALUE str;
    size_t len;

    Data_Get_Struct(rslv, csolver, cslv);
    switch(cslv->result) {
        case NOT_SOLVED_YET:
            msg = "not solved yet";
            break;
        case SATISFIED:
            msg = "satisfied";
            break;
        case UNSATISFIABLE:
            msg = "unsatisfiable";
            break;
        case UNSATISFIABLE_UNDER_ASSUMPTIONS:
            msg = "unsatisfiable under assumptions";
            break;
    }
    len = strlen(cname) + strlen(msg) + 6 + 16;
    buf = ALLOCA_N(char, len);
    snprintf(buf, len + 1, "#<%s:%p %s>", cname, (void*)rslv, msg);
    str = rb_str_new2(buf);
    if(OBJ_TAINTED(rslv)) OBJ_TAINT(str);

    return str;
}

#var_size ⇒ Integer

Returns the count of defined variables.

Returns:

  • (Integer) 


370
371
372
373
374
375
376
377
 
# File 'ext/minisat/minisat.c', line 370

static VALUE solver_var_size(VALUE rslv)
{
    csolver *cslv;

    Data_Get_Struct(rslv, csolver, cslv);

    return LONG2NUM(wrap_solver_var_size(cslv->solver));
}