Commit 3550d6f7 authored by Farid Alijani's avatar Farid Alijani
Browse files

sat solver added

parent af0b4891
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="12.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Debug|Win32'">
<LocalDebuggerCommandArguments>E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\Sat_Solver\Sat_Solver\ecos_features.dimacs</LocalDebuggerCommandArguments>
<DebuggerFlavor>WindowsLocalDebugger</DebuggerFlavor>
</PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)'=='Release|Win32'">
<LocalDebuggerCommandArguments>E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\Sat_Solver\Sat_Solver\ecos_features.dimacs</LocalDebuggerCommandArguments>
<DebuggerFlavor>WindowsLocalDebugger</DebuggerFlavor>
</PropertyGroup>
</Project>
\ No newline at end of file
#include "sat.h"
#include <iostream>
#include <string>
#include <cstdlib>
#include <cstdio>
using namespace std;
int main(int argc, char** argv)
{
SATSOLVER sat;
sat.import_file(argv[1]);
cout << "Press ENTER to terminate the program..." << endl;
cin.get();
return 0;
}
\ No newline at end of file
#include <iostream>
#include <fstream>
#include <cstdlib>
#include <cstdio>
#include <set>
#include <vector>
#include <assert.h>
#include "sat.h"
#include <dirent.h>
using namespace std;
const int SATSOLVER::max_line_length = 65536;
const int SATSOLVER::max_word_length = 64;
int SATSOLVER::line_number = 0;
// constructor
SATSOLVER::SATSOLVER()
{
};
//deconstructor
SATSOLVER::~SATSOLVER()
{
};
void SATSOLVER::import_file(char * filename)
{
char line_array[max_line_length];
char word_array[max_word_length];
set<int> clause_variables;
ifstream input_file(filename);
if (opendir(filename)){
cerr << "Can't open input file, it's a directory" << endl;
exit(1);
}
else if (!input_file) {
cerr << "Can't open input file" << endl;
//exit(1);
}
else
{
cerr << "File opened successfully" << endl;
}
while (input_file.getline(line_array, max_line_length))
{
++ line_number;
if (line_array[0] == 'c') // first line is initialized with 'c' => not improtant, continue...
{
continue;
}
else if (line_array[0] == 'p') // first line is initiallized with 'p' => save it...
{
int variable_num;
int clause_num;
int argument = sscanf(line_array, "p cnf %d %d", &variable_num, &clause_num);
if (argument < 2)
{
cerr << "variable and clause numbers aren't read!!"
<< " @ line : "
<< line_number
<< endl;
exit(3);
}
}
else
{
char *lp = line_array;
while (*lp)
{
char *wp = word_array;
while (*lp && ((*lp == ' ') || (*lp == '\t')))
{ // space or tab
lp++;
}
while (*lp && (*lp != ' ') && (*lp != '\t') && (*lp != '\n'))
{
*(wp++) = *(lp++);
}
*wp = '\0';
int string_length = strlen(word_array);
int var_indx = atoi(word_array);
if (string_length != 0) // build variables
{
if (var_indx != 0)
{
if (var_indx < 0) { var_indx = -var_indx;}
clause_variables.insert(var_indx);
cout << "String length = " << string_length
<< " , index = " << var_indx
<< endl;
}
else // build clauses (index = 0)
{
vector<int> temp;
for (set<int>::iterator it = clause_variables.begin();
it != clause_variables.end(); ++it)
{
temp.push_back(*it);
}
cout << "Clause size = " << temp.size() << endl;
clause_variables.clear();
}
}
}
}
}
};
void SATSOLVER::SAT_Solver()
{
};
void SATSOLVER::output()
{
};
\ No newline at end of file
#include <iostream>
#include <fstream>
#include <sstream>
#include <math.h>
class SATSOLVER
{
private:
public:
SATSOLVER();
~SATSOLVER();
static const int max_line_length;
static const int max_word_length;
static int line_number;
void import_file(char * filename);
void SAT_Solver();
void output();
};
\ No newline at end of file

