line |
stmt |
bran |
cond |
sub |
pod |
time |
code |
1
|
|
|
|
|
|
|
package Algorithm::SAT::Expression; |
2
|
6
|
|
|
6
|
|
17646
|
use 5.008001; |
|
6
|
|
|
|
|
19
|
|
|
6
|
|
|
|
|
260
|
|
3
|
6
|
|
|
6
|
|
30
|
use strict; |
|
6
|
|
|
|
|
22
|
|
|
6
|
|
|
|
|
203
|
|
4
|
6
|
|
|
6
|
|
23
|
use warnings; |
|
6
|
|
|
|
|
7
|
|
|
6
|
|
|
|
|
212
|
|
5
|
|
|
|
|
|
|
require Algorithm::SAT::Backtracking; |
6
|
6
|
|
|
6
|
|
21
|
use Carp qw(croak); |
|
6
|
|
|
|
|
9
|
|
|
6
|
|
|
|
|
3190
|
|
7
|
|
|
|
|
|
|
our $VERSION = "0.11"; |
8
|
|
|
|
|
|
|
|
9
|
|
|
|
|
|
|
# Boolean expression builder. Note that the connector for clauses is `OR`; |
10
|
|
|
|
|
|
|
# so, when calling the instance methods `xor`, `and`, and `or`, the clauses |
11
|
|
|
|
|
|
|
# you're generating are `AND`ed with the existing clauses in the expression. |
12
|
|
|
|
|
|
|
sub new { |
13
|
25
|
|
|
25
|
0
|
31984
|
return bless { |
14
|
|
|
|
|
|
|
_literals => {}, |
15
|
|
|
|
|
|
|
_expr => [], |
16
|
|
|
|
|
|
|
_implementation => "Algorithm::SAT::Backtracking" |
17
|
|
|
|
|
|
|
}, |
18
|
|
|
|
|
|
|
shift; |
19
|
|
|
|
|
|
|
} |
20
|
|
|
|
|
|
|
|
21
|
|
|
|
|
|
|
sub with { |
22
|
20
|
|
|
20
|
1
|
32
|
my $self = shift; |
23
|
20
|
50
|
|
|
|
1386
|
if ( eval "require $_[0];1;" ) { |
24
|
20
|
|
|
|
|
57
|
$self->{_implementation} = shift; $self->{_implementation}->import(); |
|
20
|
|
|
|
|
126
|
|
25
|
|
|
|
|
|
|
} |
26
|
|
|
|
|
|
|
else { |
27
|
0
|
|
|
|
|
0
|
croak "The '$_[0]' could not be loaded"; |
28
|
|
|
|
|
|
|
} |
29
|
20
|
|
|
|
|
69
|
return $self; |
30
|
|
|
|
|
|
|
} |
31
|
|
|
|
|
|
|
|
32
|
|
|
|
|
|
|
# ### or |
33
|
|
|
|
|
|
|
# Add a clause consisting of the provided literals or'ed together. |
34
|
|
|
|
|
|
|
sub or { |
35
|
50
|
|
|
50
|
1
|
158
|
my $self = shift; |
36
|
50
|
|
|
|
|
74
|
$self->_ensure(@_); |
37
|
50
|
|
|
|
|
64
|
push( @{ $self->{_expr} }, [@_] ); |
|
50
|
|
|
|
|
89
|
|
38
|
50
|
|
|
|
|
70
|
return $self; |
39
|
|
|
|
|
|
|
} |
40
|
|
|
|
|
|
|
|
41
|
|
|
|
|
|
|
# ### xor |
42
|
|
|
|
|
|
|
# Add clauses causing each of the provided arguments to be xored.2 |
43
|
|
|
|
|
|
|
sub xor { |
44
|
|
|
|
|
|
|
|
45
|
|
|
|
|
|
|
# This first clause is the 'or' portion. "One of them must be true." |
46
|
10
|
|
|
10
|
1
|
1242
|
my $self = shift; |
47
|
10
|
|
|
|
|
23
|
my @literals = @_; |
48
|
10
|
|
|
|
|
13
|
push( @{ $self->{_expr} }, \@_ ); |
|
10
|
|
|
|
|
28
|
|
49
|
10
|
|
|
|
|
26
|
$self->_ensure(@literals); |
50
|
|
|
|
|
|
|
|
51
|
|
|
|
|
|
|
# Then, we generate clauses such that "only one of them is true". |
52
|
10
|
|
|
|
|
37
|
for ( my $i = 0; $i <= $#literals; $i++ ) { |
53
|
25
|
|
|
|
|
89
|
for ( my $j = $i + 1; $j <= $#literals; $j++ ) { |
54
|
20
|
|
|
|
|
47
|
push( |
55
|
20
|
|
|
|
|
17
|
@{ $self->{_expr} }, |
56
|
|
|
|
|
|
|
[ $self->negate_literal( $literals[$i] ), |
57
|
|
|
|
|
|
|
$self->negate_literal( $literals[$j] ) |
58
|
|
|
|
|
|
|
] |
59
|
|
|
|
|
|
|
); |
60
|
|
|
|
|
|
|
} |
61
|
|
|
|
|
|
|
} |
62
|
10
|
|
|
|
|
20
|
return $self; |
63
|
|
|
|
|
|
|
} |
64
|
|
|
|
|
|
|
|
65
|
|
|
|
|
|
|
# ### and |
66
|
|
|
|
|
|
|
# Add each of the provided literals into their own clause in the expression. |
67
|
|
|
|
|
|
|
sub and { |
68
|
10
|
|
|
10
|
1
|
39
|
my $self = shift; |
69
|
10
|
|
|
|
|
25
|
$self->_ensure(@_); |
70
|
10
|
|
|
|
|
33
|
push( @{ $self->{_expr} }, [$_] ) for @_; |
|
15
|
|
|
|
|
35
|
|
71
|
10
|
|
|
|
|
15
|
return $self; |
72
|
|
|
|
|
|
|
} |
73
|
|
|
|
|
|
|
|
74
|
|
|
|
|
|
|
# ### solve |
75
|
|
|
|
|
|
|
# Solve this expression with the backtrack solver. Lazy-loads the solver. |
76
|
|
|
|
|
|
|
sub solve { |
77
|
10
|
|
|
10
|
1
|
4603
|
return $_[0]->{_implementation} |
78
|
|
|
|
|
|
|
->new->solve( $_[0]->{_variables}, $_[0]->{_expr} ); |
79
|
|
|
|
|
|
|
} |
80
|
|
|
|
|
|
|
|
81
|
|
|
|
|
|
|
# ### _ensure |
82
|
|
|
|
|
|
|
# Private method that ensures that a particular literal is marked as being in |
83
|
|
|
|
|
|
|
# the expression. |
84
|
|
|
|
|
|
|
sub _ensure { |
85
|
70
|
|
|
70
|
|
66
|
my $self = shift; |
86
|
165
|
|
|
|
|
367
|
do { |
87
|
110
|
|
|
|
|
165
|
$self->{_literals}->{$_} = 1; |
88
|
110
|
|
|
|
|
82
|
push( @{ $self->{_variables} }, $_ ); |
|
110
|
|
|
|
|
201
|
|
89
|
|
|
|
|
|
|
} |
90
|
70
|
100
|
|
|
|
108
|
for grep { !$self->{_literals}->{$_} } |
|
165
|
|
|
|
|
330
|
|
91
|
|
|
|
|
|
|
map { substr( $_, 0, 1 ) eq "-" ? substr( $_, 1 ) : $_ } @_; |
92
|
|
|
|
|
|
|
} |
93
|
|
|
|
|
|
|
|
94
|
|
|
|
|
|
|
sub negate_literal { |
95
|
40
|
|
|
40
|
0
|
30
|
my $self = shift; |
96
|
40
|
|
|
|
|
34
|
my $var = shift; |
97
|
|
|
|
|
|
|
|
98
|
40
|
50
|
|
|
|
153
|
return ( substr( $var, 0, 1 ) eq "-" ) |
99
|
|
|
|
|
|
|
? substr( $var, 1 ) |
100
|
|
|
|
|
|
|
: '-' . $var; |
101
|
|
|
|
|
|
|
} |
102
|
|
|
|
|
|
|
|
103
|
|
|
|
|
|
|
1; |
104
|
|
|
|
|
|
|
__END__ |