/*
 * sat.h -- minimal CDCL SAT solver
 *
 * Variables are numbered 1..N (DIMACS convention). A literal is a signed
 * integer: +k for variable k, -k for its negation. A clause is a disjunction
 * passed as an array of literals. The formula is the conjunction of all
 * clauses.
 *
 * Typical use:
 *
 *     Sat *s = sat_new(n_vars);
 *     sat_add_clause(s, (int[]){ 1, -2,  3}, 3);
 *     sat_add_clause(s, (int[]){-1,  2, -3}, 3);
 *     int status = sat_solve(s);
 *     if (status == SAT_SATISFIABLE)
 *         for (int v = 1; v <= n_vars; v++)
 *             printf("x%d = %d\n", v, sat_value(s, v));
 *     sat_free(s);
 */

#ifndef SAT_H
#define SAT_H

#ifdef __cplusplus
extern "C" {
#endif

typedef struct Sat Sat;

/* Solver result. */
#define SAT_SATISFIABLE   10
#define SAT_UNSATISFIABLE 20
#define SAT_UNKNOWN        0

/* Variable values returned by sat_value(). */
#define SAT_FALSE  0
#define SAT_TRUE   1
#define SAT_UNDEF -1

/* Create a solver with n_vars variables (numbered 1..n_vars), all initially
 * unassigned. Returns NULL on allocation failure. */
Sat *sat_new(int n_vars);
void sat_free(Sat *s);

/* Add a clause as an array of n_lits signed integers in DIMACS form.
 * Tautologies (containing both v and -v) are silently dropped.
 * Duplicate literals are de-duplicated. The empty clause makes the formula
 * trivially unsatisfiable. Returns 0 on success, 1 if the problem is now
 * trivially UNSAT (an empty clause was added, or a unit clause conflicted
 * with an existing assignment). */
int sat_add_clause(Sat *s, const int *lits, int n_lits);

/* Solve. Returns SAT_SATISFIABLE, SAT_UNSATISFIABLE, or SAT_UNKNOWN if a
 * conflict budget was exhausted. */
int sat_solve(Sat *s);

/* Value of variable v (1..n_vars) after a satisfiable solve. */
int sat_value(const Sat *s, int v);

/* Tuning. Defaults: conflict_limit = -1 (unlimited), verbose = 0. */
void sat_set_conflict_limit(Sat *s, long limit);
void sat_set_verbose(Sat *s, int level);

/* Statistics. */
long sat_decisions       (const Sat *s);
long sat_conflicts       (const Sat *s);
long sat_propagations    (const Sat *s);
long sat_restarts        (const Sat *s);
long sat_learned_clauses (const Sat *s);

#ifdef __cplusplus
}
#endif

#endif