Microsoft Visual Studio Solution File, Format Version 12.00
# Visual Studio 2013
VisualStudioVersion = 12.0.31101.0
MinimumVisualStudioVersion = 10.0.40219.1
Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "test_code", "test_code\test_code.vcxproj", "{419BE543-B096-420B-9207-9E1D481AADEA}"
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|Win32 = Debug|Win32
Release|Win32 = Release|Win32
EndGlobalSection
GlobalSection(ProjectConfigurationPlatforms) = postSolution
{419BE543-B096-420B-9207-9E1D481AADEA}.Debug|Win32.ActiveCfg = Debug|Win32
{419BE543-B096-420B-9207-9E1D481AADEA}.Debug|Win32.Build.0 = Debug|Win32
{419BE543-B096-420B-9207-9E1D481AADEA}.Release|Win32.ActiveCfg = Release|Win32
{419BE543-B096-420B-9207-9E1D481AADEA}.Release|Win32.Build.0 = Release|Win32
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
EndGlobalSection
EndGlobal
Build started 12/10/2016 9:07:09 PM.
1>Project "E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\test_code\test_code\test_code.vcxproj" on node 2 (Build target(s)).
1>ClCompile:
C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\bin\CL.exe /c /ZI /nologo /W3 /WX- /sdl /Od /Oy- /D WIN32 /D _CRT_SECURE_NO_WARNINGS /Gm /EHsc /RTC1 /MDd /GS /fp:precise /Zc:wchar_t /Zc:forScope /Fo"Debug\\" /Fd"Debug\vc120.pdb" /Gd /TP /analyze- /errorReport:prompt test_sample_code.cpp
test_sample_code.cpp
Link:
C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\bin\link.exe /ERRORREPORT:PROMPT /OUT:"E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\test_code\Debug\test_code.exe" /INCREMENTAL /NOLOGO kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /MANIFEST /MANIFESTUAC:"level='asInvoker' uiAccess='false'" /manifest:embed /DEBUG /PDB:"E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\test_code\Debug\test_code.pdb" /SUBSYSTEM:CONSOLE /TLBID:1 /DYNAMICBASE /NXCOMPAT /IMPLIB:"E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\test_code\Debug\test_code.lib" /MACHINE:X86 Debug\test_sample_code.obj
test_code.vcxproj -> E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\test_code\Debug\test_code.exe
1>Done Building Project "E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\test_code\test_code\test_code.vcxproj" (Build target(s)).
Build succeeded.
Time Elapsed 00:00:02.68
B^E:\LTH\GIT_REPOSITORY\THESIS\MOBILEROBOT\MACHINE_LEARNING\TEST_CODE\TEST_CODE\TEST_SAMPLE_CODE.CPP
B^E:\LTH\GIT_REPOSITORY\THESIS\MOBILEROBOT\MACHINE_LEARNING\TEST_CODE\TEST_CODE\TEST_SAMPLE_CODE.CPP
B^E:\LTH\GIT_REPOSITORY\THESIS\MOBILEROBOT\MACHINE_LEARNING\TEST_CODE\TEST_CODE\TEST_SAMPLE_CODE.CPP
B^E:\LTH\GIT_REPOSITORY\THESIS\MOBILEROBOT\MACHINE_LEARNING\TEST_CODE\TEST_CODE\DEBUG\TEST_SAMPLE_CODE.OBJ
B^E:\LTH\GIT_REPOSITORY\THESIS\MOBILEROBOT\MACHINE_LEARNING\TEST_CODE\TEST_CODE\DEBUG\TEST_SAMPLE_CODE.OBJ
B^E:\LTH\GIT_REPOSITORY\THESIS\MOBILEROBOT\MACHINE_LEARNING\TEST_CODE\TEST_CODE\DEBUG\TEST_SAMPLE_CODE.OBJ
#TargetFrameworkVersion=v4.0:PlatformToolSet=v120:EnableManagedIncrementalBuild=false:VCToolArchitecture=Native32Bit
Debug|Win32|E:\LTH\Git_Repository\thesis\MobileRobot\Machine_Learning\test_code\|
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment