kissatSolver.h File Reference

#include "aig/gia/gia.h"
#include "sat/cnf/cnf.h"

Include dependency graph for kissatSolver.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
struct	kissat_solver_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct kissat_solver_	kissat_solver
	INCLUDES ///.

Functions
kissat_solver *	kissat_solver_new (void)
	MACRO DEFINITIONS ///.
void	kissat_solver_delete (kissat_solver *s)
int	kissat_solver_addclause (kissat_solver *s, int *begin, int *end)
int	kissat_solver_solve (kissat_solver *s, int *begin, int *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
int	kissat_solver_nvars (kissat_solver *s)
int	kissat_solver_addvar (kissat_solver *s)
void	kissat_solver_setnvars (kissat_solver *s, int n)
int	kissat_solver_get_var_value (kissat_solver *s, int v)
Vec_Int_t *	kissat_solve_cnf (Cnf_Dat_t *pCnf, char *pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose)

Typedef Documentation

kissat_solver

typedef typedefABC_NAMESPACE_HEADER_START struct kissat_solver_ kissat_solver

INCLUDES ///.

CFile****************************************************************

FileName [kissatSolver.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT solver Kissat by Armin Biere, University of Freiburg]

Synopsis [https://github.com/arminbiere/kissat]

Author [Integrated into ABC by Yukio Miyasaka]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

kissatSolver.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 41 of file kissatSolver.h.

Function Documentation

kissat_solve_cnf()

Vec_Int_t * kissat_solve_cnf ( Cnf_Dat_t * pCnf, char * pArgs, int nConfs, int nTimeLimit, int fSat, int fUnsat, int fPrintCex, int fVerbose )

extern

Function*************************************************************

Synopsis [Solves the given CNF using kissat.]

Description []

SideEffects []

SeeAlso []

Definition at line 206 of file kissatSolver.c.

{
    abctime clk = Abc_Clock();
    Vec_Int_t * vRes = NULL;
    int i, * pBeg, * pEnd, RetValue;    
    if ( fVerbose )
        printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
    kissat_solver *pSat = kissat_solver_new();
    kissat_solver_setnvars(pSat, pCnf->nVars);
    assert(kissat_solver_nvars(pSat) == pCnf->nVars);
    Cnf_CnfForClause( pCnf, pBeg, pEnd, i ) {
        if ( !kissat_solver_addclause(pSat, pBeg, pEnd) )
        {
            assert( 0 ); // if it happens, can return 1 (unsatisfiable)
            return NULL;
        }    
    }
    RetValue = kissat_solver_solve(pSat, NULL, NULL, 0, 0, 0, 0);
    if ( RetValue == 1 )
      printf( "Result: Satisfiable.  " );
    else if ( RetValue == -1 )
      printf( "Result: Unsatisfiable.  " );
    else
      printf( "Result: Undecided.  " );
    if ( RetValue == 1 ) {
        vRes = Vec_IntAlloc( pCnf->nVars );
        for ( i = 0; i < pCnf->nVars; i++ )
          Vec_IntPush( vRes, kissat_solver_get_var_value(pSat, i) );
    }
    kissat_solver_delete(pSat);
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return vRes;
}

Here is the call graph for this function:

kissat_solver_addclause()

int kissat_solver_addclause ( kissat_solver * s, int * begin, int * end )

extern

Function*************************************************************

Synopsis [add clause]

Description [kissat takes x and -x as a literal for a variable x > 0, where 0 is an indicator of the end of a clause. since variables start from 0 in abc, a variable v is translated into v + 1 in kissat.]

SideEffects []

SeeAlso []

Definition at line 82 of file kissatSolver.c.

                                                                    {
  for(;begin != end; begin++) {
    if(*begin & 1) {
      kissat_add((kissat*)s->p, -(1 + ((*begin) >> 1)));
    } else {
      kissat_add((kissat*)s->p,   1 + ((*begin) >> 1) );
    }
  }
  kissat_add((kissat*)s->p, 0);
  return !kissat_is_inconsistent((kissat*)s->p);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_solver_addvar()

int kissat_solver_addvar ( kissat_solver * s )

extern

Function*************************************************************

Synopsis [add new variable]

Description [emulated using "nVars".]

SideEffects []

SeeAlso []

Definition at line 158 of file kissatSolver.c.

                                           {
  return s->nVars++;
}

Here is the caller graph for this function:

kissat_solver_delete()

void kissat_solver_delete ( kissat_solver * s )

extern

Function*************************************************************

Synopsis [delete solver]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file kissatSolver.c.

                                            {
  kissat_release((kissat*)s->p);
  free(s);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_solver_get_var_value()

int kissat_solver_get_var_value ( kissat_solver * s, int v )

extern

Function*************************************************************

Synopsis [get value of variable]

Description [kissat returns x (true) or -x (false) for a variable x. note a variable v was translated into v + 1 in kissat.]

SideEffects []

SeeAlso []

Definition at line 190 of file kissatSolver.c.

                                                         {
  return kissat_value((kissat*)s->p, v + 1) > 0;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_solver_new()

kissat_solver * kissat_solver_new ( void )

extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

CFile****************************************************************

FileName [kissatSolver.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT solver Kissat by Armin Biere, University of Freiburg]

Synopsis [https://github.com/arminbiere/kissat]

Author [Integrated into ABC by Yukio Miyasaka]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

kissatSolver.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [allocate solver]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file kissatSolver.c.

                                       {
  kissat_solver* s = (kissat_solver*)malloc(sizeof(kissat_solver));
  s->p = (void*)kissat_init();
  s->nVars = 0;
  return s;
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_solver_nvars()

int kissat_solver_nvars ( kissat_solver * s )

extern

Function*************************************************************

Synopsis [get number of variables]

Description [emulated using "nVars".]

SideEffects []

SeeAlso []

Definition at line 143 of file kissatSolver.c.

                                          {
  return s->nVars;
}

Here is the caller graph for this function:

kissat_solver_setnvars()

void kissat_solver_setnvars ( kissat_solver * s, int n )

extern

Function*************************************************************

Synopsis [set number of variables]

Description [not only emulate with "nVars" but also reserve memory.]

SideEffects []

SeeAlso []

Definition at line 173 of file kissatSolver.c.

                                                    {
  s->nVars = n;
  kissat_reserve((kissat*)s->p, n);
}

Here is the call graph for this function:

Here is the caller graph for this function:

kissat_solver_solve()

int kissat_solver_solve ( kissat_solver * s, int * begin, int * end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal )

extern

Function*************************************************************

Synopsis [solve with resource limits]

Description [assumptions and inspection limits are not supported.]

SideEffects []

SeeAlso []

Definition at line 105 of file kissatSolver.c.

                                                                                                                                                                          {
  // assumptions are not supported
  assert(begin == end);
  // inspection limits are not supported
  assert(nInsLimit == 0);
  assert(nInsLimitGlobal == 0);
  // set conflict limits
  if(nConfLimit)
    kissat_set_conflict_limit((kissat*)s->p, nConfLimit);
  if(nConfLimitGlobal && (nConfLimit == 0 || nConfLimit > nConfLimitGlobal))
    kissat_set_conflict_limit((kissat*)s->p, nConfLimitGlobal);
  // solve
  int res = kissat_solve((kissat*)s->p);
  // translate this kissat return value into a corresponding ABC status value
  switch(res) {
  case  0: // UNDETERMINED
    return 0;
  case 10: // SATISFIABLE
    return 1;
  case 20: // UNSATISFIABLE
    return -1;
  default:
    assert(0);
  }
  return 0;
}

Here is the call graph for this function:

Here is the caller graph for this function: