Class: CaDiCaL

Inherits:
Object
  • Object
show all
Defined in:
ext/cadical/cadical_ext.c,
lib/cadical.rb,
lib/cadical/version.rb,
ext/cadical/cadical_ext.c

Overview

A Ruby binding for the CaDiCaL SAT solver.

Decide whether a set of boolean clauses can all be true at once, and if so produce a satisfying assignment.

This is a thin, general-purpose binding over CaDiCaL's C API (ccadical_*).

Typical use:

s = CaDiCaL.new
x = s.new_var
y = s.new_var
s.add(x, y)    # (x \/ y)
s.add(-x, y)   # (!x \/ y)
s.solve        # => :sat
s.true?(y)     # => true
  • Make variables with #new_var (each is just an Integer).
  • A literal is a variable or its negation: v means "variable v is true", -v means false.
  • A clause is a list of literals; add it as a constraint with #add.
  • #solve reports whether the clauses can all be satisfied: :sat if so, :unsat if not.
  • After :sat, read a variable's assigned truth value with #true?.

Constant Summary collapse

VERSION = 
"0.9.0"

Class Method Summary collapse

Instance Method Summary collapse

Class Method Details

.signature ⇒ String

The name of this library.

Returns:

  • (String) 


724
725
726
727
 
# File 'ext/cadical/cadical_ext.c', line 724

static VALUE cad_signature(VALUE klass) {
  (void)klass;
  return rb_str_new_cstr(ccadical_signature());
}

Instance Method Details

#active ⇒ Integer

Returns the number of currently active variables. A variable becomes active if a clause is added with it, and inactive again if it is eliminated or fixed at the root level.

Returns:

  • (Integer) 


521
522
523
 
# File 'ext/cadical/cadical_ext.c', line 521

static VALUE cad_active(VALUE self) {
  return LL2NUM(ccadical_active(get_cad(self, READY)->solver));
}

#add(*lits) ⇒ self

Add a permanent clause: the disjunction of the given literals.

Unlike the C API you need not add the terminating 0, it is appended for you. With no literals it adds the empty clause (an unsatisfiable formula).

Returns:

  • (self) 


166
167
168
169
170
171
172
173
 
# File 'ext/cadical/cadical_ext.c', line 166

static VALUE cad_add(int argc, VALUE *argv, VALUE self) {
  cadical_t *c = get_cad(self, READY);
  int i;
  for (i = 0; i < argc; i++) ccadical_add(c->solver, NUM2INT(argv[i]));
  ccadical_add(c->solver, 0);
  ensure(c, STEADY); /* adding a clause leaves the SATISFIED / UNSATISFIED state */
  return self;
}

#assume(lit) ⇒ self

Assume valid non-zero literal lit for next call to #solve. These assumptions are reset after the call to #solve as well as after returning from #simplify.

See #failed.

Returns:

  • (self) 


184
185
186
187
188
189
 
# File 'ext/cadical/cadical_ext.c', line 184

static VALUE cad_assume(VALUE self, VALUE lit) {
  cadical_t *c = get_cad(self, READY);
  ccadical_assume(c->solver, NUM2INT(lit));
  ensure(c, STEADY);
  return self;
}

#close_proof ⇒ self

Close the proof trace early. Before actually closing, CaDiCaL checks whether a proof step (a clause addition or deletion) has been traced since the last flush and, if so, flushes it first. The file opened by #trace_proof is closed as well.

Raises RuntimeError unless a proof trace is currently open (CaDiCaL would otherwise abort the process).

Returns:

  • (self) 


690
691
692
693
694
695
696
697
 
# File 'ext/cadical/cadical_ext.c', line 690

static VALUE cad_close_proof(VALUE self) {
  cadical_t *c = get_cad(self, READY);
  if (!c->proof_file) rb_raise(rb_eRuntimeError, "no proof trace is open (see #trace_proof)");
  ccadical_close_proof(c->solver);
  fclose(c->proof_file);
  c->proof_file = NULL;
  return self;
}

#conclude ⇒ self

Triggers the conclusion of incremental proofs. If the solver is satisfied it gives the model to the proof tracer; if it is unsatisfied it learns the failing core (for failed assumptions the core negated as a single clause, for a failing constraint possibly several) and concludes with the ids of the newly learnt clauses or the id of the global conflict; if the result was unknown it collects the currently entailed literals and adds them to the proof.

