Program Listing for File SatSolvers.h

↰ Return to documentation for file (ADS/backtrack/SatSolvers.h)

/*--------------------------------------------------------------------------*/
/*--------------------------- File SatSolvers.h ----------------------------*/
/*--------------------------------------------------------------------------*/
/*--------------------------------------------------------------------------*/
/*----------------------------- DEFINITIONS --------------------------------*/
/*--------------------------------------------------------------------------*/

#ifndef __ADS_SatSolvers
 #define __ADS_SatSolvers
                      /* self-identification: #endif constant */

/*--------------------------------------------------------------------------*/
/*------------------------------ INCLUDES ----------------------------------*/
/*--------------------------------------------------------------------------*/

#include "ADS/Contract.h"
#include "ADS/complexity/Problems.h"

#include <algorithm>
#include <cstdlib>
#include <optional>
#include <queue>
#include <utility>
#include <vector>

/*--------------------------------------------------------------------------*/
/*--------------------------- NAMESPACE ------------------------------------*/
/*--------------------------------------------------------------------------*/

namespace ADS {

inline std::optional< std::vector< bool > > dpll( const Cnf & F , int n );

/*--------------------------------------------------------------------------*/
/*---------------------------- CLASS BasicCdcl -----------------------------*/
/*--------------------------------------------------------------------------*/

template< class Heap = std::priority_queue< std::pair< double , int > > >
class BasicCdcl {

/*--------------------------------------------------------------------------*/
 public:

 enum class Result { SAT , UNSAT , UNKNOWN };

 BasicCdcl( const Cnf & F , int n );

 Result solve( long maxConflicts = -1 );

 [[nodiscard]] const std::vector< bool > & model( void ) const;

 [[nodiscard]] long conflicts( void ) const { return( f_conflicts ); }
 [[nodiscard]] long decisions( void ) const { return( f_decisions ); }

/*--------------------------------------------------------------------------*/
 private:

 static int code( int lit ) {
  return( 2 * ( std::abs( lit ) - 1 ) + ( lit < 0 ) );
  }

 [[nodiscard]] int value( int c ) const;

 void enqueue( int c , int reason );
 [[nodiscard]] int propagate( void );
 void analyze( int confl , std::vector< int > & learnt , int & back );
 void cancelUntil( int level );
 void bump( int v );
 [[nodiscard]] int pickBranch( void );
 [[nodiscard]] int level( void ) const { return( int( f_trailLim.size() ) ); }
 int addClause( std::vector< int > c );

 Cnf f_F;
 int f_n;
 bool f_empty = false;
 std::vector< std::vector< int > > f_C;
 std::vector< std::vector< int > > f_watch;
 std::vector< int > f_assign , f_level , f_reason;
 std::vector< bool > f_phase , f_seen , f_model;
 std::vector< int > f_trail , f_trailLim;
 std::size_t f_qhead = 0;
 std::vector< double > f_act;
 double f_inc = 1;
 Heap f_heap;
 long f_conflicts = 0 , f_decisions = 0;

 };  // end( class BasicCdcl )

using Cdcl = BasicCdcl<>;

/*--------------------------------------------------------------------------*/

}  // end( namespace ADS )

/*--------------------------------------------------------------------------*/
/*-------------------------- IMPLEMENTATION --------------------------------*/
/*--------------------------------------------------------------------------*/

#include "ADS/backtrack/impl/SatSolvers.tpp"

/*--------------------------------------------------------------------------*/

#endif  /* SatSolvers.h included */

/*--------------------------------------------------------------------------*/
/*------------------------- End File SatSolvers.h --------------------------*/
/*--------------------------------------------------------------------------*/