bill,lsils

Problem with solve after solve and single-literal assumptions

The following test case does not fail:

Lines 163 to 178 in e0b12ec

 TEMPLATE_TEST_CASE("Solve after solve, no problem", "[sat][template]", SOLVER_TYPES) 

 { 

 TestType solver; 

 const auto zero = bill::lit_type{solver.add_variable()}; 

 const auto a = bill::lit_type{solver.add_variable()}; 

 const auto b = bill::lit_type{solver.add_variable()}; 

 const auto f = bill::lit_type{solver.add_variable()}; 

 solver.add_clause({~zero}); 

 solver.add_clause({~a, b, f}); 

 solver.add_clause({a, ~b, f}); 

 solver.add_clause({a, b, ~f}); 

 solver.add_clause({~a, ~b, ~f}); 

 CHECK(solver.solve({zero}) == bill::result::states::unsatisfiable); 

 }

The following test case fails in the second check for glucose_41, ghack, and maple solvers:

bill/tests/sat/sat.cpp

Lines 180 to 196 in e0b12ec

 TEMPLATE_TEST_CASE("Double assumptions, solve after solve", "[sat][template]", SOLVER_TYPES) 

 { 

 TestType solver; 

 const auto zero = bill::lit_type{solver.add_variable()}; 

 const auto a = bill::lit_type{solver.add_variable()}; 

 const auto b = bill::lit_type{solver.add_variable()}; 

 const auto f = bill::lit_type{solver.add_variable()}; 

 solver.add_clause({~zero}); 

 solver.add_clause({~a, b, f}); 

 solver.add_clause({a, ~b, f}); 

 solver.add_clause({a, b, ~f}); 

 solver.add_clause({~a, ~b, ~f}); 

 CHECK(solver.solve({f}) == bill::result::states::satisfiable); 

 CHECK(solver.solve({zero}) == bill::result::states::unsatisfiable); 

 }

Bug was discovered by @lee30sonia in lsils/mockturtle#303.

Test case is in branch msoeken/bug

Incompatibility with Alpine Linux

Hi,

I started deploying my software, which uses the EPFL Logic Synthesis Libraries, via Docker. I want to use Alpine Linux for image size reasons. As its standard C library, Alpine Linux uses musl libc instead of glibc and, therefore, does not include certain headers that glibc provides. One of which is fpu_control.h that is used in the ghack SAT solver here.

Its include is guarded by an #if defined(__linux__), but should probably be #if defined(__GLIBC__) from features.h. I don't know whether that would break anything though.

I'm not using bill directly but since it's included in mockturtle, it is affecting me.

Thank you for your help!
-- Marcel

lsils / bill Goto Github PK

bill's People

Contributors

Stargazers

Watchers

Forkers

bill's Issues

Problem with solve after solve and single-literal assumptions

Incompatibility with Alpine Linux

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent

	TEMPLATE_TEST_CASE("Solve after solve, no problem", "[sat][template]", SOLVER_TYPES)
	{
	TestType solver;
	const auto zero = bill::lit_type{solver.add_variable()};
	const auto a = bill::lit_type{solver.add_variable()};
	const auto b = bill::lit_type{solver.add_variable()};
	const auto f = bill::lit_type{solver.add_variable()};

	solver.add_clause({~zero});
	solver.add_clause({~a, b, f});
	solver.add_clause({a, ~b, f});
	solver.add_clause({a, b, ~f});
	solver.add_clause({~a, ~b, ~f});

	CHECK(solver.solve({zero}) == bill::result::states::unsatisfiable);
	}

	TEMPLATE_TEST_CASE("Double assumptions, solve after solve", "[sat][template]", SOLVER_TYPES)
	{
	TestType solver;
	const auto zero = bill::lit_type{solver.add_variable()};
	const auto a = bill::lit_type{solver.add_variable()};
	const auto b = bill::lit_type{solver.add_variable()};
	const auto f = bill::lit_type{solver.add_variable()};

	solver.add_clause({~zero});
	solver.add_clause({~a, b, f});
	solver.add_clause({a, ~b, f});
	solver.add_clause({a, b, ~f});
	solver.add_clause({~a, ~b, ~f});

	CHECK(solver.solve({f}) == bill::result::states::satisfiable);
	CHECK(solver.solve({zero}) == bill::result::states::unsatisfiable);
	}