Raises RuntimeError unless a #solve or #simplify has completed.

Returns:

  • (self) 


711
712
713
714
 
# File 'ext/cadical/cadical_ext.c', line 711

static VALUE cad_conclude(VALUE self) {
  ccadical_conclude(get_cad(self, SOLVED)->solver);
  return self;
}

#constrain(*lits) ⇒ self

Same functionality as #add, but the clause only exists for the next call to #solve (same lifetime as assumptions). Only one constraint may exist at a time. A new constraint replaces the old.

See #constraint_failed?.

Returns:

  • (self) 


201
202
203
204
205
206
207
208
 
# File 'ext/cadical/cadical_ext.c', line 201

static VALUE cad_constrain(int argc, VALUE *argv, VALUE self) {
  cadical_t *c = get_cad(self, READY);
  int i;
  for (i = 0; i < argc; i++) ccadical_constrain(c->solver, NUM2INT(argv[i]));
  ccadical_constrain(c->solver, 0);
  ensure(c, STEADY);
  return self;
}

#constraint_failed? ⇒ Boolean

Determine whether the constraint was used to prove the unsatisfiability. Note that the formula might still be unsatisfiable without the constraint.

Raises RuntimeError unless the last #solve returned :unsat.

Returns:

  • (Boolean) 


335
336
337
 
# File 'ext/cadical/cadical_ext.c', line 335

static VALUE cad_constraint_failed(VALUE self) {
  return ccadical_constraint_failed(get_cad(self, UNSATISFIED)->solver) ? Qtrue : Qfalse;
}

#declare_more_variables(n) ⇒ Integer

Increase the maximum variable index by n new variables. Returns the new maximum variable index, which is the highest variable name of the consecutive range of newly declared variables.

Returns:

  • (Integer) 


559
560
561
562
563
564
 
# File 'ext/cadical/cadical_ext.c', line 559

static VALUE cad_declare_more_variables(VALUE self, VALUE n) {
  cadical_t *c = get_cad(self, READY);
  int v = ccadical_declare_more_variables(c->solver, NUM2INT(n));
  ensure(c, STEADY);
  return INT2NUM(v);
}

#declare_one_more_variable ⇒ Integer Also known as: new_var

Returns the next fresh variable that was not used internally.

Returns:

  • (Integer) 


544
545
546
547
548
549
 
# File 'ext/cadical/cadical_ext.c', line 544

static VALUE cad_declare_one_more_variable(VALUE self) {
  cadical_t *c = get_cad(self, READY);
  int v = ccadical_declare_one_more_variable(c->solver);
  ensure(c, STEADY);
  return INT2NUM(v);
}

#failed(lit) ⇒ Boolean

Determine whether the valid non-zero literal lit is in the core. Returns true if the literal is in the core and false otherwise. Note that the core does not have to be minimal.

Raises RuntimeError unless the last #solve returned :unsat.

Returns:

  • (Boolean) 


322
323
324
 
# File 'ext/cadical/cadical_ext.c', line 322

static VALUE cad_failed(VALUE self, VALUE lit) {
  return ccadical_failed(get_cad(self, UNSATISFIED)->solver, NUM2INT(lit)) ? Qtrue : Qfalse;
}

#false_var ⇒ Object

A variable usable as a constant false literal, pinned false with a unit clause.



11
 
# File 'lib/cadical.rb', line 11

def false_var = @false_var ||= new_var.tap { |v| add(-v) }

#fixed(lit) ⇒ 1, ...

Root level assigned variables can be queried with this function. It returns 1 if the literal is implied by the formula, -1 if its negation is implied, or 0 if this is unclear at this point.

Returns:

  • (1, -1, 0) 


347
348
349
 
# File 'ext/cadical/cadical_ext.c', line 347

static VALUE cad_fixed(VALUE self, VALUE lit) {
  return INT2NUM(ccadical_fixed(get_cad(self, READY)->solver, NUM2INT(lit)));
}

#freeze_lit(lit) ⇒ self

