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((int) 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) 


399
400
401
402
403
404
405
406
 
# File 'ext/minisat/minisat.c', line 399

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) 


474
475
476
477
478
479
480
481
 
# File 'ext/minisat/minisat.c', line 474

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

    Data_Get_Struct(rslv, csolver, cslv);

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

#simplify ⇒ Boolean

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

Returns:

  • (Boolean) 


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

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

    Data_Get_Struct(rslv, csolver, cslv);

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

    return Qtrue;
}

#simplify_db ⇒ Boolean

Deprecated. The same as Solver#simplify.

Returns:

  • (Boolean) 


371
372
373
374
 
# File 'ext/minisat/minisat.c', line 371

static VALUE solver_simplify_db(VALUE rslv)
{
    return solver_simplify(rslv);
}

#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) 


458
459
460
461
462
463
464
465
 
# File 'ext/minisat/minisat.c', line 458

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) 


418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
 
# File 'ext/minisat/minisat.c', line 418

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) 


383
384
385
386
387
388
389
390
 
# File 'ext/minisat/minisat.c', line 383

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

    Data_Get_Struct(rslv, csolver, cslv);

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