#freeze_lit, #melt_lit and #frozen_lit? are reference-counting functions which avoid restoring clauses but require substantial user guidance. This was the only way to use inprocessing in incremental SAT solving in Lingeling (and before in MiniSAT's 'freeze' / 'thaw') and which did not use automatic clause restoring. In general this is slower than restoring clauses and should not be used.

In essence the user freezes variables which potentially are still needed in clauses added or assumptions used after the next #solve call. As in Lingeling you can freeze a variable multiple times, but then have to #melt_lit it the same number of times again in order to enable variable eliminating on it etc. The arguments can be literals (negative indices) but conceptually variables are frozen.

In the old way of doing things without restore you should not use a variable incrementally (in #add or #assume), which was used before and potentially could have been eliminated in a previous #solve call. This can lead to spurious satisfying assignment. In order to check this API contract one can use the "checkfrozen" option (via #set_option). This has the drawback that restoring clauses implicitly would fail with a fatal error message even if in principle the solver could just restore clauses. Thus this option is disabled by default.

See the CaDiCaL SAT'19 paper [FazekasBiereScholl-SAT'19] for more details.

Returns:

  • (self) 


627
628
629
630
 
# File 'ext/cadical/cadical_ext.c', line 627

static VALUE cad_freeze_lit(VALUE self, VALUE lit) {
  ccadical_freeze(get_cad(self, READY)->solver, NUM2INT(lit));
  return self;
}

#frozen_lit?(lit) ⇒ Boolean

Returns whether the variable of lit is currently frozen (see #freeze_lit).

Returns:

  • (Boolean) 


650
651
652
 
# File 'ext/cadical/cadical_ext.c', line 650

static VALUE cad_frozen_lit(VALUE self, VALUE lit) {
  return ccadical_frozen(get_cad(self, READY)->solver, NUM2INT(lit)) ? Qtrue : Qfalse;
}

#get_option(name) ⇒ Integer

Get the current value of the option name. If name is invalid then zero is returned.

Returns:

  • (Integer) 


484
485
486
 
# File 'ext/cadical/cadical_ext.c', line 484

static VALUE cad_get_option(VALUE self, VALUE name) {
  return INT2NUM(ccadical_get_option(get_cad(self, READY)->solver, StringValueCStr(name)));
}

#irredundant ⇒ Integer

Returns the number of currently active irredundant clauses. A clause becomes inactive if it is satisfied, subsumed, or eliminated.

Returns:

  • (Integer) 


532
533
534
 
# File 'ext/cadical/cadical_ext.c', line 532

static VALUE cad_irredundant(VALUE self) {
  return LL2NUM(ccadical_irredundant(get_cad(self, READY)->solver));
}

#limit(name, value) ⇒ self

Specify search limits, where currently name can be "conflicts", "decisions", "preprocessing", or "localsearch". The first two limits are unbounded by default. Thus using a negative limit for conflicts or decisions switches back to the default of unlimited search (for that particular limit). The preprocessing limit determines the number of preprocessing rounds, which is zero by default. Similarly, the local search limit determines the number of local search rounds (zero by default).

These limits are only valid for the next #solve or #simplify call and reset to their default after #solve returns (as well as overwritten and reset during calls to #simplify).

An unknown name raises ArgumentError.

Returns:

  • (self) 


504
505
506
507
508
509
510
511
512
 
# File 'ext/cadical/cadical_ext.c', line 504

static VALUE cad_limit(VALUE self, VALUE name, VALUE limit) {
  const char *n = StringValueCStr(name);
  cadical_t *c = get_cad(self, READY);
  if (strcmp(n, "conflicts") && strcmp(n, "decisions") &&
      strcmp(n, "preprocessing") && strcmp(n, "localsearch"))
    rb_raise(rb_eArgError, "unknown CaDiCaL limit: %s", n);
  ccadical_limit(c->solver, n, NUM2INT(limit));
  return self;
}

#melt_lit(lit) ⇒ self

Melt (thaw) the variable of lit, reversing one #freeze_lit: once its freeze count reaches zero, simplification may eliminate the variable again. The variable must currently be frozen.

Returns:

  • (self) 


639
640
641
642
 
# File 'ext/cadical/cadical_ext.c', line 639

static VALUE cad_melt_lit(VALUE self, VALUE lit) {
  ccadical_melt(get_cad(self, READY)->solver, NUM2INT(lit));
  return self;
}

#phase(lit) ⇒ self

Force the default decision phase of a variable to a certain value (the sign of lit).

Returns:

  • (self) 


582
583
584
585
 
# File 'ext/cadical/cadical_ext.c', line 582

static VALUE cad_phase(VALUE self, VALUE lit) {
  ccadical_phase(get_cad(self, READY)->solver, NUM2INT(lit));
  return self;
}

#release ⇒ nil

Release the solver and its resources now (instead of at GC); the object is unusable afterwards.

Returns:

  • (nil) 


144
145
146
147
148
149
150
151
152
153
 
# File 'ext/cadical/cadical_ext.c', line 144

static VALUE cad_release(VALUE self) {
  cadical_t *c = get_cad(self, READY);
  if (c->proof_file) {
    fclose(c->proof_file);
    c->proof_file = NULL;
  }
  ccadical_release(c->solver);
  c->solver = NULL;
  return Qnil;
}

#set_learn(max_length) {|clause| ... } ⇒ self #set_learn(max_length) ⇒ self

Add a callback which allows to export learned clauses: the block is invoked with each learned clause of at most max_length literals, as an Array of literals. Installing a second callback replaces the first, and calling with no block clears it.

Overloads:

  • #set_learn(max_length) {|clause| ... } ⇒ self

    Yields:

    • (clause)

    Returns:

    • (self)
  • #set_learn(max_length) ⇒ self

    Returns:

    • (self) 


440
441
442
443
444
445
446
447
448
449
450
 
# File 'ext/cadical/cadical_ext.c', line 440

static VALUE cad_set_learn(VALUE self, VALUE max_length) {
  cadical_t *c = get_cad(self, READY);
  if (rb_block_given_p()) {
    c->on_learn = rb_block_proc();
    ccadical_set_learn(c->solver, c, NUM2INT(max_length), learn_trampoline);
  } else {
    c->on_learn = Qnil;
    ccadical_set_learn(c->solver, NULL, NUM2INT(max_length), NULL);
  }
  return self;
}

#set_option(name, value) ⇒ self

Set the option name to value. If the option value is out of range the actual value is computed as the closest (minimum or maximum) value possible. Options can only be set right after initialization; the binding raises RuntimeError otherwise.

Returns:

  • (self) 


473
474
475
476
 
# File 'ext/cadical/cadical_ext.c', line 473

static VALUE cad_set_option(VALUE self, VALUE name, VALUE val) {
  ccadical_set_option(get_cad(self, CONFIGURING)->solver, StringValueCStr(name), NUM2INT(val));
  return self;
}

#set_terminate ⇒ Object

solver.set_terminate -> self

Add a callback which is checked regularly for termination: return a truthy value from the block to abort the search (#solve then returns :unknown). There can only be one such callback; installing a second replaces the first, and calling with no block clears it.



419
420
421
422
423
424
425
426
427
428
429
 
# File 'ext/cadical/cadical_ext.c', line 419

static VALUE cad_set_terminate(VALUE self) {
  cadical_t *c = get_cad(self, READY);
  if (rb_block_given_p()) {
    c->on_terminate = rb_block_proc();
    ccadical_set_terminate(c->solver, c, terminate_trampoline);
  } else {
    c->on_terminate = Qnil;
    ccadical_set_terminate(c->solver, NULL, NULL);
  }
  return self;
}

#simplify ⇒ Object

This function executes preprocessing rounds. It is similar to #solve except that no CDCL nor local search, nor lucky phases are executed. The result values are also the same: :sat, :unsat, or :unknown.

As #solve it resets current assumptions and limits before returning.



273
274
275
276
277
278
279
280
 
# File 'ext/cadical/cadical_ext.c', line 273

static VALUE cad_simplify(VALUE self) {
  cadical_t *c = get_cad(self, READY);
  struct solve_call a = { c->solver, 0 };
  rb_thread_call_without_gvl(do_simplify, &a, unblock_solve, &a);
  ensure(c, a.result == 10 ? SATISFIED : a.result == 20 ? UNSATISFIED : INCONCLUSIVE);
  reraise_pending(c);
  return result_sym(a.result);
}

#solve ⇒ Object

Try to solve the current formula. Returns :sat (satisfiable), :unsat (unsatisfiable), or :unknown (limit reached or interrupted through #terminate).



254
255
256
257
258
259
260
261
 
# File 'ext/cadical/cadical_ext.c', line 254

static VALUE cad_solve(VALUE self) {
  cadical_t *c = get_cad(self, READY);
  struct solve_call a = { c->solver, 0 };
  rb_thread_call_without_gvl(do_solve, &a, unblock_solve, &a);
  ensure(c, a.result == 10 ? SATISFIED : a.result == 20 ? UNSATISFIED : INCONCLUSIVE);
  reraise_pending(c);
  return result_sym(a.result);
}

#terminate ⇒ self

Force termination of #solve asynchronously.

Returns:

  • (self) 


458
459
460
461
 
# File 'ext/cadical/cadical_ext.c', line 458

static VALUE cad_terminate(VALUE self) {
  ccadical_terminate(get_cad(self, READY)->solver);
  return self;
}

#trace_proof(path) ⇒ Boolean

Enable clausal proof tracing to the file at path; returns true if it was successfully opened for writing. Must be called before any #add or #solve, else it raises RuntimeError.

Returns:

  • (Boolean) 


663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
 
# File 'ext/cadical/cadical_ext.c', line 663

static VALUE cad_trace_proof(VALUE self, VALUE path) {
  cadical_t *c = get_cad(self, CONFIGURING);
  const char *p = StringValueCStr(path);
  FILE *f = fopen(p, "w");
  int ok;
  if (!f) rb_sys_fail(p);
  ok = ccadical_trace_proof(c->solver, f, p);
  if (!ok) {
    fclose(f);
    return Qfalse;
  }
  if (c->proof_file) fclose(c->proof_file);
  c->proof_file = f;
  return Qtrue;
}

#true?(lit) ⇒ Boolean

Determine whether lit is assigned to true (i.e. val(lit) == lit).

Raises RuntimeError unless the last #solve returned :sat.

Returns:

  • (Boolean) 


308
309
310
311
 
# File 'ext/cadical/cadical_ext.c', line 308

static VALUE cad_is_true(VALUE self, VALUE lit) {
  int l = NUM2INT(lit);
  return ccadical_val(get_cad(self, SATISFIED)->solver, l) == l ? Qtrue : Qfalse;
}

#true_var ⇒ Object

A variable usable as a constant true literal, pinned true with a unit clause.



8
 
# File 'lib/cadical.rb', line 8

def true_var = @true_var ||= new_var.tap { |v| add(v) }

#unphase(lit) ⇒ self

Reset the default decision phase of +lit+'s variable forced by #phase.

Returns:

  • (self) 


593
594
595
596
 
# File 'ext/cadical/cadical_ext.c', line 593

static VALUE cad_unphase(VALUE self, VALUE lit) {
  ccadical_unphase(get_cad(self, READY)->solver, NUM2INT(lit));
  return self;
}

#val(lit) ⇒ Integer

Get the value of a valid non-zero literal lit. This follows the IPASIR semantics which says to return lit if lit is assigned to true and -lit if lit is assigned to false. This has the consequence that the returned literal is always assigned to true and thus might be a bit confusing. To avoid the headache of these semantics (which we unfortunately should follow to be compatible with IPASIR) the user can simply use positive variable indices instead of literals. Then the returned integer is negative if the variable is assigned to false and positive if it is assigned to true.

Raises RuntimeError unless the last #solve returned :sat.

Returns:

  • (Integer) 


296
297
298
 
# File 'ext/cadical/cadical_ext.c', line 296

static VALUE cad_val(VALUE self, VALUE lit) {
  return INT2NUM(ccadical_val(get_cad(self, SATISFIED)->solver, NUM2INT(lit)));
}

#vars ⇒ Integer

The library internally keeps a maximum variable index, which this returns.

Returns:

  • (Integer) 


572
573
574
 
# File 'ext/cadical/cadical_ext.c', line 572

static VALUE cad_vars(VALUE self) {
  return INT2NUM(ccadical_vars(get_cad(self, READY)->solver));
}